altitudeFoot_mem_affineSpan — Mathlib

English

The altitude foot belongs to the affine span of the vertex set of the simplex.

Русский

Опорная точка высоты принадлежит афинной оболочке множества вершин симплекса.

LaTeX

$$$\mathrm{altitudeFoot}_i \in \operatorname{affineSpan}(\{ s.\text{points}(j) : j\in \{0,\dots,n\} \})$$$

Lean4

theorem altitudeFoot_mem_affineSpan {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    s.altitudeFoot i ∈ affineSpan ℝ (Set.range s.points) :=
  by
  refine SetLike.le_def.1 (affineSpan_mono _ ?_) (s.altitudeFoot_mem_affineSpan_faceOpposite _)
  simp

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