ratCast_atBot — Mathlib

English

Analogous to atTop, if a property holds eventually on the bottom, then it holds eventually for rationals cast to R atBot.

Русский

Аналогично снизу: если свойство выполняется в предельном смысле для вещественного atBot, то оно выполняется и для рациональных через приведение к R в atBot.

LaTeX

$$$\forall p:\, R \to \mathrm{Prop},\; \big(\forall^\infty x \in \mathrm{atBot},\ p(x)\big) \Rightarrow \big(\forall^\infty n \in \mathrm{atBot},\ p(n)\big)$$$

Lean4

theorem ratCast_atBot [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atBot, p x) : ∀ᶠ (n : ℚ) in atBot, p n := by rw [← Rat.comap_cast_atBot (R := R)];
  exact h.comap _

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