Theorems · Definition · general topology

Filter.atTop

{α : Type u_3} → [Preorder α] → Filter α

atTop is the filter representing the limit → ∞ on an ordered set. It is generated by the collection of up-sets {b | a ≤ b}. (The preorder need not have a top element for this to be well defined, and indeed is trivial when a top element x exists, i.e., it coincides with pure x.)

Defined in

Mathlib.Order.Filter.AtTopBot.Defs

Cited by

2,405 results in Mathlib

Foundations

Depth 15 from the axioms, rests on 87 definitions · uses propext, Quot.sound

Assumes

Preorder