altitudeFoot_mem_affineSpan_image_compl

English

The altitude foot lies in the affine span of the image of the complementary face.

Русский

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

LaTeX

$$$\mathrm{altitudeFoot}_i \in \operatorname{affineSpan}(\mathrm{points}_i''\,\text{compl})$$$

Lean4

@[simp]
theorem altitudeFoot_mem_affineSpan_image_compl {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    s.altitudeFoot i ∈ affineSpan ℝ (s.points '' { i }ᶜ) :=
  by
  rw [← range_faceOpposite_points]
  exact orthogonalProjection_mem _

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