instIsPredArchimedean — Mathlib

English

The natural numbers satisfy the PredArchimedean property: for any a ≤ b there exists k such that pred^[k](b) = a.

Русский

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

LaTeX

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

Lean4

instance : IsPredArchimedean ℕ :=
  ⟨fun {a} {b} h => ⟨b - a, by rw [pred_eq_pred, Nat.pred_iterate, tsub_tsub_cancel_of_le h]⟩⟩

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