English
Define atTop for a preorder by taking the infimum of all principal filters generated by the upward rays {b | a ≤ b} as a runs over the whole α.
Русский
Определим atTop для частично упорядоченного множества так: это инфимума всех перинциальных фильтров, порождаемых надмножествами {b | a ≤ b} по всем a в α.
LaTeX
$$$\\mathrm{atTop} = \\bigsqcap_{a\\in \\alpha} \\mathcal{P}(\\{ b \\in \\alpha \\mid a \\le b \\}).$$$
Lean4
/-- `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 exists.) -/
def atTop [Preorder α] : Filter α :=
⨅ a, 𝓟 (Ici a)
