lift_mk_eq — Mathlib

English

Equality of lifts of mk α and mk β is equivalent to the existence of a bijection α ≃ β.

Русский

Сходство подъемов mk α и mk β эквивалентно существованию биекции α ≃ β.

LaTeX

$$$\\text{lift}^{\\max v w} \\#α = \\text{lift}^{\\max u w} \\#β \\iff \\text{Nonempty}(α \\simeq β)$$$

Lean4

theorem lift_mk_eq {α : Type u} {β : Type v} : lift.{max v w} #α = lift.{max u w} #β ↔ Nonempty (α ≃ β) :=
  Quotient.eq'.trans
    ⟨fun ⟨f⟩ => ⟨Equiv.ulift.symm.trans <| f.trans Equiv.ulift⟩, fun ⟨f⟩ =>
      ⟨Equiv.ulift.trans <| f.trans Equiv.ulift.symm⟩⟩

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