infinite_of_infinitesimal_inv — Mathlib

English

Integral reciprocity: infinitesimal and infinite are reciprocals.

Русский

Кратно-инфинициалы и бесконечности взаимно обратны.

LaTeX

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

Lean4

theorem infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : Infinitesimal x⁻¹) : Infinite x :=
  by
  rcases lt_or_gt_of_ne h0 with hn | hp
  · exact Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)
  · exact Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)

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