card_biUnion — Mathlib

English

If t : ι → Finset M has pairwise disjoint sets, then |s.biUnion t| = ∑_{u ∈ s} |t(u)|.

Русский

Если функция t имеет попарно непересекающиеся множества, тогда |s.biUnion t| = ∑_{u ∈ s} |t(u)|.

LaTeX

$$$$\\#(s.biUnion t) = \\sum_{u \\in s} \\#(t(u))$$$$

Lean4

theorem card_biUnion [DecidableEq M] {t : ι → Finset M} (h : s.toSet.PairwiseDisjoint t) :
    #(s.biUnion t) = ∑ u ∈ s, #(t u) := by simpa using sum_biUnion h (M := ℕ) (f := 1)

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