def EuclidGeom.Height_Line₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : EuclidGeom.Line P

Equations

• EuclidGeom.Height_Line₁ tr = EuclidGeom.perp_line (↑tr).point₁ (LIN (↑tr).point₂ (↑tr).point₃ (_ : (↑tr).point₃ ≠ (↑tr).point₂))

def EuclidGeom.Height_Line₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : EuclidGeom.Line P

Equations

• EuclidGeom.Height_Line₂ tr = EuclidGeom.perp_line (↑tr).point₂ (LIN (↑tr).point₃ (↑tr).point₁ (_ : (↑tr).point₁ ≠ (↑tr).point₃))

def EuclidGeom.Height_Line₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : EuclidGeom.Line P

Equations

• EuclidGeom.Height_Line₃ tr = EuclidGeom.perp_line (↑tr).point₃ (LIN (↑tr).point₁ (↑tr).point₂ (_ : (↑tr).point₂ ≠ (↑tr).point₁))

structure EuclidGeom.Is_Orthocenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) (H : P) : Prop

• perp1 : inner (EuclidGeom.Vec.mkPtPt (↑tr).point₁ H) (EuclidGeom.Vec.mkPtPt (↑tr).point₂ (↑tr).point₃) = 0
• perp2 : inner (EuclidGeom.Vec.mkPtPt (↑tr).point₂ H) (EuclidGeom.Vec.mkPtPt (↑tr).point₃ (↑tr).point₁) = 0
• perp3 : inner (EuclidGeom.Vec.mkPtPt (↑tr).point₃ H) (EuclidGeom.Vec.mkPtPt (↑tr).point₁ (↑tr).point₂) = 0

theorem EuclidGeom.orthocenter_exists {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) (H : P) (h₁ : inner (EuclidGeom.Vec.mkPtPt tr.point₁ H) (EuclidGeom.Vec.mkPtPt tr.point₂ tr.point₃) = 0) (h₂ : inner (EuclidGeom.Vec.mkPtPt tr.point₂ H) (EuclidGeom.Vec.mkPtPt tr.point₃ tr.point₁) = 0) : inner (EuclidGeom.Vec.mkPtPt tr.point₃ H) (EuclidGeom.Vec.mkPtPt tr.point₁ tr.point₂) = 0

theorem EuclidGeom.proj_eq_for_line_and_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (h : B ≠ A) : EuclidGeom.toProj (LIN A B h) = (VEC_nd A B h).toDir.toProj

theorem EuclidGeom.not_para_if_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : ¬EuclidGeom.Parallel (LIN (↑tr).point₁ (↑tr).point₂) (LIN (↑tr).point₃ (↑tr).point₁)

theorem EuclidGeom.two_perp_not_para {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l₁ : EuclidGeom.Line P) (l₂ : EuclidGeom.Line P) (l₃ : EuclidGeom.Line P) (l₄ : EuclidGeom.Line P) (h₁ : ¬EuclidGeom.Parallel l₁ l₂) (h₂ : EuclidGeom.Perpendicular l₃ l₁) (h₃ : EuclidGeom.Perpendicular l₄ l₂) : ¬EuclidGeom.Parallel l₃ l₄

theorem EuclidGeom.Height₁₂_not_para {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : ¬EuclidGeom.Parallel (EuclidGeom.Height_Line₁ tr) (EuclidGeom.Height_Line₂ tr)

theorem EuclidGeom.Height₂₃_not_para {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : ¬EuclidGeom.Parallel (EuclidGeom.Height_Line₂ tr) (EuclidGeom.Height_Line₃ tr)

def EuclidGeom.Orthocenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : P

Equations

• EuclidGeom.Orthocenter tr = EuclidGeom.Line.inx (EuclidGeom.Height_Line₁ tr) (EuclidGeom.Height_Line₂ tr) (_ : ¬EuclidGeom.Parallel (EuclidGeom.Height_Line₁ tr) (EuclidGeom.Height_Line₂ tr))

def EuclidGeom.aux_inter_is_Orthocenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : inner (EuclidGeom.Vec.mkPtPt (↑tr).point₁ (EuclidGeom.Orthocenter tr)) (EuclidGeom.Vec.mkPtPt (↑tr).point₂ (↑tr).point₃) = 0

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.aux_inter_is_Orthocenter_perm {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : inner (EuclidGeom.Vec.mkPtPt (↑tr).point₂ (EuclidGeom.Orthocenter tr)) (EuclidGeom.Vec.mkPtPt (↑tr).point₃ (↑tr).point₁) = 0

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.inter_is_Orthocenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : EuclidGeom.Is_Orthocenter tr (EuclidGeom.Orthocenter tr)

Equations

• (_ : EuclidGeom.Is_Orthocenter tr (EuclidGeom.Orthocenter tr)) = (_ : EuclidGeom.Is_Orthocenter tr (EuclidGeom.Orthocenter tr))

theorem EuclidGeom.lies_on_perp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (p₁ : P) (p₂ : P) (l₁ : EuclidGeom.Line P) (nd : p₁ ≠ p₂) (vert : EuclidGeom.Perpendicular (LIN p₁ p₂ (_ : p₂ ≠ p₁)) l₁) : EuclidGeom.lies_on p₂ (EuclidGeom.perp_line p₁ l₁)

theorem EuclidGeom.Orthocenter_on_all_height {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) : EuclidGeom.lies_on (EuclidGeom.Orthocenter tr) (EuclidGeom.Height_Line₁ tr) ∧ EuclidGeom.lies_on (EuclidGeom.Orthocenter tr) (EuclidGeom.Height_Line₂ tr) ∧ EuclidGeom.lies_on (EuclidGeom.Orthocenter tr) (EuclidGeom.Height_Line₃ tr)

theorem EuclidGeom.perm_orthocenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tr : EuclidGeom.TriangleND P} : EuclidGeom.Orthocenter (EuclidGeom.TriangleND.perm_vertices tr) = EuclidGeom.Orthocenter tr

theorem EuclidGeom.Orthocenter_iff_Is_Orthocenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr : EuclidGeom.TriangleND P) (H : P) : EuclidGeom.Is_Orthocenter tr H ↔ H = EuclidGeom.Orthocenter tr