Topology on infinite sequence spaces

Stream: Is there code for X?

[Patrick Lutz]

Suppose $A$ is any set. Then the set of infinite sequences $A^{\mathbb{N}}$ has a natural topology, which corresponds to the product topology after giving $A$ the discrete topology. Such spaces are very common in logic, e.g. they are often the most natural setting for various constructions in descriptive set theory. Does mathlib know about this topology?

And if so, does mathlib already contain basic facts about it? For example, that every closed set corresponds to a set of finite sequences over $A$ in the following way: for every closed set $X \subseteq A^{\mathbb{N}}$, there is a set $C$ of finite sequences such that for each $x\in A^{\mathbb{N}}$, $x \in X$ if and only if some element of $C$ is a prefix of $x$.

[Jireh Loreaux]

The type of sequences with values in A in Lean is just ℕ → A, which is a (non-dependent) Π-type and so inherits the topology docs#Pi.topological_space (which is the product topology). So, if you give A the discrete topology, then ℕ → A will automatically have the topology you want. I'm not sure if we have the prefix result, but I haven't looked, I just don't know off the top of my head.

[Patrick Lutz]

Thanks! I suspected that $A^{\mathbb{N}}$ should already be a topological space in mathlib but wasn't sure where to look so this is helpful. I'm also still very interested in knowing if mathlib has lemmas of the sort I mentioned

[Kevin Buzzard]

Nat can be replaced by any type at all here.

[Patrick Lutz]

Kevin Buzzard said:

Nat can be replaced by any type at all here.

Good point, though some of the results I'm interested in only work for $\mathbb{N}$

[Kevin Buzzard]

By the way, your claim should be about open sets not closed sets, right? And it wouldn't surprise me if there was a result in mathlib giving the canonical basis for a product of (possibly infinitely many) topological spaces.

[Patrick Lutz]

Yes, I meant open sets

[Junyan Xu]

Should be relatively easy from docs#is_topological_basis_pi

[Pedro Sánchez Terraf]

Hi Patrick, @Felix Weilacher has been working on DST and I'm also doing some baby steps into that direction (#17972).

[Felix Weilacher]

https://leanprover-community.github.io/mathlib_docs/topology/metric_space/pi_nat.html
has a lot about these spaces.

And for your fact see docs#pi_nat.is_topological_basis_cylinders