infinitesimal_def — Mathlib

English

An element x is infinitesimal iff it is smaller in absolute value than every positive real number.

Русский

Элемент x бесконечно малый тогда и только тогда, когда его модуль меньше любого положительного вещественного числа.

LaTeX

$$$\\forall {x : \\mathbb{R}^*}, \\ Infinitesimal(x) \\iff \\forall r \\in \\mathbb{R}, 0 < r \\rightarrow -(r : \\mathbb{R}^*) < x \\land x < r$$$

Lean4

theorem infinitesimal_def {x : ℝ*} : Infinitesimal x ↔ ∀ r : ℝ, 0 < r → -(r : ℝ*) < x ∧ x < r := by
  simp [Infinitesimal, IsSt]

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