continuousAt_rpow — Mathlib

English

For p = (a,b), if either a ≠ 0 or b > 0, the map (a,b) ↦ a^b is continuous at p.

Русский

Для p = (a,b), если либо a ≠ 0, либо b > 0, отображение (a,b) ↦ a^b непрерывно в p.

LaTeX

$$$$\forall p=(a,b)\in\mathbb{R}^2,\ a\neq 0 \lor b>0 \Rightarrow \text{ContinuousAt}((a,b)\mapsto a^b)\,p.$$$$

Lean4

theorem continuousAt_rpow (p : ℝ × ℝ) (h : p.1 ≠ 0 ∨ 0 < p.2) : ContinuousAt (fun p : ℝ × ℝ => p.1 ^ p.2) p :=
  h.elim (fun h => continuousAt_rpow_of_ne p h) fun h => continuousAt_rpow_of_pos p h

Похожие утверждения