P-Space

A -space is a topological space in which every countable intersection of open sets is open. Equivalently, every G_delta set is open (Gillman and Henriksen 1954).

Every discrete topology gives a -space. Conversely, a metrizable topology on a -space is discrete, because each singleton is a G_delta set. There are nondiscrete examples. On an uncountable set, the topology consisting of the empty set and the sets with countable complements is a -space, since a countable union of countable sets is countable.

For a Tychonoff space , let be its real-valued continuous function space with the topology of pointwise convergence. Dow and Tkachuk (2025) asked whether must be a -space if the closure of every countable subset of is a pseudocomplete space. Almeida (2026) reported an affirmative answer. The stronger reported statement is that whenever is not a -space, contains a closed separable, metrizable linear subspace that is not pseudocomplete. This removes the additional functional-countability assumption in the earlier result. Here functional countability means that every real-valued continuous function on has countable image.

Almeida supplied the main strategy and credits ChatGPT Astra with completing the argument and Claude Opus 5.5 with producing the Lean formalization. As of Oct. 15, 2026, the project reported successful Lean checks with only standard axioms, but independent expert review had not been reported (Almeida 2026).