tendsto_ratCast_atTop_iff — Mathlib

English

For any f: α → ℚ, the tendsto of f cast to R atTop is equivalent to the tendsto of f atTop.

Русский

Для любой функции f: α → ℚ предельность в R на atTop эквивалентна предельности самой функции f на atTop.

LaTeX

$$$\\operatorname{Tendsto}((f(n) : R))\, l\, \\mathrm{atTop} \\;\\Longleftrightarrow\\; \\operatorname{Tendsto} f\, l\, \\mathrm{atTop}$$$

Lean4

theorem tendsto_ratCast_atTop_iff [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℚ}
    {l : Filter α} : Tendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop := by
  rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]; rfl

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