lt_add_one_iff_of_not_isMax

Mathlib.Algebra.Order.SuccPred

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

English

If y is not a maximal element, then x < y + 1 is equivalent to x ≤ y.

Русский

Если y не является максимальным элементом, то x < y + 1 эквивалентно x ≤ y.

LaTeX

$$$\neg \mathrm{IsMax}(y) \Rightarrow (x < y + 1 \iff x \le y)$$$

Lean4

theorem lt_add_one_iff_of_not_isMax (hy : ¬IsMax y) : x < y + 1 ↔ x ≤ y := by
  rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]

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

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

Разделы

Аффилиация

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