altitudeFoot — Mathlib

English

The altitude foot is the orthogonal projection of a vertex of a simplex onto the opposite face.

Русский

Опорная точка высоты — ортогональная проекция вершины симплекса на противоположную грань.

LaTeX

$$$\text{altitudeFoot}(s,i) = \operatorname{orthogonalProjection}_{\text{faceOpposite}}(s.\text{points}(i))$$$

Lean4

/-- The foot of an altitude is the orthogonal projection of a vertex of a simplex onto the
opposite face. -/
def altitudeFoot {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : P :=
  (s.faceOpposite i).orthogonalProjectionSpan (s.points i)

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