Cofinite Convergence (補有限収束) (Example III.1.17)

• Cofinite Convergence (補有限収束) (Example III.1.17) #Card
  • The cofinite convergence of an infinite set $X$ is the pretopology $\theta$ such that $X = \lim_\theta (X)0$; then $x \in \lim\theta \mathcal{F} \iff \mathcal{F} \supset (X)_0 \wedge x^\uparrow$.

Back

The cofinite convergence of an infinite set $X$ is the pretopology $\theta$ such that $$X = \lim_\theta (X)0,$$ where $(X)0$ is the cofinite filter of $X$. Then ${x} = \lim\theta x^\uparrow$, and by (isotone), $x \in \lim\theta \mathcal{F}$ if and only if $\mathcal{F} \supset (X)_0 \wedge x^\uparrow$.

• $\theta$ is free (alias $T_1$) but not Hausdorff（補有限フィルターが全点に収束する）.
• $\theta$ is the coarsest free convergence on $X$（cards/topology/lem-iii-3-9）.

Lean

位相の場合は補有限位相（Mathlib: CofiniteTopology）。Filter.cofinite と比較