English
A specialized version: lift a lift equality is equivalent to the existence of a bijection α ≃ β.
Русский
Усложнённая версия: равенство подъемов эквивалентно существованию биекции α ≃ β.
LaTeX
$$$\\forall {\\alpha : Type u} {\\beta : Type v}, \\; (lift.{v} \\#\\alpha = lift.{u} \\#\\beta) \\iff \\exists (e: \\alpha \\simeq \\beta)$$$
Lean4
/-- A variant of `Cardinal.lift_mk_eq` with specialized universes.
Because Lean often cannot realize it should use this specialization itself,
we provide this statement separately so you don't have to solve the specialization problem either.
-/
theorem lift_mk_eq' {α : Type u} {β : Type v} : lift.{v} #α = lift.{u} #β ↔ Nonempty (α ≃ β) :=
lift_mk_eq.{u, v, 0}
