ratCast_atTop — Mathlib

English

If a property holds eventually on the real atTop, then it holds eventually for rational values atTop as well.

Русский

Если свойство выполняется в предельно часто встречающемся смысле на вещественном atTop, то оно тоже выполняется для рациональных значений в atTop.

LaTeX

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

Lean4

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

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