lift_id' — Mathlib

English

An ordinal lifted to a smaller or equal universe is equal to itself.

Русский

Ординал, поднятый в меньшую или равную вселенную, равен самому себе.

LaTeX

$$$\\mathrm{lift}_{U}(a) = a$ for a in Ordinal when lifting to a smaller or equal universe.$$

Lean4

/-- An ordinal lifted to a lower or equal universe equals itself.

Unfortunately, the simp lemma doesn't work. -/
theorem lift_id' (a : Ordinal) : lift a = a :=
  inductionOn a fun _ r _ => Quotient.sound ⟨RelIso.preimage Equiv.ulift r⟩

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