mk_iUnion_le_lift — Mathlib

English

If f is pairwise disjoint, then lifting the cardinality of the union equals the sum of the lifted cardinalities: lift(|⋃_i f(i)|) = ∑_i |f(i)|.

Русский

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

LaTeX

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

Lean4

theorem mk_iUnion_le_lift {α : Type u} {ι : Type v} (f : ι → Set α) :
    lift.{v} #(⋃ i, f i) ≤ lift.{u} #ι * ⨆ i, lift.{v} #(f i) :=
  by
  refine mk_iUnion_le_sum_mk_lift.trans <| Eq.trans_le ?_ (sum_le_iSup_lift _)
  rw [← lift_sum, lift_id'.{_, u}]

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