succ — Mathlib

English

There is a successor function on the subcollection s of naturals, giving the least element of s strictly greater than each x in s.

Русский

Существует функция следующего элемента на подмножестве s натуральных чисел, которая даёт наименьший элемент в s, больший каждого x ∈ s.

LaTeX

$$$\forall x\in s,\ succ(x)\in s\ \land\ x < succ(x)$$$

Lean4

/-- Returns the next natural in a set, according to the usual ordering of `ℕ`. -/
def succ (x : s) : s :=
  have h : ∃ m, (x : ℕ) + m + 1 ∈ s := exists_succ x
  ⟨↑x + Nat.find h + 1, Nat.find_spec h⟩

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