Gδ subspaces of Polish spaces

A subset of a completely metrizable space is completely metrizable in the subspace topology if and only if it is a Gδ set (Alexandrov's theorem together with its converse). In particular a subset of a Polish space is Polish exactly when it is Gδ. Open and closed subsets are the special cases IsOpen.isGδ and IsClosed.isGδ.

This is how Polish structures are found on the subspaces arising in descriptive set theory, such as comeagre Gδ sets and model classes cut out by countably many open conditions.

Main results

• TauCeti.isGδ_of_isCompletelyMetrizableSpace: in a Hausdorff space, a completely metrizable subspace whose closure is Gδ is itself Gδ. The closure of every set is Gδ in a perfectly normal space, for example in a metrizable space.
• TauCeti.isGδ_iff_isCompletelyMetrizableSpace, TauCeti.isGδ_iff_polishSpace: the resulting characterizations of Gδ subsets of completely metrizable and of Polish spaces.

Implementation notes

The forward direction uses Mathlib's IsGδ.isCompletelyMetrizableSpace and IsGδ.polishSpace. This file supplies the converse and combines it with those upstream results to obtain the iff characterizations.

For the converse, the sets U n of points having a neighbourhood whose trace on s has diameter less than 1 / (n + 1) for a complete metric on s are open and contain s, and s = closure s ∩ ⋂ n, U n: at a point of the right-hand side, the trace on s of its neighbourhood filter is a Cauchy filter, whose limit in s must be the point itself.

References

• A. S. Kechris, Classical Descriptive Set Theory, Springer, 1995, Theorem 3.11.

theorem TauCeti.isGδ_of_isCompletelyMetrizableSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} [TopologicalSpace.IsCompletelyMetrizableSpace ↑s] (hclosure : IsGδ (closure s)) : IsGδ s

A subset of a Hausdorff space which is completely metrizable in the subspace topology and whose closure is a Gδ set is itself a Gδ set. The closure is Gδ for every subset of a perfectly normal space, for example of a metrizable space, where isClosed_closure.isGδ supplies the hypothesis.

theorem TauCeti.isGδ_iff_isCompletelyMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X] {s : Set X} : IsGδ s ↔ TopologicalSpace.IsCompletelyMetrizableSpace ↑s

Alexandrov's theorem and its converse: a subset of a completely metrizable space is completely metrizable in the subspace topology if and only if it is a Gδ set.

theorem TauCeti.isGδ_iff_polishSpace {X : Type u_1} [TopologicalSpace X] [PolishSpace X] {s : Set X} : IsGδ s ↔ PolishSpace ↑s

A subset of a Polish space is Polish in the subspace topology if and only if it is a Gδ set.