direction_altitude — Mathlib

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]

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