English
If p = (a,b) with b > 0, then the map (a,b) ↦ a^b is continuous at p.
Русский
Если p = (a,b) с b > 0, то отображение (a,b) ↦ a^b непрерывно в точке p.
LaTeX
$$$$\forall p=(a,b)\in\mathbb{R}^2,\ b>0 \Rightarrow \text{ContinuousAt}((a,b)\mapsto a^b)\,p.$$$$
Lean4
theorem continuousAt_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.2) : ContinuousAt (fun p : ℝ × ℝ => p.1 ^ p.2) p :=
by
obtain ⟨x, y⟩ := p
dsimp only at hp
obtain hx | rfl := ne_or_eq x 0
· exact continuousAt_rpow_of_ne (x, y) hx
have A : Tendsto (fun p : ℝ × ℝ => exp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
tendsto_exp_atBot.comp ((tendsto_log_nhdsNE_zero.comp tendsto_fst).atBot_mul_pos hp tendsto_snd)
have B : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
squeeze_zero_norm (fun p => abs_rpow_le_exp_log_mul p.1 p.2) A
have C : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0) :=
by
rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'
simpa only [← sup_prod, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ, nhds_prod_eq, ContinuousAt,
zero_rpow hp.ne'] using B.sup (C.mono_right (pure_le_nhds _))
