tendsto_ofReal — Mathlib

English

If m: α → ℝ tends to a under f, then ENNReal.ofReal ∘ m tends to ENNReal.ofReal a under f.

Русский

Если m: α → ℝ стремится к a по f, то ENNReal.ofReal ∘ m стремится к ENNReal.ofReal a по f.

LaTeX

$$$\\operatorname{Tendsto}(\\mathrm{ENNReal}.ofReal \\circ m) f (\\mathcal{N}(\\mathrm{ENNReal}.ofReal(a))) \\;\\text{from } \\operatorname{Tendsto} m f (\\mathcal{N}(a))$$$

Lean4

theorem tendsto_ofReal {f : Filter α} {m : α → ℝ} {a : ℝ} (h : Tendsto m f (𝓝 a)) :
    Tendsto (fun a => ENNReal.ofReal (m a)) f (𝓝 (ENNReal.ofReal a)) :=
  (continuous_ofReal.tendsto a).comp h

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