lt_add_one_iff — Mathlib

English

In a linear order with addition, there is an equivalence x < y + 1 if there is no max on y; specifically, x < y + 1 iff x ≤ y.

Русский

В линейном порядке с операцией сложения существует эквивалентность: x < y + 1 тогда и только тогда, когда x ≤ y, при условии отсутствия максимума у y.

LaTeX

$$$x < y + 1 \iff x \le y$$$

Lean4

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

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