English
Let p = (z,w) with z in slitPlane. The map (z,w) ↦ z^w is continuous at p.
Русский
Пусть p=(z,w) и z находится в slitPlane. Отображение (z,w) ↦ z^w непрерывно в p.
LaTeX
$$$$\\text{If } p=(z,w)\\text{ with } z \\in \\text{slitPlane},\\quad (z,w) \\mapsto z^{w} \\text{ is continuous at } p.$$$$
Lean4
/-- The function `z ^ w` is continuous in `(z, w)` provided that `z` does not belong to the interval
`(-∞, 0]` on the real line. See also `Complex.continuousAt_cpow_zero_of_re_pos` for a version that
works for `z = 0` but assumes `0 < re w`. -/
theorem continuousAt_cpow {p : ℂ × ℂ} (hp_fst : p.fst ∈ slitPlane) : ContinuousAt (fun x : ℂ × ℂ => x.1 ^ x.2) p :=
by
rw [continuousAt_congr (cpow_eq_nhds' <| slitPlane_ne_zero hp_fst)]
refine continuous_exp.continuousAt.comp ?_
exact
ContinuousAt.mul (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
continuous_snd.continuousAt
