ncard_iUnion_le_of_fintype — Mathlib

English

If ι is finite, then the ncard of the union is less than or equal to the finsum of ncards.

Русский

Если индексный набор конечен, мощность объединения не превосходит суммы мощностей.

LaTeX

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

Lean4

theorem ncard_iUnion_le_of_fintype [Fintype ι] (s : ι → Set α) : (⋃ i, s i).ncard ≤ ∑ i, (s i).ncard := by
  simpa using Finset.univ.set_ncard_biUnion_le s

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