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.