infinitesimal_pos_iff_infinitePos_inv

English

Inverse relation: InfinitePos x⁻¹ iff Infinitesimal x and 0 < x⁻¹.

Русский

Инверсия: InfinitePos x⁻¹ эквивалентно Infinitesimal x и 0 < x⁻¹.

LaTeX

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

Lean4

theorem infinitesimal_pos_iff_infinitePos_inv {x : ℝ*} : InfinitePos x⁻¹ ↔ Infinitesimal x ∧ 0 < x :=
  infinitePos_iff_infinitesimal_inv_pos.trans <| by rw [inv_inv]

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