Mathlib Map

Theorems · Theorem · order theory

Rat.comap_cast_atTop

∀ {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R],
  Filter.comap Rat.cast Filter.atTop = Filter.atTop
Defined in
Mathlib.Order.Filter.AtTopBot.Archimedean
Cited by
2 results in Mathlib
Foundations
Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldLinearOrderIsStrictOrderedRingArchimedean
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

tendsto_ratCast_atTop_iff · cited by 0tendsto_ratCast_atTop_iffFilter.Eventually.ratCast_atTop · cited by 0Eventually.ratCast_atTopLinearOrder · cited by 8572LinearOrderFilter · cited by 8121FilterField · cited by 7404FieldIsStrictOrderedRing · cited by 2490IsStrictOrderedRingFilter.atTop · cited by 2405Filter.atTopArchimedean · cited by 603ArchimedeanFilter.comap · cited by 546Filter.comapRat.cast_natCast · cited by 67Rat.cast_natCastexists_nat_ge · cited by 20exists_nat_geRat.cast_le · cited by 9Rat.cast_leFilter.comap_embedding_atTop · cited by 4Filter.comap_embedding_at…Rat.comap_cast_atTopCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.