fun_pow — Mathlib

English

Powers of analytic functions are analytic (fun_pow form) for any n.

Русский

Степени аналитических функций аналитичны в любой форме (fun_pow) для любого n.

LaTeX

$$$\text{AnalyticAt}_{\mathbb{k}}(f,z) \Rightarrow \forall n, \text{AnalyticAt}_{\mathbb{k}}(f^n,z)$$$

Lean4

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
@[fun_prop]
theorem fun_pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) : AnalyticAt 𝕜 (fun x ↦ f x ^ n) z :=
  by
  rw [← analyticWithinAt_univ] at hf ⊢
  exact hf.pow n

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