fun_pow — Mathlib

English

If a function f is analytic on a set s, then for every natural number n the function x ↦ f(x)^n is analytic on s.

Русский

Если функция f аналитична на множестве s, то для каждого натурального числа n функция x ↦ f(x)^n аналитична на s.

LaTeX

$$$\mathrm{AnalyticOn}_{\mathbb{K}}(f,s) \Rightarrow \forall n \in \mathbb{N}, \mathrm{AnalyticOn}_{\mathbb{K}}(x \mapsto f(x)^n, s)$$$

Lean4

/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
theorem fun_pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) : AnalyticOn 𝕜 (fun x ↦ f x ^ n) s := fun _ m ↦
  (hf _ m).pow n

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