Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

define and prove properties of orthocenters with vector algebra #294

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

define and prove properties of orthocenters with vector algebra #294

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
import EuclideanGeometry.Foundation.Axiom.Triangle.Basic
import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular

/-!

Expand All @@ -10,7 +11,15 @@ variable {P : Type _} [EuclideanPlane P]

def TriangleND.Height1 (tr_nd : TriangleND P) : SegND P := sorry

structure IsOrthocenter (tr_nd : TriangleND P) (H : P) : Prop where
-- this takes care of corner cases such as right triangles, where AH ⟂ BC runs into trouble since A = H
def IsOrthocenter (tr_nd : TriangleND P) (H : P) : Prop := inner (VEC tr_nd.point₁ H) (VEC tr_nd.point₂ tr_nd.point₃) = (0 : ℝ) ∧ inner (VEC tr_nd.point₂ H) (VEC tr_nd.point₃ tr_nd.point₁) = (0 : ℝ) ∧ inner (VEC tr_nd.point₃ H) (VEC tr_nd.point₁ tr_nd.point₂) = (0 : ℝ)
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. Please write this as a structure
structure IsOrthocenter ... : Prop where

to avoid usage of plural and.

  1. Is it possible to use perpendicular, or perp foot or LiesOn Height1 to define orthocenter? I do hope that there will be a "uniform" way of defining each center of a triangle. This needs a further discussion.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  1. Please write a plan file (possibly using overleaf) if you are going to build a whole new file, thank you! You may find some example of plan file in the folder PlanFiles.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LiesOn Height1 will work, but the necessary lemmas are not ready yet.


theorem orthocenter_exists (tr : Triangle P) (H : P) (h₁ : inner (VEC tr.point₁ H) (VEC tr.point₂ tr.point₃) = (0 : ℝ)) (h₂ : inner (VEC tr.point₂ H) (VEC tr.point₃ tr.point₁) = (0 : ℝ)) : inner (VEC tr.point₃ H) (VEC tr.point₁ tr.point₂) = (0 : ℝ) := by
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This theorem could be instead stated as a def that takes in an triangle and output a point. Then check this def do satisfies IsOrthocenter

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This strategy is used in the file AngBisector. Maybe first writing a plan file or discussing directly with me is more time-saving!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, this can be implemented. But surely there is no need to complete everything in one commit?

set A := tr.point₁
set B := tr.point₂
set C := tr.point₃
rw [← vec_sub_vec C, inner_sub_left, sub_eq_zero] at h₁ h₂
rw [← vec_sub_vec C A B, inner_sub_right, sub_eq_zero, ← neg_vec B C, inner_neg_right, h₁, h₂, real_inner_comm, ← inner_neg_left, neg_vec]

def TriangleND.Orthocenter (tr_nd : TriangleND P) : P := sorry

Expand Down