rpow — Mathlib

English

If f → x and g → y with x ≠ 0 or y > 0, then f^g → x^y.

Русский

Если f тяготеет к x и g к y при условии x ≠ 0 или y > 0, то f^g → x^y.

LaTeX

$$$$\text{Tendsto } f\ l\ (l) \ (\,f\to x,\ g\to y\ )\Rightarrow \text{Tendsto } (t\mapsto f(t)^{g(t)})\ l\ (\nhds(x^y)),\text{ provided } x\neq 0\lor y>0.$$$$

Lean4

theorem rpow {l : Filter α} {f g : α → ℝ} {x y : ℝ} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y))
    (h : x ≠ 0 ∨ 0 < y) : Tendsto (fun t => f t ^ g t) l (𝓝 (x ^ y)) :=
  (Real.continuousAt_rpow (x, y) h).tendsto.comp (hf.prodMk_nhds hg)

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