pred_lt_iff_not_isSuccPrelimit

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

pred o < o iff not IsSuccPrelimit o.

Русский

pred o < o экв. не IsSuccPrelimit o.

LaTeX

$$$$ \mathrm{pred}(o) < o \iff \neg \mathrm{IsSuccPrelimit}(o) $$$$

Lean4

theorem pred_lt_iff_not_isSuccPrelimit {o} : pred o < o ↔ ¬IsSuccPrelimit o :=
  by
  rw [(pred_le_self o).lt_iff_ne]
  exact pred_eq_iff_isSuccPrelimit.not

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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