encard_iUnion_of_finite — Mathlib

English

If the index type ι is finite, then the encard of the union equals the finsum of encards.

Русский

Если индексный тип ι конечен, то encard объединения равен сумме encard.

LaTeX

$$$\\text{Encards}(\\bigcup_i s(i)) = \\sum_i (s(i)).encard$$$

Lean4

theorem encard_iUnion_of_finite [Finite ι] {s : ι → Set α} (hs : Pairwise (Disjoint on s)) :
    (⋃ i, s i).encard = ∑ᶠ i, (s i).encard :=
  by
  rw [← finsum_mem_univ, ← finite_univ.encard_biUnion (fun a _ b _ hab ↦ hs hab)]
  simp

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