English
Equivalence between expressing v as a weightedVSub over a subset s using a Finset and expressing it over the subtype with the same sum of weights.
Русский
Эквивалентность выражения v в weightedVSub через подмножество и через подтип с тем же сумарным весом.
LaTeX
$$$$ (\exists fs ⊆ s)(\exists w) (\sum w_i = x) \land v = fs.weightedVSub p w \iff \dots $$$$
Lean4
/-- Suppose an indexed family of points is given, along with a subset
of the index type. A vector can be expressed as `weightedVSub` using
a `Finset` lying within that subset and with sum of weights 0 if and
only if it can be expressed as `weightedVSub` with sum of weights 0
for the corresponding indexed family whose index type is the subtype
corresponding to that subset. -/
theorem eq_weightedVSub_subset_iff_eq_weightedVSub_subtype {v : V} {s : Set ι} {p : ι → P} :
(∃ fs : Finset ι, ↑fs ⊆ s ∧ ∃ w : ι → k, ∑ i ∈ fs, w i = 0 ∧ v = fs.weightedVSub p w) ↔
∃ (fs : Finset s) (w : s → k), ∑ i ∈ fs, w i = 0 ∧ v = fs.weightedVSub (fun i : s => p i) w :=
eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
