instIsSuccArchimedean — Mathlib

English

The natural numbers carry a SuccArchimedean structure: for any a,b with a ≤ b, there exists k such that b = succ^[k](a).

Русский

Натуральные числа обладают SuccArchimedean структурой: для любых a ≤ b существует k такое, что b = succ^[k](a).

LaTeX

$$$\\\\forall a,b \\\\in \\\\mathbb N, \\\\ a \\\\le \\\\ b \\\\Rightarrow \\\\exists k \\\\in \\\\mathbb N, \\\\operatorname{succ}^{[k]}(a) = b.$$$

Lean4

instance : IsSuccArchimedean ℕ :=
  ⟨fun {a} {b} h => ⟨b - a, by rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]⟩⟩

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