touchpoint_mem_affineSpan — Mathlib

English

The touchpoint lies in the affine span of the face opposite i's vertices.

Русский

Touchpoint принадлежит афинному замещению вершин грани противоположной i.

LaTeX

$$s.touchpoint(signs,i) ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points)$$

Lean4

theorem touchpoint_mem_affineSpan (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) :
    s.touchpoint signs i ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points) :=
  orthogonalProjection_mem _

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