Filter.AtTopBot

このファイルでは前順序集合上の極限→ ∞を表すフィルタatTopを定義しています.

コード元 Filter.AtTopBot

/-- `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, Filter.principal (Set.Ici a)

atTopは前順序(preorder)集合上の極限→ ∞を表すフィルタです. {b | a ≤ b}の上に生成されるフィルタの下限を取ることで定義されます.