lt_pred_iff_succ_lt

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

a < pred b iff succ a < b.

Русский

a < pred b экв. succ a < b.

LaTeX

$$$$ a < \mathrm{pred}(b) \iff \mathrm{succ}(a) < b $$$$

Lean4

@[simp]
theorem lt_pred_iff_succ_lt {a b} : a < pred b ↔ succ a < b :=
  le_iff_le_iff_lt_iff_lt.1 pred_le_iff_le_succ

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

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

Разделы

Аффилиация

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