fun_inv — Mathlib

English

For HasSummableGeomSeries, the reciprocal map is analytic on a neighborhood of the unit set.

Русский

При условии HasSummableGeomSeries отображение обратной функции аналитично на окрестности множества единиц.

LaTeX

$$AnalyticOnNhd 𝕜 Ring.inverse {x : A | IsUnit x}$$

Lean4

/-- `(f x)⁻¹` is analytic away from `f x = 0` -/
theorem fun_inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOnNhd 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) :
    AnalyticOnNhd 𝕜 (fun x ↦ (f x)⁻¹) s := fun x m ↦ (fa x m).inv (f0 x m)

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