lift_umax — Mathlib

English

The two-way universe lifting of ordinals with maximum universe parameters are equal.

Русский

Две эквивалентные операции подъёма по площадкам мира по максимальному верхнему уровню совпадают.

LaTeX

$$$\\operatorname{lift}_{\\max u v, u} = \\operatorname{lift}_{v, u}.$$$

Lean4

/-- `lift.{max u v, u}` equals `lift.{v, u}`.

Unfortunately, the simp lemma doesn't seem to work. -/
theorem lift_umax : lift.{max u v, u} = lift.{v, u} :=
  funext fun a =>
    inductionOn a fun _ r _ =>
      Quotient.sound ⟨(RelIso.preimage Equiv.ulift r).trans (RelIso.preimage Equiv.ulift r).symm⟩

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