continuousAt_rpow_const — Mathlib

English

For any x in NNReal and any real y, if x ≠ 0 or y ≥ 0, then the map z ↦ z^y is continuous at x.

Русский

Для любого x в ℝ≥0 и любого вещественного y, если x ≠ 0 или y ≥ 0, отображение z ↦ z^y непрерывно в точке x.

LaTeX

$$$\\\\forall x \\in \\mathbb{R}_{\\ge 0}, \\\\forall y \\in \\mathbb{R}, \\\\ (x \\neq 0 \\lor y \\ge 0) \\\\Rightarrow \\\\text{ContinuousAt}(z \\mapsto z^y)~x$$$

Lean4

theorem continuousAt_rpow_const {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 ≤ y) : ContinuousAt (fun z => z ^ y) x :=
  h.elim (fun h => tendsto_id.nnrpow tendsto_const_nhds (Or.inl h)) fun h =>
    h.eq_or_lt.elim (fun h => h ▸ by simp only [rpow_zero, continuousAt_const]) fun h =>
      tendsto_id.nnrpow tendsto_const_nhds (Or.inr h)

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