Commit 2024-07-15 21:27 a2e9dd8f

View on Github →

chore: split some lemmas out of Topology.MetricSpace.ProperSpace (#13834) This removes Mathlib.Topology.MetricSpace.ProperSpace from the longest pole.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/OpenMapping.lean

Modified Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

deleted theorem Metric.exists_isLocalMin_mem_ball

deleted theorem exists_lt_subset_ball

deleted theorem exists_pos_lt_subset_ball

Created Mathlib/Topology/MetricSpace/ProperSpace/Lemmas.lean

added theorem Metric.exists_isLocalMin_mem_ball

added theorem exists_lt_subset_ball

added theorem exists_pos_lt_subset_ball

Modified Mathlib/Topology/MetricSpace/ShrinkingLemma.lean