out_lift_equiv — Mathlib

English

There exists an equivalence between the out of the lift of a cardinal and the out of the cardinal itself.

Русский

Существует эквивалентность между выходом подъема кардинала и выходом самого кардинала.

LaTeX

$$Nonempty ((lift\\, a).out ≃ a.out)$$

Lean4

theorem out_lift_equiv (a : Cardinal.{u}) : Nonempty ((lift.{v} a).out ≃ a.out) :=
  by
  rw [← mk_out a, ← mk_uLift, mk_out]
  exact ⟨outMkEquiv.trans Equiv.ulift⟩

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