Commit 2023-10-30 02:26 442eef6f

View on Github →

chore: split Topology.MetricSpace.Metrizable* (#7912) Move

basic definitions to Topology.Metrizable.Basic,
Urysohn's metrization theorem to `Topology.Metrizable.Urysohns', and
metrizability of a uniform space with countably generated uniformity to Topology.Metrizable.Uniform. The next step is to redefine Metrizable as "uniformizable with countably generated uniformity" and make this definition available much earlier.

Estimated changes

Modified Counterexamples/SorgenfreyLine.lean

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/Metrizable.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

Modified Mathlib/Topology/Instances/Discrete.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Renamed Mathlib/Topology/MetricSpace/Metrizable.lean to Mathlib/Topology/Metrizable/Basic.lean

deleted theorem TopologicalSpace.exists_embedding_l_infty

deleted theorem TopologicalSpace.metrizableSpace_of_t3_second_countable

Renamed Mathlib/Topology/MetricSpace/MetrizableUniformity.lean to Mathlib/Topology/Metrizable/Uniformity.lean

Created Mathlib/Topology/Metrizable/Urysohn.lean

added theorem TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology

added theorem TopologicalSpace.exists_embedding_l_infty

added theorem TopologicalSpace.exists_inducing_l_infty

added theorem TopologicalSpace.metrizableSpace_of_t3_second_countable