Topology Terminology Map (Royal Road ↔ 標準 ↔ Mathlib)

Topology 用語対応表（Royal Road ↔ 標準用語 ↔ Mathlib）

Royal Road to Topology（Dolecki–Mynard, Convergence Foundations of Topology）は フィルター・収束第一主義を採り、標準的な位相の教科書とは語彙・記号・順序の向きが体系的にずれている（20_Literature/royal_road_to_topology/reader-guide 参照）。この表は本書の用語を 標準的な数学用語（英語表記） と Mathlib の宣言名／型クラス に対応づける横断辞書。記号 → 定義カードの逆引きは 20_Literature/royal_road_to_topology/symbol-index、章/節順の索引は royal-road-to-topology-Flashcards を参照。

Mathlib 対応が「—（本体になし）」の行は、本書独自の一般化（一般の収束構造）で Mathlib 本体に対応物がないもの。位相に特殊化した場合の対応物を括弧で補記する。自作の最小形式化 (Notes/Chapter*.lean) がある場合はその名前を添える。

フィルター・収束の基礎語彙

Royal Road 用語	標準用語	Mathlib 名
filter（cards/topology/filter）	filter	Filter
proper filter（固有フィルター, cards/topology/proper-filter）	proper / nondegenerate filter	Filter.NeBot (f ≠ ⊥)
principal filter（cards/topology/principal-filter）	principal filter	Filter.principal (𝓟 s)
ultrafilter（cards/topology/ultrafilter）	ultrafilter	Ultrafilter
grill $\mathcal{A}^{#}$（cards/topology/grill）	grill (Choquet)	—（超フィルター経由で還元）
mesh $\mathcal{A}#\mathcal{B}$（cards/topology/grill）	filters mesh / meet is proper	Filter.NeBot (𝒜 ⊓ ℬ)
convergence structure $\xi$（cards/topology/convergence）	convergence structure / limit relation	—（位相版 F ≤ 𝓝 x；自作 ConvergenceSpace）
$\lim_\xi \mathcal{F}$（極限, cards/topology/convergence）	set of limit points	—（位相版 𝓝 x, Filter.Tendsto）

近傍・閉包まわり（最も語彙が独特）

Royal Road 用語	標準用語	Mathlib 名
vicinity filter $V_\xi(x)$（cards/topology/vicinity-filter）	neighborhood filter	nhds (𝓝 x)
adherence $\operatorname{adh}_\xi A$（cards/topology/adherence）	closure / set of adherent points	closure（mem_closure_iff_clusterPt）
adherent point（$x\in\operatorname{adh}_\xi\mathcal{F}$）	cluster / adherent point	ClusterPt
inherence $\operatorname{inh}_\xi A$（cards/topology/inherence）	interior（adherence の双対）	interior
vicinity $V\in V_\xi(x)$	neighborhood	s ∈ 𝓝 x

収束構造の分類（本書の「収束の分類学」）

Royal Road 用語	標準用語	Mathlib 名
topology（cards/topology/pretopology 内対比）	topology	TopologicalSpace
pretopology（cards/topology/pretopology）	pretopology / Čech closure space	—（自作 IsPretopology；位相は特殊ケース）
pseudotopology（cards/topology/pseudotopology）	pseudotopology	—（超フィルターに還元され現れにくい）
convergence modifier / topologizer（cards/topology/convergence-modifier）	topological modification / reflector	—（本体になし）
discrete convergence $\iota$（cards/topology/discrete-convergence）	discrete topology	⊥（Mathlib TopologicalSpace 順序）
chaotic convergence $o$（cards/topology/chaotic-convergence）	indiscrete / trivial topology	⊤（同上）

コンパクト性・被覆・連続

Royal Road 用語	標準用語	Mathlib 名
compact（cards/topology/compact-convergence-definition）	compact	IsCompact / CompactSpace
compactoid set（cards/topology/compactoid-set）	compactoid（相対コンパクト様）	—（位相版 IsCompact の一般化）
$\xi$-cover $\mathcal{P}\trianglerighteq_\xi A$（cards/topology/xi-cover-definition）	cover	—（集合演算 A ⊆ ⋃₀ 𝒫）
continuous map（cards/topology/continuous-map）	continuous map	Continuous / ContinuousAt = Tendsto f (𝓝 x) (𝓝 (f x))
$\beta X$（超フィルター空間, cards/topology/stone-topology-ultrafilter-space）	Stone space / Stone–Čech compactification	Ultrafilter X（台）+ TopologicalSpace

順序の向きに関する重要な注意

本書と Mathlib は finer/coarser の記号の向きが逆。混同を避けるための対応を明示する。

Royal Road 用語	標準用語	Mathlib 名
$\zeta \geq \xi$（$\zeta$ が finer, cards/topology/order-on-convergences）	finer convergence/topology	t ≤ s（逆向き: ≤ が小さいほど finer, ⊥=離散, ⊤=密着）
$\mathcal{F} \subset \mathcal{G}$（$\mathcal{G}$ が finer, cards/topology/filter）	finer filter	𝓖 ≤ 𝓕（逆向き: 包含が大きいほど finer）

• 本書: フィルターは $\subset$ が大きいほど finer、収束は $\geq$ が大きいほど finer（$\iota$ 離散が最大）。
• Mathlib: Filter・TopologicalSpace とも ≤ が 小さいほど finer（⊥ が離散）。規約ブリッジは cards/topology/filter-decomposition-theorem・20_Literature/royal_road_to_topology/chapter2 を参照。