Proposition III.1.11 (前位相の特徴づけ)
- Proposition III.1.11 (前位相の特徴づけ) #Card
- 近傍系フィルターによる前位相の言い換え。
A convergence $\xi$ on $X$ is a pretopology if and only if $x \in \lim_\xi V_\xi(x)$ for each $x \in X$.
証明の骨子. 近傍系フィルター $V_\xi(x) = \bigwedge \xi^-(x)$（cards/topology/vicinity-filter）は定義上 $\xi^-(x)$ のすべての元より粗い下界であり、$\xi^-(x)$ の任意の下界より細かい（最大下界）。
- ($\Leftarrow$) 各 $x$ で $x \in \lim_\xi V_\xi(x)$、すなわち $V_\xi(x) \in \xi^-(x)$ ならば、$V_\xi(x)$ は $\xi^-(x)$ に属する下界だから $\xi^-(x)$ の最小（最粗）元。よって $\xi$ は前位相（cards/topology/pretopology）。
- ($\Rightarrow$) $\xi$ が前位相なら $\xi^-(x)$ に最粗元 $W$ が存在する。$W$ は $\xi^-(x)$ の下界だから $W \geq V_\xi(x)$（$V_\xi(x)$ が最大下界）、一方 $W \in \xi^-(x)$ より $V_\xi(x) \geq W$（$V_\xi(x)$ が下界）。ゆえに $V_\xi(x) = W \in \xi^-(x)$、すなわち $x \in \lim_\xi V_\xi(x)$。∎
なお $\sigma_\mathbb{R}$ では $V_{\sigma_\mathbb{R}}(x)$（開区間基）は sequential でないので収束せず、前位相にならない（Example III.1.9）。
Notes/ChapterIII.lean : prop_III_1_11（vicinityFilter を Mathlib の sSup で構成し、IsGreatest との同値を証明。lake build 済み）