Theorems · Theorem · order theory

Filter.Eventually.intCast_atTop

∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop},
  (∀ᶠ (x : R) in Filter.atTop, p x) → ∀ᶠ (n : ℤ) in Filter.atTop, p ↑n

Defined in

Mathlib.Order.Filter.AtTopBot.Archimedean

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingPartialOrderIsStrictOrderedRingArchimedean