pred_lt_iff_eq_or_lt

Mathlib.Order.SuccPred.Basic

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

English

For all a,b with PredOrder, pred a < b if and only if a = b or a < b.

Русский

Для любых a,b с PredOrder: pred a < b эквивалентно a = b или a < b.

LaTeX

$$$ pred\\ a < b \\iff a = b \\lor a < b $$$

Lean4

theorem pred_lt_iff_eq_or_lt : pred a < b ↔ a = b ∨ a < b :=
  pred_lt_iff.trans le_iff_eq_or_lt

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

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

Разделы

Аффилиация

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