English
For p = (z,w) with either Re(z) ≥ 0 or Im(z) ≠ 0 and Re(w) > 0, the map (z,w) ↦ z^w is continuous at p.
Русский
Для p=(z,w) с (Re(z) ≥ 0 или Im(z) ≠ 0) и Re(w) > 0 отображение (z,w) ↦ z^w непрерывно в p.
LaTeX
$$$$\forall p=(z,w)\in\mathbb{C}^2,\ (\Re(z) \ge 0 \lor \Im(z) \neq 0) \land \Re(w) > 0 \Rightarrow \text{ContinuousAt}( (z,w)\mapsto z^w )\, p.$$$$
Lean4
/-- See also `continuousAt_cpow` for a version that assumes `p.1 ≠ 0` but makes no
assumptions about `p.2`. -/
theorem continuousAt_cpow_of_re_pos {p : ℂ × ℂ} (h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0) (h₂ : 0 < p.2.re) :
ContinuousAt (fun x : ℂ × ℂ => x.1 ^ x.2) p :=
by
obtain ⟨z, w⟩ := p
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne, Classical.not_not, not_le_zero_iff] at h₁
rcases h₁ with (h₁ | (rfl : z = 0))
exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]
