height — Mathlib · SciLib

English

The height of a vertex i of a simplex s is the distance between the vertex i and the foot of its altitude.

Русский

Высота вершины i у симплекса s равна расстоянию между вершиной i и опорной точкой высоты из этой вершины.

LaTeX

$$$\\mathrm{height}(s,i)=\\operatorname{dist}(s.\\text{points}(i), s.\\text{altitudeFoot}(i))$$$

Lean4

/-- The height of a vertex of a simplex is the distance between it and the foot of the altitude
from that vertex. -/
def height {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : ℝ :=
  dist (s.points i) (s.altitudeFoot i)

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