English
There is an equivalence between expressing a vector as a weightedVSubOfPoint using a Finset within a subset s of indices and expressing the same using the corresponding subtype Finset. The equivalence is between fs ⊆ s with weights and fs mapped to s via the subtype.
Русский
Существуют эквивалентности между выражениями в weightedVSubOfPoint через подмножество и через подтип соответствующего подмножества индексов.
LaTeX
$$$$ \exists fs \subset s, \exists w, \sum_{i\in fs} w_i = x \land v = fs.weightedVSubOfPoint p b w \iff \exists fs' \subset s, \exists w', \sum w'=x \land v = fs'.weightedVSubOfPoint (fun i \to p i) b w' $$$$
Lean4
/-- An affine combination over `s.subtype pred` equals one over `{x ∈ s | pred x}`. -/
theorem affineCombination_subtype_eq_filter (w : ι → k) (p : ι → P) (pred : ι → Prop) [DecidablePred pred] :
((s.subtype pred).affineCombination k (fun i => p i) fun i => w i) = {x ∈ s | pred x}.affineCombination k p w := by
rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]
