English
For p = (a,b) with a ≠ 0, the map (x,y) ↦ x^y is approximately exp((log x)·y) near p; i.e., (x^y) ≈ exp(log x · y) as (x,y) → p.
Русский
Для p = (a,b) с a ≠ 0 местами (x,y) ↦ x^y близко к exp((log x)·y) при (x,y) → p.
LaTeX
$$$$\\text{If } p=(a,b)\\text{ with } a \\neq 0,\\quad (x,y) \\mapsto x^{y} \\sim \\exp(\\log x \\cdot y) \\text{ as } (x,y) \\to p.$$$$
Lean4
theorem cpow_eq_nhds' {p : ℂ × ℂ} (hp_fst : p.fst ≠ 0) : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
by
suffices ∀ᶠ x : ℂ × ℂ in 𝓝 p, x.1 ≠ 0 from
this.mono fun x hx ↦ by
dsimp only
rw [cpow_def_of_ne_zero hx]
refine IsOpen.eventually_mem ?_ hp_fst
change IsOpen {x : ℂ × ℂ | x.1 = 0}ᶜ
rw [isOpen_compl_iff]
exact isClosed_eq continuous_fst continuous_const
