instIsPredArchimedean — Mathlib

English

The integers are pred-Archimedean: for all a ≤ b, there exists n ∈ ℕ with b ≤ a + n.

Русский

Целые числа являются пред-архимедовыми: для любых a ≤ b существует n ∈ ℕ такое, что b ≤ a + n.

LaTeX

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

Lean4

instance : IsPredArchimedean ℤ :=
  ⟨fun {a b} h => ⟨(b - a).toNat, by rw [pred_iterate, toNat_sub_of_le h, sub_sub_cancel]⟩⟩

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