mem_affineSpan_image_iff — Mathlib

English

Let s be a simplex, fs a finite set of indices, and i an index. Then s.points i lies in the affine span of the image of s.points on fs if and only if i ∈ fs.

Русский

Пусть s — симплекс, fs — конечный набор индексов, i — индекс. Тогда точка s.points i принадлежит афинному обобщению образа s.points на fs тогда и только если i принадлежит fs.

LaTeX

$$$ s.points(i) \\in \\operatorname{affineSpan}_k( s.points''fs ) \\iff i \\in fs $$$

Lean4

@[simp]
theorem mem_affineSpan_image_iff [Nontrivial k] {n : ℕ} (s : Simplex k P n) {fs : Set (Fin (n + 1))} {i : Fin (n + 1)} :
    s.points i ∈ affineSpan k (s.points '' fs) ↔ i ∈ fs :=
  s.independent.mem_affineSpan_iff _ _

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