touchpoint_mem_affineSpan_simplex

English

The touchpoint lies in the affine span of the range of the simplex's points.

Русский

Touchpoint принадлежит афинному замещению диапазона точек симплекса.

LaTeX

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

Lean4

/-- A weaker version of `touchpoint_mem_affineSpan`. -/
theorem touchpoint_mem_affineSpan_simplex (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) :
    s.touchpoint signs i ∈ affineSpan ℝ (Set.range s.points) :=
  by
  refine SetLike.le_def.1 (affineSpan_mono _ ?_) (s.touchpoint_mem_affineSpan signs i)
  simp

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