affineSpan_orthocenter_point_le_altitude

English

Perpendicular bisector of a segment in a Euclidean affine space: the set of points equidistant from p1 and p2, passing through the midpoint.

Русский

Перпендикулярная биссектриса отрезка в евклидовом аффинном пространстве — множество точек равноудалённых от p1 и p2, проходящее через середину.

LaTeX

$$$\operatorname{perpBisector}(p_1,p_2) = \{ x : P \mid \langle p_2-p_1, x-\tfrac{p_1+p_2}{2} \rangle = 0\}$$$

Lean4

/-- The affine span of the orthocenter and a vertex is contained in
the altitude. -/
theorem affineSpan_orthocenter_point_le_altitude (t : Triangle ℝ P) (i : Fin 3) :
    line[ℝ, t.orthocenter, t.points i] ≤ t.altitude i :=
  by
  refine affineSpan_le_of_subset_coe ?_
  rw [Set.insert_subset_iff, Set.singleton_subset_iff]
  exact ⟨t.orthocenter_mem_altitude, t.mem_altitude i⟩

Похожие утверждения