covBy_add_one — Mathlib

English

For a NoMaxOrder α with addition, one, and successor, x is covered by x+1; i.e., x < x+1 and there is no element between.

Русский

Для порядка без максимума α с операциями сложения и преемника x покрывается x+1; то есть x < x+1 и между ними нет элемента.

LaTeX

$$$\\\\forall x \\\\in \\\\alpha,\quad x < x+1 \\\\land\\\\ \\\\nexists z (x < z \\\\land z < x+1).$$$

Lean4

@[simp]
theorem covBy_add_one [NoMaxOrder α] (x : α) : x ⋖ x + 1 :=
  by
  rw [← succ_eq_add_one]
  exact covBy_succ x

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