Proposition III.3.2 (最細・最粗の収束)
- Proposition III.3.2 (最細・最粗の収束) #Card
- $X$ 上の収束全体の中で最細・最粗のものは何か。
The discrete convergence $\iota_X$ is the finest, and the chaotic convergence $o_X$ is the coarsest convergence on $X$.
証明の骨子. $\zeta \geq \xi$（$\zeta$ が finer）とは各 $\mathcal{F}$ で $\lim_\zeta \mathcal{F} \subset \lim_\xi \mathcal{F}$（cards/topology/order-on-convergences）。
- $\iota_X$ が最細: 任意の収束 $\xi$ に対し $\iota_X \geq \xi$ を示す。離散収束では $\lim_\iota \mathcal{F} = {x : \mathcal{F} = x^\uparrow}$（cards/topology/discrete-convergence）。$x \in \lim_\iota \mathcal{F}$ なら $\mathcal{F} = x^\uparrow$、(centered) より $x \in \lim_\xi x^\uparrow = \lim_\xi \mathcal{F}$。ゆえに $\lim_\iota \mathcal{F} \subset \lim_\xi \mathcal{F}$。
- $o_X$ が最粗: 任意の $\xi$ に対し $\xi \geq o_X$。混沌収束は $\lim_o \mathcal{F} = X$（cards/topology/chaotic-convergence）なので $\lim_\xi \mathcal{F} \subset X = \lim_o \mathcal{F}$ は自明。∎
（Lean では discrete/chaotic を自作し IsFiner で両端性を証明済み。）
Notes/ChapterIII.lean : prop_III_3_2（lake build 済み）