Theorems · Theorem · geometry

Affine.Triangle.eq_orthocenter_of_forall_mem_altitude

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P} {i₁ i₂ : Fin 3} {p : P},
  i₁ ≠ i₂ → p ∈ Affine.Simplex.altitude t i₁ → p ∈ Affine.Simplex.altitude t i₂ → p = t.orthocenter

The orthocenter is the only point lying in any two of the altitudes.

Defined in

Mathlib.Geometry.Euclidean.MongePoint

Cited by

1 results in Mathlib

Foundations

Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor