fold_disjiUnion — Mathlib

English

Under the disjointness hypothesis, the disjiUnion over f coincides with the biUnion over f.

Русский

При условии попарной непересекаемости disjiUnion совпадает с biUnion.

LaTeX

$$$s.disjiUnion f hf = s.biUnion f$$$

Lean4

theorem fold_disjiUnion {ι : Type*} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h) :
    (s.disjiUnion t h).fold op (s.fold op b₀ b) f = s.fold op b₀ fun i => (t i).fold op (b i) f :=
  (congr_arg _ <| Multiset.map_bind _ _ _).trans (Multiset.fold_bind _ _ _ _ _)

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