lift_umax_eq — Mathlib

English

Equality of lifts across universes reduces to equality after lifting in the opposite direction: lift_{max v w} a = lift_{max u w} b ⇔ lift_v a = lift_u b.

Русский

Равенство подъёмов между вселенными эквивалентно равенству после подъёма в противоположном направлении: lift_{max v w} a = lift_{max u w} b ⇔ lift_v a = lift_u b.

LaTeX

$$$$ \\operatorname{lift}_{\\max v w} a = \\operatorname{lift}_{\\max u w} b \\iff \\operatorname{lift}_{v} a = \\operatorname{lift}_{u} b. $$$$

Lean4

theorem lift_umax_eq {a : Cardinal.{u}} {b : Cardinal.{v}} :
    lift.{max v w} a = lift.{max u w} b ↔ lift.{v} a = lift.{u} b := by
  rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]

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