English
If f is injective on a finite set s, attaching the affine combination over s to a function yields the same as taking the affine combination over the image of f and precomposing accordingly.
Русский
Если f инъективна на s, присоединение аффинной комбинации над s к функции дает то же самое, что и прямая комбинация над образами f, с предобработкой.
LaTeX
$$$ s.attach.affineCombination k f (w \circ f) = (image f unary).affineCombination k id w $$$
Lean4
theorem attach_affineCombination_of_injective [DecidableEq P] (s : Finset P) (w : P → k) (f : s → P)
(hf : Function.Injective f) : s.attach.affineCombination k f (w ∘ f) = (image f univ).affineCombination k id w :=
by
simp only [affineCombination, weightedVSubOfPoint_apply, id, vadd_right_cancel_iff, Function.comp_apply,
AffineMap.coe_mk]
let g₁ : s → V := fun i => w (f i) • (f i -ᵥ Classical.choice S.nonempty)
let g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice S.nonempty)
change univ.sum g₁ = (image f univ).sum g₂
have hgf : g₁ = g₂ ∘ f := by
ext
simp [g₁, g₂]
rw [hgf, sum_image]
· simp only [g₂, Function.comp_apply]
· exact fun _ _ _ _ hxy => hf hxy
