English
If p = (a,b) with a ≠ 0, then the map (a,b) ↦ a^b is continuous at p.
Русский
Если p = (a,b) с a ≠ 0, отображение (a,b) ↦ a^b непрерывно в точке p.
LaTeX
$$$$\forall p=(a,b)\in\mathbb{R}^2,\ a\neq 0 \Rightarrow \text{ContinuousAt}((a,b)\mapsto a^b)\,p.$$$$
Lean4
theorem continuousAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) : ContinuousAt (fun p : ℝ × ℝ => p.1 ^ p.2) p :=
by
rw [ne_iff_lt_or_gt] at hp
cases hp with
| inl hp =>
rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
refine ContinuousAt.mul ?_ (continuous_cos.continuousAt.comp ?_)
· refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
refine (continuousAt_log ?_).comp continuous_fst.continuousAt
exact hp.ne
· exact continuous_snd.continuousAt.mul continuousAt_const
| inr hp =>
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
refine (continuousAt_log ?_).comp continuous_fst.continuousAt
exact hp.ne'
