English
Define atBot as the infimum of principal filters generated by downward rays {b | b ≤ a} as a runs over α.
Русский
Определим atBot как инфимуум всех перинциальных фильтров, порождаемых подстановками {b | b ≤ a} по всем a в α.
LaTeX
$$$\\mathrm{atBot} = \\bigsqcap_{a\\in \\alpha} \\mathcal{P}(\\{ b \\in \\alpha \\mid b \\le a \\}).$$$
Lean4
/-- `atBot` is the filter representing the limit `→ -∞` on an ordered set.
It is generated by the collection of down-sets `{b | b ≤ a}`.
(The preorder need not have a bottom element for this to be well defined,
and indeed is trivial when a bottom element exists.) -/
def atBot [Preorder α] : Filter α :=
⨅ a, 𝓟 (Iic a)
