pred_eq_of_isSuccPrelimit

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

pred o = o iff o is a succ-prelimit.

Русский

pred o = o тогда и только тогда, когда o является succ-prelimit.

LaTeX

$$$$ \mathrm{pred}(o) = o \iff \mathrm{IsSuccPrelimit}(o) $$$$

Lean4

theorem pred_eq_of_isSuccPrelimit {o} : IsSuccPrelimit o → pred o = o :=
  isSuccPrelimitRecOn_of_isSuccPrelimit _ _

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

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

Разделы

Аффилиация

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