📐 Proposition VII.3.9（連続性の開集合・閉集合特徴づけ）

📐 Proposition VII.3.9（連続性の開集合・閉集合特徴づけ） #Card
- 位相 $\xi, \tau$ 間の $f \in C(\xi,\tau)$ を開集合・閉集合で言い換えると。

Back

$\xi, \tau$ が位相のとき、$f \in C(\xi,\tau)$ は次と同値:

$f^-(O) \in \mathcal{O}\xi$ for every $O \in \mathcal{O}\tau$（開集合の逆像は開）
$f^-(C) \in \mathcal{C}\xi$ for every $C \in \mathcal{C}\tau$（閉集合の逆像は閉）

証明の鍵は Cor VII.3.3（$\lim_\theta$ の閉集合表示）で、連続性の filter 定義から「収束点の像が収束する」条件を、開集合を含む filter の条件に翻訳する。一般の収束（位相でない）ではこの同値性は崩れる。

Meaning

Proposition VII.3.9 の直前で著者は「位相空間間の連続性は閉集合・開集合の言葉で特徴づけられる」と述べる。位相 $\xi,\tau$ 間の $f \in C(\xi,\tau)$ は、開集合の逆像が開（または閉集合の逆像が閉）ことと同値——これは位相に限った性質であり、一般の収束では成立しない。

出典: refs/math/topology/royal-road-to-topology/pdfs/chp7-2024-topological-structures.pdf p.134–135

Lean

continuous_def（IsOpen.preimage）が Mathlib の標準定義そのもの。

本ノート RoyalRoad.ChapterVII.prop_VII_3_9_10（連続性の5条件 TFAE、Notes/ChapterVII.lean、lake build 済み）