cpow — Mathlib

English

If f ⇢ a and g ⇢ b in a filter l, with a in slitPlane, then f(x)^g(x) tends to a^b along l.

Русский

Если f(x) → a и g(x) → b в фильтре l, при этом a ∈ slitPlane, то f(x)^{g(x)} стремится к a^{b} вдоль l.

LaTeX

$$$$\\text{If } f\\to a,\\ g\\to b\\text{ with } a\\in\\text{slitPlane},\\quad f^{g}\\to a^{b} \\text{ in the filter } l.$$$$

Lean4

theorem cpow {l : Filter α} {f g : α → ℂ} {a b : ℂ} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b))
    (ha : a ∈ slitPlane) : Tendsto (fun x => f x ^ g x) l (𝓝 (a ^ b)) :=
  (@continuousAt_cpow (a, b) ha).tendsto.comp (hf.prodMk_nhds hg)

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