lift_umax — Mathlib

English

Two universal lifts coincide: lifting from u to max(u,v) then to u is the same as lifting from v to u.

Русский

Две операции подъёма по наименьшему и максимальному вселенным совпадают: подъем из u до max(u,v) затем до u эквивалентен подьему из v до u.

LaTeX

$$$\\mathrm{lift}^{\\max u v, u} = \\mathrm{lift}^{v, u}$$$

Lean4

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

Unfortunately, the simp lemma doesn't work. -/
theorem lift_umax : lift.{max u v, u} = lift.{v, u} :=
  funext fun a => inductionOn a fun _ => (Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq

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