lift_mk_shrink — Mathlib

English

For type α with a small instance, lifting the size of Shrink(α) equals lifting the size of α.

Русский

Для типа α с малым экземпляром подъем размеров Shrink(α) равен подъем размера α.

LaTeX

$$$\\operatorname{lift} (\\#\\mathrm{Shrink}(\\alpha)) = \\operatorname{lift} (\\#\\alpha)$$$

Lean4

theorem lift_mk_shrink (α : Type u) [Small.{v} α] :
    Cardinal.lift.{max u w} #(Shrink.{v} α) = Cardinal.lift.{max v w} #α :=
  lift_mk_eq.2 ⟨(equivShrink α).symm⟩

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