setInterior_subset_affineSpan — Mathlib

English

Every point expressible as an affine combination of vertices lies in the affine span of those vertices.

Русский

Любая точка, выражаемая как аффинное сочетание вершин, принадлежит афинному образу порождающих вершин.

LaTeX

$$$ s.\mathrm{setInterior} I \subseteq \operatorname{affineSpan}(\{s.points(i)\}). $$$

Lean4

theorem setInterior_subset_affineSpan {I : Set k} {n : ℕ} {s : Simplex k P n} :
    s.setInterior I ⊆ affineSpan k (Set.range s.points) :=
  by
  rintro p ⟨w, hw, hi, rfl⟩
  exact affineCombination_mem_affineSpan_of_nonempty hw _

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