Proposition II.3.5 (フィルターは主フィルターの sup)
- Proposition II.3.5 (フィルターは主フィルターの sup) #Card
- 任意のフィルターを主フィルターからどう再構成するか。
Each filter is a supremum of principal filters: $$\mathcal{F} = \bigvee_{F \in \mathcal{F}} {F}^\uparrow.$$
（主フィルターが $\overline{\mathbb{F}}X$ で sup-dense——収束の prime 分解（cards/topology/prop-iii-4-4）と対をなす「ビルディングブロック」定理。）
証明の骨子:
- （$\supset$ 側）各 $F \in \mathcal{F}$ で ${F}^\uparrow \subset \mathcal{F}$（$\mathcal{F}$ は isotone で $F$ を含む）。上限 $\bigvee_{F} {F}^\uparrow$ は $\mathcal{F}$ に含まれる。
- （$\subset$ 側）逆に $F_0 \in \mathcal{F}$ なら $F_0 \in {F_0}^\uparrow \subset \bigvee_{F \in \mathcal{F}}{F}^\uparrow$。よって $\mathcal{F} \subset \bigvee_F {F}^\uparrow$。
- 両包含より $\mathcal{F} = \bigvee_{F \in \mathcal{F}} {F}^\uparrow$。各元 $F$ が生成する主フィルターの sup として $\mathcal{F}$ が再構成される。
Mathlib 順序では f = ⨅ s ∈ f, 𝓟 s（Filter.iInf_principal_eq_self 相当; Filter.le_iff_forall_principal 系）
本ノート RoyalRoad.ChapterII.prop_II_3_5（f = ⨅ s ∈ {s | s ∈ f}, 𝓟 s、Notes/ChapterII.lean、lake build 済み）