Proposition II.3.4 (主フィルターの inf)
- Proposition II.3.4 (主フィルターの inf) #Card
- 主フィルターの族の infimum はどうなるか。
Each infimum of principal filters is a principal filter: $$\bigwedge_{A \in \mathcal{A}} {A}^\uparrow = \Big{\bigcup_{A \in \mathcal{A}} A\Big}^\uparrow.$$
（主フィルターのクラス $\mathbb{F}_0$ は inf で閉じる。sup では閉じない——有限基底が保たれるとは限らない。）
証明の骨子:
- inf は共通部分（cards/topology/prop-ii-3-2）: $\bigwedge_A {A}^\uparrow = \bigcap_A {A}^\uparrow$。
- $F \in \bigcap_A {A}^\uparrow \iff$ 各 $A$ で $A \subset F \iff \bigcup_A A \subset F \iff F \in {\bigcup_A A}^\uparrow$。
- ゆえに $\bigwedge_A {A}^\uparrow = {\bigcup_A A}^\uparrow$——核 $\bigcup_A A$ を持つ主フィルター。「各主フィルターの核（生成集合）の合併」が inf の核になる、という単純な集合演算。
Filter.iInf_principal…は有限版; 一般には Filter.principal_iUnion 相当（Mathlib 順序で ⨆ 𝓟 = 𝓟 ⋃: Filter.iSup_principal）
本ノート RoyalRoad.ChapterII.prop_II_3_4（⨆ i, 𝓟 (s i) = 𝓟 (⋃ i, s i)、Notes/ChapterII.lean、lake build 済み）