tendsto_coe_atTop — Mathlib

English

Tendsto (a ↦ (m a : ℝ)) f atTop is equivalent to Tendsto m f atTop for NNReal m.

Русский

Сходимость через коe на atTop равна сходимости исходной функции на atTop.

LaTeX

$$$\\text{Tendsto} (a \\mapsto (m a : \\mathbb{R})) f atTop \\iff \\text{Tendsto} m f atTop$$$

Lean4

@[simp, norm_cast]
theorem tendsto_coe_atTop {f : Filter α} {m : α → ℝ≥0} : Tendsto (fun a => (m a : ℝ)) f atTop ↔ Tendsto m f atTop :=
  tendsto_Ici_atTop.symm

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