closedInterior_subset_affineSpan — Mathlib

English

Every point in the closed interior can be expressed as an affine combination of the vertices, hence lies in the affine span of the vertices.

Русский

Каждая точка в закрытой внутренности может быть выражена как аффинное сочетание вершин, следовательно принадлежит афинному span вершин.

LaTeX

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

Lean4

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

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