ncard_biUnion — Mathlib

English

If t is a finite set of indices and each s(i) is finite, and the family s is pairwise disjoint, then the ncard of the union equals the finsum of ncard(s(i)).

Русский

Если t содержит конечное число индексов, каждый s(i) конечен и семейство попарно непересекается, то мощность объединения равна сумме мощностей.

LaTeX

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

Lean4

theorem ncard_biUnion {t : Set ι} (ht : t.Finite) {s : ι → Set α} (hs : ∀ i ∈ t, (s i).Finite)
    (h : t.PairwiseDisjoint s) : (⋃ i ∈ t, s i).ncard = ∑ᶠ i ∈ t, (s i).ncard := by
  rw [← finsum_one, finsum_mem_biUnion h ht hs, finsum_mem_congr rfl fun i hi ↦ finsum_one]

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