tendsto_toNNReal_iff — Mathlib

English

If f: α → ENNReal has f x ≠ ∞ for all x, then Tendsto (ENNReal.toNNReal ∘ f) u (nhds a) iff Tendsto f u (nhds a) for a ∈ NNReal.

Русский

Если f: α → ENNReal таково, что f x ≠ ∞ для всех x, то Tendsto (toNNReal ∘ f) к a эквивалентно Tendsto f к a, когда a ∈ NNReal.

LaTeX

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

Lean4

theorem tendsto_toNNReal_iff {f : α → ℝ≥0∞} {u : Filter α} (ha : a ≠ ∞) (hf : ∀ x, f x ≠ ∞) :
    Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (a.toNNReal)) ↔ Tendsto f u (𝓝 a) :=
  by
  refine ⟨fun h => ?_, fun h => (ENNReal.tendsto_toNNReal ha).comp h⟩
  rw [← coe_comp_toNNReal_comp hf]
  exact (tendsto_coe_toNNReal ha).comp h

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