mem_altitude — Mathlib

English

A vertex of a simplex lies on its corresponding altitude: s.points i ∈ s.altitude i.

Русский

Вершина многоугольника принадлежит соответствующей высоте: s.points i ∈ s.altitude i.

LaTeX

$$$s.points i \in s.altitude i$$$

Lean4

/-- A vertex lies in the corresponding altitude. -/
theorem mem_altitude {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.points i ∈ s.altitude i :=
  (mem_inf_iff _ _ _).2 ⟨self_mem_mk' _ _, mem_affineSpan ℝ (Set.mem_range_self _)⟩

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