Proposition II.2.6 (補有限フィルターの適切性)
- Proposition II.2.6 (補有限フィルターの適切性) #Card
- $(X)_0$ が proper filter になる条件。
The family $(X)_0$ of cofinite subsets of a non-empty set $X$ is a proper filter if and only if $X$ is infinite.
証明の骨子:
- isotone は明らか。有限交叉閉性は $X \setminus (F_0 \cap F_1) = (X \setminus F_0) \cup (X \setminus F_1)$ が有限の和ゆえ有限、から従う。
- proper 性 $\emptyset \notin (X)_0$ は「$X \setminus \emptyset = X$ が有限でない」、すなわち $X$ が無限であることと同値。$X$ が有限なら $X = X \setminus \emptyset$ が有限で $\emptyset \in (X)_0$、improper になる。
- ゆえに $(X)_0$ が proper filter $\iff X$ 無限。
Filter.cofinite.neBot（Infinite X が仮定）
本ノート RoyalRoad.ChapterII.prop_II_2_6（Notes/ChapterII.lean、lake build 済み）