inv — Mathlib

English

If x is close to r and not infinitesimal, then x^{-1} is close to r^{-1}.

Русский

Если x близко к r и не инфинитезимально, то x^{-1} близко к r^{-1}.

LaTeX

$$$ (\neg \operatorname{Infinitesimal}(x)) \land \operatorname{IsSt}(x, r) \Rightarrow \operatorname{IsSt}(x^{-1}, r^{-1}) $$$

Lean4

theorem inv {x : ℝ*} {r : ℝ} (hi : ¬Infinitesimal x) (hr : IsSt x r) : IsSt x⁻¹ r⁻¹ :=
  hr.map <| continuousAt_inv₀ <| by rintro rfl; exact hi hr

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