# Polish spaces #

A topological space is Polish if its topology is second-countable and there exists a compatible complete metric. This is the class of spaces that is well-behaved with respect to measure theory. In this file, we establish the basic properties of Polish spaces.

## Main definitions and results #

`PolishSpace α`

is a mixin typeclass on a topological space, requiring that the topology is second-countable and compatible with a complete metric. To endow the space with such a metric, use in a proof`letI := upgradePolishSpace α`

. We register an instance from complete second-countable metric spaces to Polish spaces, not the other way around.- We register that countable products and sums of Polish spaces are Polish.
`IsClosed.polishSpace`

: a closed subset of a Polish space is Polish.`IsOpen.polishSpace`

: an open subset of a Polish space is Polish.`exists_nat_nat_continuous_surjective`

: any nonempty Polish space is the continuous image of the fundamental Polish space`ℕ → ℕ`

.

A fundamental property of Polish spaces is that one can put finer topologies, still Polish, with additional properties:

`exists_polishSpace_forall_le`

: on a topological space, consider countably many topologies`t n`

, all Polish and finer than the original topology. Then there exists another Polish topology which is finer than all the`t n`

.`IsClopenable s`

is a property of a subset`s`

of a topological space, requiring that there exists a finer topology, which is Polish, for which`s`

becomes open and closed. We show that this property is satisfied for open sets, closed sets, for complements, and for countable unions. Once Borel-measurable sets are defined in later files, it will follow that any Borel-measurable set is clopenable. Once the Lusin-Souslin theorem is proved using analytic sets, we will even show that a set is clopenable if and only if it is Borel-measurable, see`isClopenable_iff_measurableSet`

.

### Basic properties of Polish spaces #

A Polish space is a topological space with second countable topology, that can be endowed with a metric for which it is complete. We register an instance from complete second countable metric space to polish space, and not the other way around as this is the most common use case.

To endow a Polish space with a complete metric space structure, do `letI := upgradePolishSpace α`

.

- is_open_generated_countable : ∃ (b : Set (Set α)), b.Countable ∧ h = TopologicalSpace.generateFrom b
- complete : ∃ (m : MetricSpace α), UniformSpace.toTopologicalSpace = h ∧ CompleteSpace α

## Instances

A convenience class, for a Polish space endowed with a complete metric. No instance of this
class should be registered: It should be used as `letI := upgradePolishSpace α`

to endow a Polish
space with a complete metric.

## Instances

## Equations

- ⋯ = ⋯

Construct on a Polish space a metric (compatible with the topology) which is complete.

## Equations

- polishSpaceMetric α = ⋯.choose.replaceTopology ⋯

## Instances For

This definition endows a Polish space with a complete metric. Use it as:
`letI := upgradePolishSpace α`

.

## Equations

- upgradePolishSpace α = let __src := ⋯; UpgradedPolishSpace.mk

## Instances For

## Equations

- ⋯ = ⋯

A countable product of Polish spaces is Polish.

## Equations

- ⋯ = ⋯

A countable disjoint union of Polish spaces is Polish.

## Equations

- ⋯ = ⋯

The product of two Polish spaces is Polish.

## Equations

- ⋯ = ⋯

The disjoint union of two Polish spaces is Polish.

## Equations

- ⋯ = ⋯

Any nonempty Polish space is the continuous image of the fundamental space `ℕ → ℕ`

.

Given a closed embedding into a Polish space, the source space is also Polish.

Any countable discrete space is Polish.

## Equations

- ⋯ = ⋯

Pulling back a Polish topology under an equiv gives again a Polish topology.

A closed subset of a Polish space is also Polish.

## Equations

- ⋯ = ⋯

Given a Polish space, and countably many finer Polish topologies, there exists another Polish topology which is finer than all of them.

### An open subset of a Polish space is Polish #

To prove this fact, one needs to construct another metric, giving rise to the same topology,
for which the open subset is complete. This is not obvious, as for instance `(0,1) ⊆ ℝ`

is not
complete for the usual metric of `ℝ`

: one should build a new metric that blows up close to the
boundary.

Porting note: definitions and lemmas in this section now take `(s : Opens α)`

instead of
`{s : Set α} (hs : IsOpen s)`

so that we can turn various definitions and lemmas into instances.
Also, some lemmas used to assume `Set.Nonempty sᶜ`

in Lean 3. In fact, this assumption is not
needed, so it was dropped.

A type synonym for a subset `s`

of a metric space, on which we will construct another metric
for which it will be complete.

## Equations

- s.CompleteCopy = ↥s

## Instances For

A distance on an open subset `s`

of a metric space, designed to make it complete. It is given
by `dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|`

, where the second term blows up close to
the boundary to ensure that Cauchy sequences for `dist'`

remain well inside `s`

.

## Equations

- TopologicalSpace.Opens.CompleteCopy.instDist = { dist := fun (x y : s.CompleteCopy) => dist ↑x ↑y + |1 / Metric.infDist (↑x) (↑s)ᶜ - 1 / Metric.infDist (↑y) (↑s)ᶜ| }

## Equations

- TopologicalSpace.Opens.CompleteCopy.inst = inferInstanceAs (TopologicalSpace ↥s)

## Equations

- ⋯ = ⋯

A metric space structure on a subset `s`

of a metric space, designed to make it complete
if `s`

is open. It is given by `dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|`

, where the
second term blows up close to the boundary to ensure that Cauchy sequences for `dist'`

remain well
inside `s`

.

Porting note: the definition changed to ensure that the `TopologicalSpace`

structure on
`TopologicalSpace.Opens.CompleteCopy s`

is definitionally equal to the original one.

## Equations

- TopologicalSpace.Opens.CompleteCopy.instMetricSpace = MetricSpace.ofT0PseudoMetricSpace s.CompleteCopy

## Equations

- ⋯ = ⋯

An open subset of a Polish space is also Polish.

### Clopenable sets in Polish spaces #

A set in a topological space is clopenable if there exists a finer Polish topology for which
this set is open and closed. It turns out that this notion is equivalent to being Borel-measurable,
but this is nontrivial (see `isClopenable_iff_measurableSet`

).

## Equations

- PolishSpace.IsClopenable s = ∃ t' ≤ t, PolishSpace α ∧ IsClosed s ∧ IsOpen s

## Instances For

Given a closed set `s`

in a Polish space, one can construct a finer Polish topology for
which `s`

is both open and closed.