continuousAt_const_cpow — Mathlib

English

Fix a ≠ 0; the map z ↦ z^b is continuous at any b in the exponent when considering base a; equivalently, z ↦ a^z is continuous at z = b.

Русский

Пусть a ≠ 0; отображение z ↦ z^b непрерывно в точке z = b при основании a, т.е. a^z непрерывно по z в точке b.

LaTeX

$$$$\\text{If } a \\neq 0,\\quad z \\mapsto z^{b} \\text{ is continuous at } z=a.$$$$

Lean4

theorem continuousAt_const_cpow {a b : ℂ} (ha : a ≠ 0) : ContinuousAt (fun x : ℂ => a ^ x) b :=
  by
  have cpow_eq : (fun x : ℂ => a ^ x) = fun x => exp (log a * x) :=
    by
    ext1 b
    rw [cpow_def_of_ne_zero ha]
  rw [cpow_eq]
  exact continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)

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