const_cpow — Mathlib

English

If a ≠ 0 or b ≠ 0, then Tendsto a^{f(x)} to a^{b} whenever f(x) → b.

Русский

Если a ≠ 0 или b ≠ 0, то при f(x) → b имеем стремление a^{f(x)} → a^{b}.

LaTeX

$$$$\\text{Let } a,b \\in \\mathbb{C},\\ ha:\\mathrm{Tendsto} f \\ l\\to b.\\quad \\text{Then } a^{f(x)} \\to a^{b}. $$$$

Lean4

theorem const_cpow {l : Filter α} {f : α → ℂ} {a b : ℂ} (hf : Tendsto f l (𝓝 b)) (h : a ≠ 0 ∨ b ≠ 0) :
    Tendsto (fun x => a ^ f x) l (𝓝 (a ^ b)) := by
  cases h with
  | inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
  | inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf

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