mk_iUnion_eq_sum_mk_lift — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mk_iUnion_eq_sum_mk_lift {α : Type u} {ι : Type v} {f : ι → Set α} (h : Pairwise (Disjoint on f)) :
    lift.{v} #(⋃ i, f i) = sum fun i => #(f i) :=
  calc
    lift.{v} #(⋃ i, f i) = #(Σ i, f i) := mk_congr <| .trans Equiv.ulift (Set.unionEqSigmaOfDisjoint h)
    _ = sum fun i => #(f i) := mk_sigma _

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