infinitesimal_neg_iff_infiniteNeg_inv

English

Infinitesimal numbers preserve sign under inversion: the negation of an infinitesimal is infinitesimal, and so forth.

Русский

Инфинитезимальные сохраняют знак при инверсии и т.д.

LaTeX

$$$\operatorname{Infinitesimal}(x) \Rightarrow \operatorname{Infinitesimal}(-x)$$$

Lean4

theorem infinitesimal_neg_iff_infiniteNeg_inv {x : ℝ*} : InfiniteNeg x⁻¹ ↔ Infinitesimal x ∧ x < 0 :=
  infiniteNeg_iff_infinitesimal_inv_neg.trans <| by rw [inv_inv]

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