instIsSuccArchimedean — Mathlib

English

The integers are succ-Archimedean: for all a ≤ b, there exists n ∈ ℕ with a + n ≥ b; in fact n = b − a works (so a + (b − a) = b).

Русский

Целые числа обладают свойством succ-архимедова: для всех a ≤ b существует n ∈ ℕ такое, что a + n ≥ b; на самом деле n = b − a работает (здесь a + (b − a) = b).

LaTeX

$$$\forall a,b \in \mathbb{Z},\; a \le b \rightarrow \exists n \in \mathbb{N},\; a + n \ge b$$$

Lean4

instance : IsSuccArchimedean ℤ :=
  ⟨fun {a b} h => ⟨(b - a).toNat, by rw [succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel_left]⟩⟩

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