tendsto_coe_ennreal — Mathlib

English

The inclusion ℝ≥0∞ → EReal preserves convergence: Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a).

Русский

Включение ℝ≥0∞ в EReal сохраняет сходимость: Tendsto (m a : EReal) ↔ Tendsto m.

LaTeX

$$$\\ Tendsto (\\lambda a. (m(a) : \\mathrm{EReal}))\\ f\\ (\\mathcal{N}\\, \\uparrow a) \\ \\Longleftrightarrow\\ Tendsto\\ m\\ f\\ (\\mathcal{N}\\ a)$$$

Lean4

@[norm_cast]
theorem tendsto_coe_ennreal {α : Type*} {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} :
    Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) :=
  isEmbedding_coe_ennreal.tendsto_nhds_iff.symm

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