mk_iUnion_eq_sum_mk — Mathlib

English

If a family f: ι → Set α is pairwise disjoint, then the cardinality of the union equals the sum of the cardinalities: |⋃_i f(i)| = ∑_i |f(i)|.

Русский

Если множество f(i) попарно непересекаются, то кардинальность объединения равна сумме кардинальностей: |⋃_i f(i)| = ∑_i |f(i)|.

LaTeX

$$$\\left|\\bigcup_{i} f(i)\\right| = \\sum_{i} |f(i)|$$$

Lean4

theorem mk_iUnion_eq_sum_mk {α ι : Type u} {f : ι → Set α} (h : Pairwise (Disjoint on f)) :
    #(⋃ i, f i) = sum fun i => #(f i) :=
  calc
    #(⋃ i, f i) = #(Σ i, f i) := mk_congr (Set.unionEqSigmaOfDisjoint h)
    _ = sum fun i => #(f i) := mk_sigma _

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