add_one_le_iff — Mathlib

English

In any preorder with addition, one, and a successor operator, and with no maximal elements, we have x + 1 ≤ y ⇔ x < y for all x,y.

Русский

Во всяком порядке с операциями сложения и единицы и с операции successor, если максимум отсутствует, то для любых x,y выполняется x+1 ≤ y ⇔ x < y.

LaTeX

$$$\\\\forall x,y \\\\in \\\\alpha,\ [NoMaxOrder \\\\alpha] \\\\Rightarrow (x+1 \\\\le y \\\\iff x < y).$$$

Lean4

theorem add_one_le_iff [NoMaxOrder α] : x + 1 ≤ y ↔ x < y :=
  add_one_le_iff_of_not_isMax (not_isMax x)

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