analyticOn_inv — Mathlib

English

The reciprocal map is analytic on the set of nonzero elements, i.e., z ↦ z^{-1} is analytic on {z ≠ 0}.

Русский

Обратное отображение аналитично на множестве ненулевых элементов: z ↦ z^{-1} аналитично на {z ≠ 0}.

LaTeX

$$AnalyticOn 𝕜 (fun z ↦ z^{-1}) {z : 𝕝 | z ≠ 0}$$

Lean4

theorem analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} :=
  analyticOnNhd_inv.analyticOn

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