ncard_iUnion_le_of_finite — Mathlib

English

If s is a family of sets indexed by a finite ι, then the ncard of the union is bounded by the finsum of ncards.

Русский

Если s имеет конечное индексационное множество, то мощность объединения ограничена суммой мощностей.

LaTeX

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

Lean4

theorem ncard_iUnion_le_of_finite [Finite ι] (s : ι → Set α) : (⋃ i, s i).ncard ≤ ∑ᶠ i, (s i).ncard := by
  simpa using finite_univ.ncard_biUnion_le s

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