Commit 2023-03-05 07:28 41b3bbf5

View on Github →

feat: port Topology.MetricSpace.ShrinkingLemma (#2629)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/ShrinkingLemma.lean

added theorem exists_locallyFinite_subset_unionᵢ_ball_radius_lt

added theorem exists_locallyFinite_unionᵢ_eq_ball_radius_lt

added theorem exists_subset_unionᵢ_ball_radius_lt

added theorem exists_subset_unionᵢ_ball_radius_pos_lt

added theorem exists_unionᵢ_ball_eq_radius_lt

added theorem exists_unionᵢ_ball_eq_radius_pos_lt