Commit 2023-04-20 03:04 b01e05bf

View on Github →

feat: port Topology.MetricSpace.Polish (#3357)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Constructions.lean

added theorem induced_to_pi

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem Metric.continuousAt_inv_infDist_pt

Created Mathlib/Topology/MetricSpace/Polish.lean

added theorem ClosedEmbedding.polishSpace

added theorem Equiv.polishSpace_induced

added theorem IsClosed.isClopenable

added theorem IsClosed.polishSpace

added theorem IsOpen.isClopenable

added theorem IsOpen.polishSpace

added def PolishSpace.AuxCopy

added theorem PolishSpace.IsClopenable.compl

added theorem PolishSpace.IsClopenable.unionᵢ

added def PolishSpace.IsClopenable

added theorem PolishSpace.exists_nat_nat_continuous_surjective

added theorem PolishSpace.exists_polishSpace_forall_le

added theorem TopologicalSpace.Opens.CompleteCopy.dist_eq

added theorem TopologicalSpace.Opens.CompleteCopy.dist_val_le_dist

added def TopologicalSpace.Opens.CompleteCopy

added theorem complete_polishSpaceMetric

added def polishSpaceMetric

added def upgradePolishSpace