lift_id' — Mathlib

English

A cardinal lifted to a lower or equal universe equals itself; lift down from max(u,v) to u yields the same cardinal.

Русский

Кардинал, поднятый в более низкую или равную вселенную, остаётся тем же самым; понижающий подъем не меняет кардинал.

LaTeX

$$$\\text{lift}^{u} a = a \\quad (a : \\mathrm{Cardinal} .\\{\\text{max } u v\\})$$$

Lean4

/-- A cardinal lifted to a lower or equal universe equals itself.

Unfortunately, the simp lemma doesn't work. -/
theorem lift_id' (a : Cardinal.{max u v}) : lift.{u} a = a :=
  inductionOn a fun _ => mk_congr Equiv.ulift

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