English
Let p = (a,b) with a > 0 be a point in the plane. Then in a neighborhood of p the map (u,v) ↦ u^v agrees with the expression exp(v log u); i.e., x^y = exp(y log x) locally around p when the base is positive.
Русский
Пусть p = (a,b) с a > 0. В окрестности p отображение (u,v) ↦ u^v совпадает с выражением exp(v log u); то есть при положительной базе имеем локально u^v = exp(v log u).
LaTeX
$$$$\text{If } p=(a,b) \text{ with } a>0, \quad (x,y) \mapsto x^y =_{\mathcal{N}(p)} \exp(y\log x).$$$$
Lean4
theorem rpow_eq_nhds_of_pos {p : ℝ × ℝ} (hp_fst : 0 < p.fst) :
(fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
by
suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, 0 < x.1 from
this.mono fun x hx ↦ by
dsimp only
rw [rpow_def_of_pos hx]
exact IsOpen.eventually_mem (isOpen_lt continuous_const continuous_fst) hp_fst
