continuousAt_cpow_const — Mathlib

English

If the first component lies in the slit plane, the map (z,w) ↦ z^w is continuous at that point.

Русский

Если первая компонента принадлежит slitPlane, отображение (z,w) ↦ z^w непрерывно в этой точке.

LaTeX

$$$$\\text{If } p=(z,w) \\text{ with } z \\in \\text{slitPlane},\\quad \\text{ContinuousAt}(\\lambda (z,w)\\, , z^w)\\text{ at } p.$$$$

Lean4

theorem continuousAt_cpow_const {a b : ℂ} (ha : a ∈ slitPlane) : ContinuousAt (· ^ b) a :=
  Tendsto.comp (@continuousAt_cpow (a, b) ha) (continuousAt_id.prodMk continuousAt_const)

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