altitude — Mathlib

English

An altitude of a simplex is the line through a vertex perpendicular to the opposite face.

Русский

Высота треугольника/многоугольника — это прямая, проходящая через вершину и перпендикулярная к противорежной грани.

LaTeX

$$$\text{altitude}(s,i) \text{ is the line through } s.points i \text{ perpendicular to the opposite face}$$$

Lean4

/-- An altitude of a simplex is the line that passes through a vertex
and is orthogonal to the opposite face. -/
def altitude {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : AffineSubspace ℝ P :=
  mk' (s.points i) (affineSpan ℝ (s.points '' { i }ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)

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