ennrpow_const — Mathlib

English

If m converges to a in ENNReal, then x ↦ m(x)^r converges to a^r under appropriate conditions.

Русский

Если m сходится к a в ENNReal, то x ↦ m(x)^r сходится к a^r при подходящих условиях.

LaTeX

$$$\\\\forall {m: A \\to \\mathbb{R}_{\\ge 0\\infty}}, \\\\text{Tendsto } m f (\\\\nhds a) \\\\Rightarrow \\\\text{Tendsto } (x \\mapsto m x)^r f (\\\\nhds (a^r))$$$

Lean4

theorem ennrpow_const {α : Type*} {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} (r : ℝ) (hm : Tendsto m f (𝓝 a)) :
    Tendsto (fun x => m x ^ r) f (𝓝 (a ^ r)) :=
  (ENNReal.continuous_rpow_const.tendsto a).comp hm

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