Commit 2024-02-13 21:51 10d64868

View on Github →

refactor(Topology): split Topology.Perfect into two modules (#10272) Splits Topology.Perfect into two modules: Topology.Perfect, where the existing definition of Perfect and Preperfect are kept, and Topology.MetricSpace.Perfect, in which the theorems specific to metric spaces are moved.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/Topology/Algebra/Module/Cardinality.lean

Created Mathlib/Topology/MetricSpace/Perfect.lean

added theorem IsClosed.exists_nat_bool_injection_of_not_countable

added theorem Perfect.exists_nat_bool_injection

added theorem Perfect.small_diam_splitting

Modified Mathlib/Topology/Perfect.lean

deleted theorem IsClosed.exists_nat_bool_injection_of_not_countable

deleted theorem Perfect.exists_nat_bool_injection

deleted theorem Perfect.small_diam_splitting