mk_iUnion_le_sum_mk — Mathlib

English

For any family f: ι → Set α, the cardinality of the union is at most the sum of the cardinalities: |⋃_i f(i)| ≤ ∑_i |f(i)|.

Русский

Для любой семейства f: ι → Set α кардинал суммы объединения несложно ограничен суммой кардиналов входящих множеств: |⋃_i f(i)| ≤ ∑_i |f(i)|.

LaTeX

$$$\\left|\\bigcup_{i} f(i)\\right| \\le \\sum_{i} |f(i)|$$$

Lean4

theorem mk_iUnion_le_sum_mk {α ι : Type u} {f : ι → Set α} : #(⋃ i, f i) ≤ sum fun i => #(f i) :=
  calc
    #(⋃ i, f i) ≤ #(Σ i, f i) := mk_le_of_surjective (Set.sigmaToiUnion_surjective f)
    _ = sum fun i => #(f i) := mk_sigma _

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