English
Equivalence between expressing v as a weightedVSub on s with weights w and as weightedVSub on the subtype of s with the corresponding weights.
Русский
Эквивалентность выражения в виде weightedVSub на s и на подтипе s с соответствующими весами.
LaTeX
$$$$ \exists fs, w, v = fs.weightedVSub p w \iff \exists fs', w', v = fs'.weightedVSub (p|_s) w'. $$$$
Lean4
/-- Suppose an indexed family of points is given, along with a subset
of the index type. A vector can be expressed as
`weightedVSubOfPoint` using a `Finset` lying within that subset and
with a given sum of weights if and only if it can be expressed as
`weightedVSubOfPoint` with that sum of weights for the
corresponding indexed family whose index type is the subtype
corresponding to that subset. -/
theorem eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype {v : V} {x : k} {s : Set ι} {p : ι → P}
{b : P} :
(∃ fs : Finset ι, ↑fs ⊆ s ∧ ∃ w : ι → k, ∑ i ∈ fs, w i = x ∧ v = fs.weightedVSubOfPoint p b w) ↔
∃ (fs : Finset s) (w : s → k), ∑ i ∈ fs, w i = x ∧ v = fs.weightedVSubOfPoint (fun i : s => p i) b w :=
by
classical
simp_rw [weightedVSubOfPoint_apply]
constructor
· rintro ⟨fs, hfs, w, rfl, rfl⟩
exact ⟨fs.subtype s, fun i => w i, sum_subtype_of_mem _ hfs, (sum_subtype_of_mem _ hfs).symm⟩
· rintro ⟨fs, w, rfl, rfl⟩
refine
⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i => if h : i ∈ s then w ⟨i, h⟩ else 0, ?_,
?_⟩ <;>
simp
