lt_of_pos_of_infinitesimal — Mathlib

English

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

Русский

Если x бесконечно мал, то x меньше любого положительного вещественного числа.

LaTeX

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

Lean4

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

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