English
An element x is infinitesimal iff |x| is smaller than |r| for every nonzero real r.
Русский
Элемент x бесконечно малый тогда и только тогда, когда |x| < |r| для каждого не нулевого вещественного r.
LaTeX
$$$\\forall {x : \\mathbb{R}^*}, \\ Infinitesimal(x) \\iff \\forall r \\in \\mathbb{R}, r \\neq 0 \\rightarrow |x| < |r|$$$
Lean4
theorem abs_lt_real_iff_infinitesimal {x : ℝ*} : Infinitesimal x ↔ ∀ r : ℝ, r ≠ 0 → |x| < |↑r| :=
⟨fun hi r hr ↦ abs_lt.mpr (coe_abs r ▸ infinitesimal_def.mp hi |r| (abs_pos.2 hr)), fun hR ↦
infinitesimal_def.mpr fun r hr => abs_lt.mp <| (abs_of_pos <| coe_pos.2 hr) ▸ hR r <| hr.ne'⟩