continuousOn_rpow_const — Mathlib

English

For any real r and any set s ⊆ ℝ≥0, if 0 ∉ s or r ≥ 0, then z^r is continuous on s.

Русский

Для любого вещественного r и любого множества s ⊆ ℝ≥0, если 0 ∉ s или r ≥ 0, то z^r непрерывна на s.

LaTeX

$$$\\\\forall r \\in \\mathbb{R}, \\; \\forall s \\subseteq \\mathbb{R}_{\\ge 0}, \\\\bigl(0 \\notin s \\lor r \\ge 0\\bigr) \\Rightarrow \\text{ContinuousOn}(z \\mapsto z^r)\\, s$$

Lean4

@[fun_prop]
theorem continuousOn_rpow_const {r : ℝ} {s : Set ℝ≥0} (h : 0 ∉ s ∨ 0 ≤ r) : ContinuousOn (fun z : ℝ≥0 => z ^ r) s :=
  h.elim (fun _ ↦ ContinuousOn.mono (s := {0}ᶜ) (by fun_prop) (by simp_all))
    (NNReal.continuous_rpow_const · |>.continuousOn)

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