tendsto_nhds_coe_iff — Mathlib

English

For any x ∈ NNReal, and f: ENNReal → α, Tendsto f (nhds (ENNReal.ofNNReal x)) l iff Tendsto (f ∘ ENNReal.ofNNReal) (nhds x) l.

Русский

Для любого x ∈ NNReal и f: ENNReal → α, сходимость f по nhds (ENNReal.ofNNReal x) равносильна сходимости f ∘ ENNReal.ofNNReal по nhds x.

LaTeX

$$$\\operatorname{Tendsto} f (\\mathcal{N}(\\mathrm{ENNReal}.ofNNReal x)) l \\iff \\operatorname{Tendsto} (f \\circ \\mathrm{ENNReal}.ofNNReal) (\\mathcal{N}(x)) l$$$

Lean4

theorem tendsto_nhds_coe_iff {α : Type*} {l : Filter α} {x : ℝ≥0} {f : ℝ≥0∞ → α} :
    Tendsto f (𝓝 ↑x) l ↔ Tendsto (f ∘ (↑) : ℝ≥0 → α) (𝓝 x) l := by rw [nhds_coe, tendsto_map'_iff]

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