continuousAt_const_cpow' — Mathlib

English

If h holds with p.fst ≠ 0, then the map (x,y) ↦ x^y is asymptotically exp(log x^fst · y) near p; i.e., the cpow expression converges to the exponential form around p.

Русский

Если p.fst ≠ 0, то около p отображение (x,y) ↦ x^y стремится к экспоненциальной форме exp(log x⋅y).

LaTeX

$$$$\\text{If } p=(x,y),\\ x\\neq 0,\\quad x^{\\,y} \\sim \\exp(\\log x \\cdot y) \\quad \\text{as } p\\to p.$$$$

Lean4

theorem continuousAt_const_cpow' {a b : ℂ} (h : b ≠ 0) : ContinuousAt (fun x : ℂ => a ^ x) b :=
  by
  by_cases ha : a = 0
  · rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]
    exact continuousAt_const
  · exact continuousAt_const_cpow ha

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