infinitesimal_inv_of_infinite — Mathlib

English

If x is Infinite, then x⁻¹ is Infinitesimal; if x is InfiniteNeg, then x⁻¹ is Infinitesimal as well.

Русский

Если x бесконечно велико, то x⁻¹ инфинитезимальна; то же верно для InfiniteNeg.

LaTeX

$$$\operatorname{Infinite}(x) \Rightarrow \operatorname{Infinitesimal}(x^{-1})$$$

Lean4

theorem infinitesimal_inv_of_infinite {x : ℝ*} : Infinite x → Infinitesimal x⁻¹ := fun hi =>
  Or.casesOn hi (fun hip => (infinitePos_iff_infinitesimal_inv_pos.mp hip).1) fun hin =>
    (infiniteNeg_iff_infinitesimal_inv_neg.mp hin).1

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