encard_iUnion_le_of_finite — Mathlib

English

Let ι be a finite index type and s : ι → Set α a family of subsets. Then the ENat-cardinality of the union over all i of s(i) is at most the finsum of the ENat-cardinalities of the individual sets: encard(⋃ i, s(i)) ≤ ∑ᶠ i, encard(s(i)).

Русский

Пусть ι — конечно индексное множество, и dано семейство подмножеств s(i) ⊆ α. Тогда ENat-кардинал объединения ⋃ i, s(i) не превосходит финитную сумму кардиналов каждого множества: encard(⋃ i, s(i)) ≤ ∑ᶠ i, encard(s(i)).

LaTeX

$$$ (\bigcup_{i \in ι} s(i)).encard \le \sum_{i \in ι} (s(i)).encard $$$

Lean4

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

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