Theorems · Theorem · order theory

Filter.Eventually.ratCast_atBot

∀ {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop},
  (∀ᶠ (x : R) in Filter.atBot, p x) → ∀ᶠ (n : ℚ) in Filter.atBot, p ↑n

Defined in

Mathlib.Order.Filter.AtTopBot.Archimedean

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingArchimedean