sub_one_lt_iff

Mathlib.Algebra.Order.SuccPred

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

English

If NoMinOrder holds, then x − 1 < y iff x ≤ y.

Русский

Если выполняется условие NoMinOrder, то x − 1 < y эквивално x ≤ y.

LaTeX

$$$x - 1 < y \iff x \le y \quad [NoMinOrder(\alpha)]$$$

Lean4

theorem sub_one_lt_iff [NoMinOrder α] : x - 1 < y ↔ x ≤ y :=
  sub_one_lt_iff_of_not_isMin (not_isMin x)

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

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

Разделы

Аффилиация

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