instArchimedean — Mathlib

English

For every real number x there exists a natural number n with x ≤ n.

Русский

Для любого вещественного числа x существует натуральное число n такое, что x ≤ n.

LaTeX

$$$\forall x \in \mathbb{R},\; \exists n \in \mathbb{N},\; x \le n$$$

Lean4

instance instArchimedean : Archimedean ℝ :=
  archimedean_iff_rat_le.2 fun x =>
    Real.ind_mk x fun f =>
      let ⟨M, _, H⟩ := f.bounded' 0
      ⟨M, mk_le_of_forall_le ⟨0, fun i _ => Rat.cast_le.2 <| le_of_lt (abs_lt.1 (H i)).2⟩⟩

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