English
Given p : ι → P and s ⊆ Set ι, an affineCombination for the image p''s subset can be expressed as an affineCombination with a corresponding finite subset fs of ι.
Русский
Для множества образа p'' подмножества s можно выразить аффинное сочетание через конечное множество fs внутри ι.
LaTeX
$$Существуют fs : Finset ι, w : ι → k с fs ⊆ s и p1 = fs.affineCombination k p w$$
Lean4
/-- A point in the `affineSpan` of a subset of an indexed family is an
`affineCombination` with sum of weights 1, using only points in the given subset. -/
theorem eq_affineCombination_of_mem_affineSpan_image {p₁ : P} {p : ι → P} {s : Set ι} (h : p₁ ∈ affineSpan k (p '' s)) :
∃ (fs : Finset ι) (w : ι → k), ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ p₁ = fs.affineCombination k p w := by
classical
rw [Set.image_eq_range] at h
obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h
refine
⟨fs'.map (Function.Embedding.subtype _), fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0, (by simp), (by simp [hw']),
?_⟩
simp only [Finset.affineCombination_map, Function.Embedding.coe_subtype]
exact fs'.affineCombination_congr (by simp) (by simp)
