wcovBy_add_one — Mathlib

English

In a suitable ordered additive structure, each element x is weakly covariantly covered by x + 1; that is, x < x+1 and there is no element strictly between.

Русский

В подходящей упорядоченной добавочной структуре каждый элемент x слабо покрывается x+1; то есть x < x+1 и не существует элемента z such that x < z < x+1.

LaTeX

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

Lean4

@[simp]
theorem wcovBy_add_one (x : α) : x ⩿ x + 1 := by
  rw [← succ_eq_add_one]
  exact wcovBy_succ x

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