# mathlibdocumentation

topology.metric_space.shrinking_lemma

# 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

theorem exists_subset_Union_ball_radius_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {s : set α} {r : ι → } (hs : is_closed s) (uf : ∀ (x : α), x s{i : ι | x metric.ball (c i) (r i)}.finite) (us : s ⋃ (i : ι), metric.ball (c i) (r i)) :
∃ (r' : ι → ), (s ⋃ (i : ι), metric.ball (c i) (r' i)) ∀ (i : ι), r' i < r i

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 λ x, ball (c i) (r i) is a locally finite covering and provides a covering indexed by the same type.

theorem exists_Union_ball_eq_radius_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {r : ι → } (uf : ∀ (x : α), {i : ι | x metric.ball (c i) (r i)}.finite) (uU : (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ) :
∃ (r' : ι → ), (⋃ (i : ι), metric.ball (c i) (r' i)) = set.univ ∀ (i : ι), r' i < r i

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.

theorem exists_subset_Union_ball_radius_pos_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {s : set α} {r : ι → } (hr : ∀ (i : ι), 0 < r i) (hs : is_closed s) (uf : ∀ (x : α), x s{i : ι | x metric.ball (c i) (r i)}.finite) (us : s ⋃ (i : ι), metric.ball (c i) (r i)) :
∃ (r' : ι → ), (s ⋃ (i : ι), metric.ball (c i) (r' i)) ∀ (i : ι), r' i (r i)

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.

theorem exists_Union_ball_eq_radius_pos_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {r : ι → } (hr : ∀ (i : ι), 0 < r i) (uf : ∀ (x : α), {i : ι | x metric.ball (c i) (r i)}.finite) (uU : (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ) :
∃ (r' : ι → ), (⋃ (i : ι), metric.ball (c i) (r' i)) = set.univ ∀ (i : ι), r' i (r i)

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.

theorem exists_locally_finite_subset_Union_ball_radius_lt {α : Type u} [metric_space α] [proper_space α] {s : set α} (hs : is_closed s) {R : α → } (hR : ∀ (x : α), x s0 < R x) :
∃ (ι : Type u) (c : ι → α) (r r' : ι → ), (∀ (i : ι), c i s 0 < r i r i < r' i r' i < R (c i)) locally_finite (λ (i : ι), metric.ball (c i) (r' i)) s ⋃ (i : ι), metric.ball (c i) (r i)

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_locally_compact_sigma_compact_of_nhds_basis_set and exists_subset_Union_ball_radius_pos_lt.

theorem exists_locally_finite_Union_eq_ball_radius_lt {α : Type u} [metric_space α] [proper_space α] {R : α → } (hR : ∀ (x : α), 0 < R x) :
∃ (ι : Type u) (c : ι → α) (r r' : ι → ), (∀ (i : ι), 0 < r i r i < r' i r' i < R (c i)) locally_finite (λ (i : ι), metric.ball (c i) (r' i)) (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ

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_locally_compact_sigma_compact_of_nhds_basis and exists_Union_ball_eq_radius_pos_lt or exists_locally_finite_subset_Union_ball_radius_lt.