Convergence

集合 $X$ 上の「フィルターが点に収束する」という関係 $\xi \subset \mathbb{F}X \times X$ を公理化したものが convergence structure。isotone（大きいフィルターほど収束しやすい）と centered（各点は自分自身の主フィルターに収束する）の2公理のみを課す最も一般的な収束の枠組みで、位相空間の収束 $\mathcal{F} \to x \iff \mathcal{F} \supset \mathcal{N}(x)$ はその特殊ケースにすぎない。測度論の測度収束・概収束、関数解析の弱収束・作用素位相など、位相化できない収束現象も同じ枠組みで扱える。

書籍別カード

• Royal Road to Topology: cards/topology/convergence — isotone + centered な関係 $\xi$ として定義。位相を第VII章まで導入しない設計思想の核。自作形式化 Notes/ChapterIII.lean : ConvergenceSpace。

用語対応（terminology-map）

30_Concepts/topology-terminology-map（PR #168、未マージ）「フィルター・収束の基礎語彙」節に該当行あり:

convergence structure $\xi$（cards/topology/convergence） | convergence structure / limit relation | —（位相版 F ≤ 𝓝 x；自作 ConvergenceSpace）

一般の convergence space は Mathlib 本体にない。位相の特殊ケースでは本書の $x \in \lim_\xi \mathcal{F}$ が Mathlib の F ≤ 𝓝 x（Filter.Tendsto id F (𝓝 x) 相当）に対応する。