2.3 Baire-space cylinder infrastructure
The proof of Theorem 2.8 requires a small theory of cylinders in \(\mathbb {N}^\mathbb {N}\), adapted from [ 14 , § 7.A ] .
Lean: Cyl
For \(N : \mathbb {N}\to \mathbb {N}\) and \(n \in \mathbb {N}\),
[ 14 , § 7.A ] .
Lean: Bnd
\(\mathrm{Bnd}\, N \; :=\; \bigcap _n \mathrm{Cyl}\, N\, n \; =\; \prod _i [0, N_i]\) [ 14 , § 7.A ] .
Lean: truncate
\(\mathrm{truncate}\, N\, g\, i \; :=\; \min (g\, i,\; N\, i)\). Sends any sequence into \(\mathrm{Bnd}\, N\) and agrees with \(g\) on cylinders.
Lean: isCompact_bnd
\(\mathrm{Bnd}\, N\) is compact (Tychonoff applied to the finite intervals \([0, N_i]\)).
Lean: bnd_subset_cyl
\(\mathrm{Bnd}\, N \subseteq \mathrm{Cyl}\, N\, n\) for every \(n\).
Lean: cyl_succ_eq
\(\mathrm{Cyl}\, N\, (n+1) = \mathrm{Cyl}\, N\, n \cap \{ g : g\, (n+1) \le N\, (n+1)\} \).
Lean: cyl_inter_eq_cyl_update
Intersecting a cylinder with a coordinate-level constraint rewrites as a cylinder with an updated bound at that coordinate.
Lean: monotone_cyl_split
The map \(k \mapsto \mathrm{Cyl}\, N\, n \cap \{ g : g\, (n+1) \le k\} \) is monotone in \(k\).
Lean: truncate_mem_bnd
\(\mathrm{truncate}\, N\, g \in \mathrm{Bnd}\, N\) for every \(g\).
Lean: truncate_agree_on_cyl
If \(g \in \mathrm{Cyl}\, N\, n\) then \(\mathrm{truncate}\, N\, g\, i = g\, i\) for all \(i \le n\).
Lean: cyl_ext
Two elements of \(\mathrm{Cyl}\, N\, n\) agreeing on the first \(n+1\) coordinates are equal on \(\mathrm{Cyl}\).
Lean: iInter_closure_image_cyl_eq
Under a continuous parametrization \(f : \mathbb {N}^\mathbb {N}\to \alpha \) into a Polish space, \(\bigcap _n \overline{f(\mathrm{Cyl}\, N\, n)} = f(\mathrm{Bnd}\, N)\).