pow — Mathlib

English

If f is analytic at z, then f^n is analytic at z for every natural n.

Русский

Если f аналитична в z, то f^n аналитична в z для каждого натурального 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. -/
theorem pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) : AnalyticWithinAt 𝕜 (f ^ n) s z :=
  AnalyticWithinAt.fun_pow hf n

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