inv₀ — Mathlib

English

If f is continuous within a set s at a point a and f(a) ≠ 0, then the map x ↦ (f(x))⁻¹ is continuous within s at a.

Русский

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

LaTeX

$$ContinuousWithinAt f s a → f a ≠ 0 → ContinuousWithinAt (\\λ x, f(x)^{-1}) s a$$

Lean4

nonrec theorem inv₀ (hf : ContinuousWithinAt f s a) (ha : f a ≠ 0) : ContinuousWithinAt (fun x => (f x)⁻¹) s a :=
  hf.inv₀ ha

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