English
As above, for finite index sets with disjoint families, encard of the union is the finsum of encards.
Русский
Как выше, для конечных индексов с попарно непересекающимися семействами, encard объединения равен сумме encard.
LaTeX
$$$(\\bigcup_{i\\in t} s(i)).encard = \\sum_{i\\in t} (s(i)).encard$$$
Lean4
theorem encard_biUnion {t : Set ι} (ht : t.Finite) {s : ι → Set α} (hs : t.PairwiseDisjoint s) :
(⋃ i ∈ t, s i).encard = ∑ᶠ i ∈ t, (s i).encard := by
classical
by_cases h : ∀ i ∈ t, (s i).Finite
· have : (⋃ i ∈ t, s i).Finite := ht.biUnion (fun i hi ↦ h i hi)
rw [← this.cast_ncard_eq, ncard_biUnion ht h hs, ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq,
Nat.cast_finsum_mem ht]
· simp only [not_forall] at h
obtain ⟨i, hi, (hn : (s i).Infinite)⟩ := h
rw [← Set.insert_diff_self_of_mem hi, finsum_mem_insert _ (notMem_diff_of_mem <| mem_singleton i) ht.diff]
simp [hn]
