zpow_nonneg — Mathlib

English

If a function f is analytic on 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{AnalyticOnNhd}_{\mathbb{K}}(f,s) \Rightarrow \forall n \in \mathbb{N}, \mathrm{AnalyticOn}_{\mathbb{K}}(x \mapsto f(x)^n, s)$$$

Lean4

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
theorem zpow_nonneg {f : E → 𝕝} {s : Set E} {n : ℤ} (hf : AnalyticOnNhd 𝕜 f s) (hn : 0 ≤ n) :
    AnalyticOnNhd 𝕜 (f ^ n) s :=
  fun_zpow_nonneg hf hn

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