inv₀ — Mathlib

English

If f is continuous at a and f(a) ≠ 0, then the inverse function x ↦ f(x)⁻¹ is continuous at a.

Русский

Если функция f непрерывна в точке a и f(a) ≠ 0, то отображение x ↦ f(x)⁻¹ непрерывно в точке a.

LaTeX

$$ContinuousAt f a → Ne (f a) 0 → ContinuousAt (\\lambda x, f(x)^{-1}) a$$

Lean4

@[fun_prop]
nonrec theorem inv₀ (hf : ContinuousAt f a) (ha : f a ≠ 0) : ContinuousAt (fun x => (f x)⁻¹) a :=
  hf.inv₀ ha

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