fun_inv — Mathlib

English

If f is analytic within a set and never vanishes on that set, then 1/f is analytic within that set.

Русский

Если f аналитична внутри множества и нигде не обращается в ноль, то 1/f аналитично внутри этого множества.

LaTeX

$$AnalyticWithinAt 𝕜 f^{−1} s x$$

Lean4

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem fun_inv {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x) (f0 : f x ≠ 0) :
    AnalyticWithinAt 𝕜 (fun x ↦ (f x)⁻¹) s x :=
  (analyticAt_inv f0).comp_analyticWithinAt fa

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