zpow_nonneg — Mathlib

English

If a function f: E → 𝕝 is analytic at z and the exponent n is a nonnegative integer, then the function x ↦ f(x)^n is analytic at z.

Русский

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

LaTeX

$$$\mathrm{AnalyticAt}_{\mathbb{K}}(f,z) \land 0 \le n \Rightarrow \mathrm{AnalyticAt}_{\mathbb{K}}(x \mapsto f(x)^n, z)$$$

Lean4

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

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