intCast_atBot — Mathlib

English

Similarly to atTop, the tendency to the bottom for integers, after casting to R, matches the bottom tendency in R.

Русский

Аналогично для снижения: тенденция к минусу бесконечности после приведения целых в R совпадает с соответствующей тенденцией в R.

LaTeX

$$$\operatorname{Tendsto}((\uparrow) : \mathbb{Z} \to R)\ \mathrm{atBot} \ \Longleftrightarrow\; \operatorname{Tendsto}\mathrm{id} \mathrm{atBot}$$$

Lean4

theorem intCast_atBot [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atBot, p x) : ∀ᶠ (n : ℤ) in atBot, p n := by rw [← Int.comap_cast_atBot (R := R)];
  exact h.comap _

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