abs_lt_real_iff_infinitesimal — Mathlib

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'⟩

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