English
The direction of an altitude is orthogonal to the vector span of the opposite face.
Русский
Направление высоты ортогонально к вектоpному спану противоребра высоты.
LaTeX
$$$\left( s.altitude(i) \right).\mathrm{direction} \perp \operatorname{vectorSpan}_{\mathbb{R}}\left( s.points''\\{ i \}^c \right)$$$
Lean4
/-- The direction of an altitude. -/
theorem direction_altitude {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) :
(s.altitude i).direction = (vectorSpan ℝ (s.points '' { i }ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points) := by
rw [altitude_def, direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
direction_mk', direction_affineSpan, direction_affineSpan]