altitudeFoot_mem_affineSpan_faceOpposite

English

Altiude foot lies in the affine span of the face opposite a vertex.

Русский

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

LaTeX

$$$\mathrm{altitudeFoot}_i \in \operatorname{affineSpan}(\mathrm{faceOpposite}(s,i).\mathrm{points})$$$

Lean4

theorem altitudeFoot_mem_affineSpan_faceOpposite {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    s.altitudeFoot i ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points) :=
  orthogonalProjection_mem _

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