Cantor Cube (カントール立方体) (Example IV.6.8)
- Cantor Cube (カントール立方体) (Example IV.6.8) #Card
- The power set ${0,1}^\mathbb{N}$ endowed with the product convergence $\iota^\mathbb{N} = \prod_{n \in \mathbb{N}} \iota$. Is it discrete?
The power ${0,1}^\mathbb{N}$ endowed with the product convergence $\iota^\mathbb{N} = \prod_{n \in \mathbb{N}} \iota$（各因子は離散）is called the Cantor cube.
- 離散ではない: $\varphi_k(n) := 1$ if $k = n$, else $0$ とすると各座標で $\lim_k \varphi_k(n) = 0$、よって $(\varphi_k)_k$ の生成する自由フィルターは $\varphi \equiv 0$ に収束する。
- 有限積の離散収束は離散（Proposition IV.6.7）なのに、可算積では崩れる典型例。非離散だが $\iota_{{0,1}}$-initial な収束の例でもある。
- 有限集合上の Hausdorff 収束は離散のみなので、「Cantor cube」と言えば暗黙に $\iota^\mathbb{N}$ を指す。
Bool^ℕ＝ℕ → Bool の積位相；Mathlib の Cantor 集合関連は Mathlib.Topology.MetricSpace.CantorScheme