Subcofinite / Almost Principal Filter (亜余有限・ほぼ主フィルター) (Definition II.5.8)
- Subcofinite / Almost Principal Filter (亜余有限・ほぼ主フィルター) (Definition II.5.8) #Card
- A filter $\mathcal{F}$ is subcofinite if there exists $F_0 \in \mathcal{F}$ such that $F_0 \setminus F$ is finite for each $F \in \mathcal{F}$.
A filter $\mathcal{F}$ is subcofinite if there exists $F_0 \in \mathcal{F}$ such that $F_0 \setminus F$ is finite for each $F \in \mathcal{F}$.
本書独自構成。Lean に直接対応なし