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