Skip to content

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 に直接対応なし