tendsto_toNNReal — Mathlib

English

For a ∈ ENNReal with a ≠ ∞ and f: α → ENNReal with f x ≠ ∞ for all x, Tendsto (ENNReal.toNNReal ∘ f) u (nhds a.toNNReal) iff Tendsto f u (nhds a).

Русский

Пусть a ∈ ENNReal, a ≠ ∞ и f: α → ENNReal с f x ≠ ∞; тогда Tendsto (toNNReal ∘ f) у (nhds a.toNNReal) эквивалентно Tendsto f у (nhds a).

LaTeX

$$$\\operatorname{Tendsto} (\\mathrm{ENNReal}.toNNReal \\circ f) u (\\mathcal{N}(a.toNNReal)) \iff \\operatorname{Tendsto} f u (\\mathcal{N}(a))$$$

Lean4

theorem tendsto_toNNReal {a : ℝ≥0∞} (ha : a ≠ ∞) : Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 a.toNNReal) :=
  by
  lift a to ℝ≥0 using ha
  rw [nhds_coe, tendsto_map'_iff]
  exact tendsto_id

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