English
Let u and v be indexable nets in α with u → x in ℝ≥0 and v → y in ℝ, where x ≥ 0 and y ∈ ℝ. If x ≠ 0 or y > 0, then u^v converges to x^y.
Русский
Пусть u : α → ℝ≥0 и v : α → ℝ удовлетворяют u a → x и v a → y соответственно, где x ≥ 0, y ∈ ℝ. При условии x ≠ 0 или y > 0, получится, что u^v → x^y.
LaTeX
$$$\\\\text{Let } u: A \\to \\mathbb{R}_{\\ge 0}, \\ v: A \\to \\mathbb{R}, \\ x \\in \\mathbb{R}_{\\ge 0}, \\ y \\in \\mathbb{R} \\\\text{and } f:\\ A \\to A \\text{ a filter so that } u \\xrightarrow{f} x, v \\xrightarrow{f} y, \\\\text{and } x \\neq 0 \\lor 0 < y. \\\\Then \\\\; (a \\mapsto u(a)^{v(a)}) \\xrightarrow{f} x^{y}. $$$
Lean4
theorem nnrpow {α : Type*} {f : Filter α} {u : α → ℝ≥0} {v : α → ℝ} {x : ℝ≥0} {y : ℝ} (hx : Tendsto u f (𝓝 x))
(hy : Tendsto v f (𝓝 y)) (h : x ≠ 0 ∨ 0 < y) : Tendsto (fun a => u a ^ v a) f (𝓝 (x ^ y)) :=
Tendsto.comp (NNReal.continuousAt_rpow h) (hx.prodMk_nhds hy)
