pow — Mathlib

English

Powers of analytic functions are analytic (pow form) for any natural exponent.

Русский

Степени аналитических функций аналитичны для любого натурального показателя в форме pow.

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 pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) : AnalyticAt 𝕜 (f ^ n) z :=
  AnalyticAt.fun_pow hf n

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