zpow_nonneg — Mathlib

English

If a function f: E → 𝕝 is analytic on s, and the exponent n is nonnegative, then f^n is analytic on s.

Русский

Если функция f: E → 𝕝 аналитична на s, и показатель степени n неотрицателен, то f^n аналитична на s.

LaTeX

$$$\mathrm{AnalyticOn}_{\mathbb{K}}(f,s) \land 0 \le n \Rightarrow \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 : AnalyticOn 𝕜 f s) (hn : 0 ≤ n) : AnalyticOn 𝕜 (f ^ n) s :=
  fun_zpow_nonneg hf hn

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