tendsto_coe_nhds_top — Mathlib

English

The coe from NNReal to ENNReal preserves convergence to ∞: a nonnegative real-valued function tends to ∞ iff its ENNReal coe-tized version tends to ∞.

Русский

Переход через встроение NNReal → ENNReal сохраняет сходящийся к бесконечности предел: сходится ли f к бесконечности, то же верно для (f x).

LaTeX

$$$\\operatorname{Tendsto} (\\lambda x. (f x : ENNReal)) \\ell (\\mathcal{N}(\\infty)) \\iff \\operatorname{Tendsto} f \\ell \\text{atTop}$$$

Lean4

@[simp, norm_cast]
theorem tendsto_coe_nhds_top {f : α → ℝ≥0} {l : Filter α} :
    Tendsto (fun x => (f x : ℝ≥0∞)) l (𝓝 ∞) ↔ Tendsto f l atTop := by
  rw [tendsto_nhds_top_iff_nnreal, atTop_basis_Ioi.tendsto_right_iff]; simp

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