fun_pow — Mathlib

English

Powers of an analytic function are analytic within a set.

Русский

Степени аналитической функции аналитичны внутри множества.

LaTeX

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

Lean4

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
theorem fun_pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
  induction n with
  | zero =>
    simp only [pow_zero]
    apply analyticWithinAt_const
  | succ m hm =>
    simp only [pow_succ]
    exact hm.mul hf

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