infiniteNeg_iff_infinitesimal_inv_neg

English

For any x, InfiniteNeg x⁻¹ holds exactly when x is infinitesimal and x < 0; equivalently, the inverse of a negative infinitesimal is infinitely negative.

Русский

Для любого x, InfiniteNeg x⁻¹ эквивалентно Infinitesimal x и x < 0; обратная у отрицательной инфинитезимальной величины бесконечно малая.

LaTeX

$$$\operatorname{InfiniteNeg}(x^{-1}) \iff (\operatorname{Infinitesimal}(x) \land x < 0)$$$

Lean4

theorem infiniteNeg_iff_infinitesimal_inv_neg {x : ℝ*} : InfiniteNeg x ↔ Infinitesimal x⁻¹ ∧ x⁻¹ < 0 := by
  rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]

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