encard_biUnion_le — Mathlib

English

If ι is finite, then the encard of the union is at most the finsum of encards.

Русский

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

LaTeX

$$$(\\bigcup_i s(i)).encard \\le \\sum_i (s(i)).encard$$

Lean4

theorem encard_biUnion_le {t : Set ι} (ht : t.Finite) (s : ι → Set α) :
    (⋃ i ∈ t, s i).encard ≤ ∑ᶠ i ∈ t, (s i).encard := by
  simpa [← finsum_mem_eq_finite_toFinset_sum] using ht.toFinset.set_encard_biUnion_le s

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