Theorem Perfect.small_diam_splitting

Modification history

2024-08-07 07:08
Mathlib/Topology/MetricSpace/Perfect.lean
chore: backports for leanprover/lean4#4814 (part 22) (#15511)
Modified Perfect.small_diam_splittingView on Github →
2024-02-13 21:51
Mathlib/Topology/MetricSpace/Perfect.lean
refactor(Topology): split Topology.Perfect into two modules (#10272) …
Modified Perfect.small_diam_splittingView on Github →
2023-04-20 06:30
Mathlib/Topology/Perfect.lean
chore: forward port last part of leanprover-community/mathlib#18248 (#3508)
Added Perfect.small_diam_splittingView on Github →