Sequential Filter (列フィルター) (Definition II.2.9)

• Sequential Filter (列フィルター) (Definition II.2.9) #Card
  • A filter $\mathcal{F}$ on $X$ is sequential if there exists a sequence $\varphi \in X^N$ such that $\mathcal{F} = \Gamma_\varphi$.

Back

A filter $\mathcal{F}$ on $X$ is sequential if there exists a sequence $\varphi \in X^N$ such that $\mathcal{F} = \Gamma_\varphi$.

Meaning

列型フィルターは II.1 で導入した $\Gamma_\varphi$ と同型である——列から得られるフィルターのクラス $\mathbb{S}$（$X$ 上では $\varepsilon X$）として定義される。

Proposition II.2.10 により、従来の表現では尾の族 ${{x_k : k \geq n} : n \in \mathbb{N}}$ が filter-base となる。Remark II.2.11 では、指標集合 $\mathbb{N}$ の順序は収束問題では無関係であり、任意の無限可算集合 $N$ 上の写像 $\varphi \in X^N$ として列を見れば足りると繰り返される。

すべての列型フィルターは可算集合を含む（Cor II.2.12）。逆に、可算基底を持つフィルターがすべて列型とは限らない（Example II.2.23）。

出典: refs/math/topology/royal-road-to-topology/pdfs/chp2-2024-from-convergence-of-sequences-to-the-concept-of-filter.pdf p.22–23

Lean

数列のフィルター Filter.map a atTop（または基底による生成）