self_le_succ_pred

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

o ≤ succ (pred o).

Русский

o ≤ succ(pred o).

LaTeX

$$$$ o \le \mathrm{succ}(\mathrm{pred}(o)) $$$$

Lean4

theorem self_le_succ_pred (o) : o ≤ succ (pred o) :=
  pred_succ_gi.gc.le_u_l o

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

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

Разделы

Аффилиация

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