lt_neg_of_pos_of_infinitesimal — Mathlib

English

If x is infinitesimal, then for any positive real r, −r < x.

Русский

Если x бесконечно мал, то для любого положительного вещественного r выполняется −r < x.

LaTeX

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

Lean4

theorem lt_neg_of_pos_of_infinitesimal {x : ℝ*} : Infinitesimal x → ∀ r : ℝ, 0 < r → -↑r < x := fun hi r hr =>
  ((infinitesimal_def.mp hi) r hr).1

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