English
For any function f from a set to the integers, the tendency to infinity of its real-valued cast is equivalent to the tendency to infinity of the original integer-valued function.
Русский
Для любого отображения f: α → ℤ предельная устремлённость к бесконечности после приведения значений в R эквивалентна устремлённости к бесконечности самой функции f.
LaTeX
$$$\operatorname{Tendsto}(\lambda n: (f\,n) : \mathbb{Z} \to R) \, l \, \mathrm{atTop} \;\Longleftrightarrow\; \operatorname{Tendsto} f \, l \, \mathrm{atTop}$$$
Lean4
theorem tendsto_intCast_atTop_iff [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℤ}
{l : Filter α} : Tendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop := by
rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]; rfl
