手筋: 分離公理を「証拠となる開集合」に翻訳して制限・積・連続像で運ぶ (Ex VII.5.5 / Prop VII.5.4 / Sorgenfrey Ex VII.2.3)
- 手筋: 分離公理を「証拠となる開集合」に翻訳して制限・積・連続像で運ぶ (Ex VII.5.5 / Prop VII.5.4 / Sorgenfrey Ex VII.2.3) #Card
- 位相の $T_0$（一般に分離公理）が部分空間・積で保存されることを、なぜ一撃で言えるのか？一般の収束では保存されないのはなぜか？
核: 位相の分離公理は「点（対）を区別する開集合という局所的な証拠」の存在で言い換えられる。証拠は制限・積・連続像で運べるので保存が自動化される。
- $T_0$（位相）= Prop VII.5.4: 相異なる2点 $x_0\neq x_1$ の一方のみを含む開集合が存在。
- 部分空間で保存（Ex VII.5.5）: $Y\subset X$、$y_0\neq y_1\in Y$ を分離する $\xi$-開 $O$ をとり、$O\cap Y$ が $\xi|_Y$-開でやはり一方のみ含む。開集合を $Y$ に制限するだけ。
- 境界判定にも同じ発想（Ex VII.2.3）: 集合が閉でないことは「境界点を1つ選び、その近傍が集合外へはみ出す」＝分離する近傍の非存在で示す。
一般の収束では破綻: $T_0$ の定義 $x_0\neq x_1\Rightarrow\xi^-(x_0)\neq\xi^-(x_1)$（cards/topology/t0-convergence）は「収束フィルターの族が点を区別」で、制限するとフィルター族が痩せて区別能力を失いうる（Example III.7.6）。位相では区別が開集合という局所化可能な object に担われるため制限で生き残る——ここが位相と一般収束の分かれ目。
射程: $T_1,T_2,T_3,T_{3\frac12}$ …すべて「分離する開集合／連続関数の存在」に翻訳してから運ぶ（Tikhonov 積での $T_2$・$T_{3\frac12}$ の保存、埋め込みでの継承）。分離を連続関数で担わせると cards/topology/technique-diagonal-embedding（対角埋め込み）に直結。
Mathlib: T0Space/T1Space/T2Space、部分空間保存は Subtype.t0Space 系（Topology.IsInducing.t0Space）、積は Pi.t2Space 等。