Theorem isCompact_sphere
Modification history
2024-01-18 02:11
Mathlib/Topology/MetricSpace/ProperSpace.lean
chore(MetricSpace/PseudoMetric): split out proper spaces (#9812) …
Modified isCompact_sphereView on Github →2023-10-30 10:24
Mathlib/Topology/MetricSpace/Basic.lean
chore: split MetricSpace.basic (#7920) …
Modified isCompact_sphereView on Github →