analyticAt_inv_one_sub — Mathlib

English

For 𝕜 and 𝕝 nontrivially normed fields with a normed algebra structure, the map x ↦ (1−x)^{-1} is analytic at 0.

Русский

Для ненулевых нормированных полей 𝕜 и 𝕝 с нормированной алгеброй отображение x ↦ (1−x)^{-1} аналитично в точке 0.

LaTeX

$$$\operatorname{AnalyticAt} 𝕜 (\lambda x, (1-x)^{-1}) 0$$$

Lean4

@[fun_prop]
theorem analyticAt_inv_one_sub (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
    AnalyticAt 𝕜 (fun x : 𝕝 ↦ (1 - x)⁻¹) 0 :=
  ⟨_, ⟨_, hasFPowerSeriesOnBall_inv_one_sub 𝕜 𝕝⟩⟩

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