Commit 2024-01-18 02:11 1872765c

View on Github →

chore(MetricSpace/PseudoMetric): split out proper spaces (#9812) And move one lemma to a better place. Shaves off another 130 lines from a 2200 line file; #9815 continues with a more far-reaching split.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Created Mathlib/Topology/MetricSpace/ProperSpace.lean

added theorem Metric.exists_isLocalMin_mem_ball

added theorem exists_lt_subset_ball

added theorem exists_pos_lt_subset_ball

added theorem isCompact_sphere

added theorem properSpace_of_compact_closedBall_of_le

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

deleted theorem Metric.exists_isLocalMin_mem_ball

deleted theorem exists_lt_subset_ball

deleted theorem exists_pos_lt_subset_ball

deleted theorem isCompact_sphere

deleted theorem properSpace_of_compact_closedBall_of_le