mk_iUnion_le_sum_mk_lift — Mathlib

English

Let f: ι → Set α. Then lifting the cardinality of the union is at most the sum of the lifted cardinalities: lift(|⋃_i f(i)|) ≤ ∑_i lift(|f(i)|).

Русский

Пусть f: ι → Set α. Тогда подъем кардинальности объединения не больше суммы подъемов кардинальностей f(i).

LaTeX

$$$\\mathrm{lift}\\bigl(\\left|\\bigcup_{i} f(i)\\right|\\bigr) = \\sum_{i} \\left|f(i)\\right|$$$

Lean4

theorem mk_iUnion_le_sum_mk_lift {α : Type u} {ι : Type v} {f : ι → Set α} :
    lift.{v} #(⋃ i, f i) ≤ sum fun i => #(f i) :=
  calc
    lift.{v} #(⋃ i, f i) ≤ #(Σ i, f i) :=
      mk_le_of_surjective <| ULift.up_surjective.comp (Set.sigmaToiUnion_surjective f)
    _ = sum fun i => #(f i) := mk_sigma _

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