ncard_iUnion_of_finite — Mathlib

English

If t is finite and the family s is pairwise disjoint, then the encard of the union equals the finsum of encards.

Русский

Если t конечно и family s попарно непересекается, то encard объединения равен сумме encard.

LaTeX

$$$(\\bigcup_{i \\in t} s(i)).encard = \\sum_{i \\in t} (s(i)).encard$$

Lean4

theorem ncard_iUnion_of_finite [Finite ι] {s : ι → Set α} (hs : ∀ i, (s i).Finite) (h : Pairwise (Disjoint on s)) :
    (⋃ i, s i).ncard = ∑ᶠ i : ι, (s i).ncard :=
  by
  rw [← finsum_mem_univ, ← finite_univ.ncard_biUnion (by simpa) (fun _ _ _ _ hab ↦ h hab)]
  simp

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