# Shrinking lemma in a proper metric space #

In this file we prove a few versions of the shrinking lemma for coverings by balls in a proper (pseudo) metric space.

## Tags #

shrinking lemma, metric space

**Shrinking lemma** for coverings by open balls in a proper metric space. A point-finite open
cover of a closed subset of a proper metric space by open balls can be shrunk to a new cover by
open balls so that each of the new balls has strictly smaller radius than the old one. This version
assumes that `fun x ↦ ball (c i) (r i)`

is a locally finite covering and provides a covering
indexed by the same type.

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of the new balls has strictly smaller radius than the old one.

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a closed subset of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one.

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one.

Let `R : α → ℝ`

be a (possibly discontinuous) function on a proper metric space.
Let `s`

be a closed set in `α`

such that `R`

is positive on `s`

. Then there exists a collection of
pairs of balls `Metric.ball (c i) (r i)`

, `Metric.ball (c i) (r' i)`

such that

- all centers belong to
`s`

; - for all
`i`

we have`0 < r i < r' i < R (c i)`

; - the family of balls
`Metric.ball (c i) (r' i)`

is locally finite; - the balls
`Metric.ball (c i) (r i)`

cover`s`

.

This is a simple corollary of `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set`

and `exists_subset_iUnion_ball_radius_pos_lt`

.

Let `R : α → ℝ`

be a (possibly discontinuous) positive function on a proper metric space. Then
there exists a collection of pairs of balls `Metric.ball (c i) (r i)`

, `Metric.ball (c i) (r' i)`

such that

- for all
`i`

we have`0 < r i < r' i < R (c i)`

; - the family of balls
`Metric.ball (c i) (r' i)`

is locally finite; - the balls
`Metric.ball (c i) (r i)`

cover the whole space.

This is a simple corollary of `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`

and `exists_iUnion_ball_eq_radius_pos_lt`

or `exists_locallyFinite_subset_iUnion_ball_radius_lt`

.