Theorem properSpace_of_compact_closedBall_of_le

Modification history

2024-01-31 18:47
Mathlib/Topology/MetricSpace/ProperSpace.lean
chore(ProperSpace): rename constructors (#10138) …
Deleted properSpace_of_compact_closedBall_of_leView on Github →
2024-01-18 02:11
Mathlib/Topology/MetricSpace/ProperSpace.lean
chore(MetricSpace/PseudoMetric): split out proper spaces (#9812) …
Modified properSpace_of_compact_closedBall_of_leView on Github →
2023-10-30 10:24
Mathlib/Topology/MetricSpace/Basic.lean
chore: split MetricSpace.basic (#7920) …
Modified properSpace_of_compact_closedBall_of_leView on Github →
2023-03-03 17:48
Mathlib/Topology/MetricSpace/Basic.lean
feat: port Topology.MetricSpace.Basic (#2425)
Added properSpace_of_compact_closedBall_of_leView on Github →