Theorem exists_locally_finite_Union_eq_ball_radius_lt
Modification history
2021-07-23 08:09
src/topology/metric_space/basic.lean
refactor(topology/metric_space): move lemmas about `paracompact_space` and the shrinking lemma to separate files (#8404) …
Modified exists_locally_finite_Union_eq_ball_radius_ltView on Github →