English
For x ∈ ℝ≥0 and y ∈ ℝ, if x ≠ 0 or y > 0 then (x,y) ↦ x^y is continuous at (x,y) in NNReal sense.
Русский
Для x ∈ ℝ≥0 и y ∈ ℝ, если x ≠ 0 или y > 0, то (x,y) ↦ x^y непрерывно в NNReal-чередовании.
LaTeX
$$$$\forall x:\mathbb{R}_{\ge 0},\forall y:\mathbb{R},\ (x\neq 0 \lor y>0) \Rightarrow \text{ContinuousAt}( (p: \mathbb{R}_{\ge 0}\times\mathbb{R})\mapsto p.1^p.2 )\,(x,y).$$$$
Lean4
theorem continuousAt_rpow {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 < y) : ContinuousAt (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) (x, y) :=
by
have :
(fun p : ℝ≥0 × ℝ => p.1 ^ p.2) = Real.toNNReal ∘ (fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun p : ℝ≥0 × ℝ => (p.1.1, p.2) :=
by
ext p
simp only [coe_rpow, val_eq_coe, Function.comp_apply, coe_toNNReal', left_eq_sup]
exact_mod_cast zero_le (p.1 ^ p.2)
rw [this]
refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)
· apply Real.continuousAt_rpow
simpa using h
· fun_prop
