Filter.AtTopBot
================

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

コード元
[Filter.AtTopBot](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/AtTopBot/Defs.html)

``` 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, Filter.principal (Set.Ici a)
```
`atTop`は前順序(preorder)集合上の極限`→ ∞`を表すフィルタです. 
`{b | a ≤ b}`の上に生成されるフィルタの下限を取ることで定義されます.