continuousOn_rpow_const_compl_zero

English

For every real r, the map z ↦ z^r is continuous on the set ℝ≥0 \ {0}.

Русский

Для любого действительного r отображение z ↦ z^r непрерывно на множестве ℝ≥0 \ {0}.

LaTeX

$$$\\\\forall r \\in \\mathbb{R}, \\\\text{ContinuousOn}(z \\mapsto z^r) \\\\bigl(\\mathbb{R}_{\\ge 0} \\setminus \\{0\\}\\bigr)$$$

Lean4

@[fun_prop]
theorem continuousOn_rpow_const_compl_zero {r : ℝ} : ContinuousOn (fun z : ℝ≥0 => z ^ r) {0}ᶜ := fun _ h =>
  ContinuousAt.continuousWithinAt <|
    NNReal.continuousAt_rpow_const
      (.inl h)
        -- even though this follows from `ContinuousOn.mono` and the previous lemma, we include it for
        -- automation purposes with `fun_prop`, because the side goal `0 ∉ s ∨ 0 ≤ r` is often easy to check

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