English
If p holds eventually for large real numbers, then it holds eventually for integers after casting, i.e., eventual properties transfer via integer casting to top.
Русский
Если свойство выполняется преимущественно для больших вещественных чисел, то оно тоже будет выполняться для целых чисел после приведения, то есть переход свойств через целочисленное приведение сохраняется.
LaTeX
$$$\forall p:\, \mathbb{R}\to \mathrm{Prop},\; (\forall^{\infty} x\in\mathrm{atTop},\ p(x)) \Rightarrow (\forall^{\infty} n\in\mathrm{atTop},\ p(n))$$$
Lean4
theorem intCast_atTop [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop}
(h : ∀ᶠ (x : R) in atTop, p x) : ∀ᶠ (n : ℤ) in atTop, p n := by rw [← Int.comap_cast_atTop (R := R)];
exact h.comap _
