fold_image — Mathlib

English

If g : γ → α is injective on s, then folding over image g equals folding over s with f ∘ g.

Русский

Если g инъективно отображает s в α, то свёртка по image g равна свёртке по s с f ∘ g.

LaTeX

$$$\\mathrm{fold}_{op}\\; b\\; f\\; (\\mathrm{image}\\ g\\ s) = \\mathrm{fold}_{op}\\; b\\; (f \\circ g)\\; s$$$

Lean4

@[simp]
theorem fold_image [DecidableEq α] {g : γ → α} {s : Finset γ} (H : Set.InjOn g s) :
    (s.image g).fold op b f = s.fold op b (f ∘ g) := by simp only [fold, image_val_of_injOn H, Multiset.map_map]

Похожие утверждения