isSuccPrelimit_lift

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.isSuccPrelimit_lift

English

IsSuccLimit is preserved by lifting: IsSuccLimit(lift(o)) iff IsSuccLimit(o).

Русский

Предел суктора сохраняется при подъёме: IsSuccLimit(lift(o)) ⇔ IsSuccLimit(o).

LaTeX

$$$\forall o, IsSuccLimit(\mathrm{lift}(o)) \iff IsSuccLimit(o)$$$

Lean4

@[simp]
theorem isSuccPrelimit_lift {o : Ordinal} : IsSuccPrelimit (lift.{u, v} o) ↔ IsSuccPrelimit o :=
  liftInitialSeg.isSuccPrelimit_apply_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru