lt_succ_iff_eq_or_lt

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.lt_succ_iff_eq_or_lt

English

Assuming no maximal elements, a < succ(b) iff a = b or a < b.

Русский

При отсутствии максимума: a < succ(b) тогда и только если a = b или a < b.

LaTeX

$$$\text{[NoMaxOrder]} \Rightarrow a < \operatorname{succ} b \iff a = b \lor a < b$$$

Lean4

theorem lt_succ_iff_eq_or_lt : a < succ b ↔ a = b ∨ a < b :=
  lt_succ_iff.trans le_iff_eq_or_lt

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

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

Разделы

Аффилиация

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