mathlib3 documentation

topology.metric_space.shrinking_lemma

Shrinking lemma in a proper metric space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 set.Ioo 0 (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 set.Ioo 0 (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 s 0 < 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.