natCast_atTop — Mathlib

English

If a property holds eventually atTop for real numbers, it also holds eventually atTop for natural numbers after casting.

Русский

Если свойство выполняется в пределе atTop для вещественных, оно выполняется и для натовых после приведения к нату.

LaTeX

$$$[Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R]\; {p: R \to Prop},\; (\forall^ᶠ x \in atTop, p x) \Rightarrow (\forall^ᶠ n \in atTop, p n)$$$

Lean4

theorem natCast_atTop [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atTop, p x) : ∀ᶠ (n : ℕ) in atTop, p n :=
  tendsto_natCast_atTop_atTop.eventually h

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