rpow_const — Mathlib

English

If f → x and x ≠ 0 or p ≤ 0, then f^p → x^p as a function of the parameter p.

Русский

Если f → x и (x ≠ 0 или p ≤ 0), тогда f^p → x^p при фиксированном p.

LaTeX

$$$$\text{Tendsto } f\ l\ (nhds\ x) \Rightarrow (x\neq 0 \lor p\le 0) \Rightarrow \text{Tendsto } (a\mapsto f(a)^p)\ l\ (nhds(x^p)).$$$$

Lean4

theorem rpow_const {l : Filter α} {f : α → ℝ} {x p : ℝ} (hf : Tendsto f l (𝓝 x)) (h : x ≠ 0 ∨ 0 ≤ p) :
    Tendsto (fun a => f a ^ p) l (𝓝 (x ^ p)) :=
  if h0 : 0 = p then h0 ▸ by simp [tendsto_const_nhds]
  else hf.rpow tendsto_const_nhds (h.imp id fun h' => h'.lt_of_ne h0)

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