add_one_le_iff_of_not_isMax — Mathlib

English

Let α be a preorder with addition and a distinguished unit and a successor operation. If x is not maximal, then for every y we have x + 1 ≤ y if and only if x < y.

Русский

Пусть α — предчисляемый порядок с операциями сложения и единицы и с операцией преемника. Если x не максимален, то для произвольного y выполняется x + 1 ≤ y тогда и только тогда, когда x < y.

LaTeX

$$$\\\\forall x,y \\\\in \\\\alpha,\ \\\\neg \\\\IsMax x \\\\Rightarrow (x+1 \\le y \\\\iff x < y).$$$

Lean4

theorem add_one_le_iff_of_not_isMax (hx : ¬IsMax x) : x + 1 ≤ y ↔ x < y := by
  rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]

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