ofReal_map_toNNReal — Mathlib

English

If f: NNReal → NNReal is continuous on t and s maps under Real.toNNReal into t, then the Real-valued map x ↦ f(x.toNNReal) is continuous on s.

Русский

Если f: NNReal → NNReal непрерывно на t и s отображается через Real.toNNReal в t, тогда отображение x ↦ f(x.toNNReal) непрерывно на s.

LaTeX

$$$ContinuousOn (\\lambda x, f(x.toNNReal))\ \text{ on } s$$$

Lean4

theorem _root_.ContinuousOn.ofReal_map_toNNReal {f : ℝ≥0 → ℝ≥0} {s : Set ℝ} {t : Set ℝ≥0} (hf : ContinuousOn f t)
    (h : Set.MapsTo Real.toNNReal s t) : ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) s :=
  continuous_subtype_val.comp_continuousOn <| hf.comp continuous_real_toNNReal.continuousOn h

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