手筋: 分離する連続写像の族 → 対角写像 → 立方体への埋め込み (Cor VII.5.6 / Tikhonov 埋め込み)
- 手筋: 分離する連続写像の族 → 対角写像 → 立方体への埋め込み (Cor VII.5.6 / Tikhonov 埋め込み) #Card
- 位相 $\xi$ をある「立方体」$\prod_{f\in C}Z$（各 $Z$ は $$$ や $[0,1]$）に埋め込むには、テスト写像の族 $C$ に何を課し、どう組み立てるか？
3段テンプレート。テスト写像族 $C\subset C(\xi,\tau_Z)$ をとり、対角写像 $$e:=\triangle_{f\in C} f:\ X\to\textstyle\prod_{f\in C} Z,\qquad e(x):=(f(x))_{f\in C}.$$
- 始位相を誘導: 積の始位相は各射影 $\pi_f$ の前像の上限 $\bigvee_f f^-\tau_Z$。族 $C$ が $\xi$ をちょうど生成する（$\xi=\bigvee_{f\in C}f^-\tau_Z$）とき $e$ は $\xi$ を誘導。位相クラスでは Sierpiński 位相がこの生成能力を持つ（cards/topology/thm-vii-5-2-sierpinski-initially-dense Thm VII.5.2）。
- 点を分離 ⟹ 単射: 相異なる $x_0\neq x_1$ をある $f\in C$ が分離（$f(x_0)\neq f(x_1)$）すれば $e$ は単射。$T_0$ 位相では Prop VII.5.4（一方のみ含む開集合＝ある $\chi_O\in C(\xi,$)$）が分離を供給。
- 1＋2 ⟹ 埋め込み: 始位相を誘導する単射連続写像は cards/topology/embedding（Def IV.3.12）。よって $e:\xi\hookrightarrow\prod Z$。
実例（同じ骨格）:
- Cor VII.5.6: $T_0$ 位相 → Sierpiński 立方体 $$^{C(\xi,$)}$（cards/topology/sierpinski-cube-embedding）。
- Tikhonov 埋め込み: $T_{3\frac12}$（完全正則 $T_1$）→ $[0,1]^{C(\xi,[0,1])}$（cards/topology/tikhonov-cube-embedding）、Urysohn の距離化定理の骨格。
- 一般に cards/topology/diagonal-product-map（単射族の対角は積への埋め込み、Prop IV.7.7）。
射程: 「分離する族で座標付けして標準空間へ埋め込む」——測度論の標準ボレル空間・分布による埋め込み、可測関数族による点分離の原型。
Mathlib: Topology.IsEmbedding（IsInducing+Injective）、Embedding.of_comp 系、Tikhonov 埋め込みは TopologicalSpace.embedding_evalCLM/Homeomorph 経由。