Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 14:03 2d6c52af

View on Github →

feat(topology/metric_space/polish): definition and basic properties of polish spaces (#12437) 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 PR, we establish basic (and not so basic) properties of Polish spaces.

Estimated changes

Modified src/topology/metric_space/isometry.lean

added theorem embedding.to_isometry

added theorem uniform_embedding.to_isometry

Created src/topology/metric_space/polish.lean

added theorem closed_embedding.polish_space

added theorem complete_polish_space_metric

added theorem equiv.polish_space_induced

added theorem is_closed.is_clopenable

added theorem is_closed.polish_space

added theorem is_open.is_clopenable

added theorem is_open.polish_space

added def polish_space.aux_copy

added def polish_space.complete_copy

added def polish_space.complete_copy_id_homeo

added def polish_space.complete_copy_metric_space

added theorem polish_space.complete_space_complete_copy

added theorem polish_space.dist_complete_copy_eq

added theorem polish_space.dist_le_dist_complete_copy

added theorem polish_space.exists_nat_nat_continuous_surjective

added theorem polish_space.exists_polish_space_forall_le

added def polish_space.has_dist_complete_copy

added theorem polish_space.is_clopenable.Union

added theorem polish_space.is_clopenable.compl

added def polish_space.is_clopenable

added def polish_space_metric

added def upgrade_polish_space