Proposition II.2.10 (列型フィルターの伝統的な形)
- Proposition II.2.10 (列型フィルターの伝統的な形) #Card
- フィルターが sequential であることの「尾の族」による言い換え。
A filter $\mathcal{F}$ on $X$ is sequential if and only if there exists a sequence $(x_n)_n$ of elements of $X$ so that $${{x_k : k \geq n} : n \in \mathbb{N}}$$ （尾 (tails) の族）is a filter-base of $\mathcal{F}$.
- 帰結（Corollary II.2.12）: 各 sequential filter は可算集合を含む（countably carried）。
- $\Gamma_\varphi$ の定義（cofinite preimage）と尾基底の定義が一致することの確認。
Filter.atTop.map φ（Filter.map_atTop_eq: 尾の族が基底）