Documentation

Mathlib.Topology.MetricSpace.ShrinkingLemma

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_iUnion_ball_radius_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {c : ια} {s : Set α} {r : ι} (hs : IsClosed s) (uf : xs, {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 fun x ↦ ball (c i) (r i) is a locally finite covering and provides a covering indexed by the same type.

theorem exists_iUnion_ball_eq_radius_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {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_iUnion_ball_radius_pos_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {c : ια} {s : Set α} {r : ι} (hr : ∀ (i : ι), 0 < r i) (hs : IsClosed s) (uf : xs, {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_iUnion_ball_eq_radius_pos_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {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_locallyFinite_subset_iUnion_ball_radius_lt {α : Type u} [MetricSpace α] [ProperSpace α] {s : Set α} (hs : IsClosed s) {R : α} (hR : xs, 0 < R x) :
∃ (ι : Type u) (c : ια) (r : ι) (r' : ι), (∀ (i : ι), c i s 0 < r i r i < r' i r' i < R (c i)) (LocallyFinite fun (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_locallyCompact_sigmaCompact_of_nhds_basis_set and exists_subset_iUnion_ball_radius_pos_lt.

theorem exists_locallyFinite_iUnion_eq_ball_radius_lt {α : Type u} [MetricSpace α] [ProperSpace α] {R : α} (hR : ∀ (x : α), 0 < R x) :
∃ (ι : Type u) (c : ια) (r : ι) (r' : ι), (∀ (i : ι), 0 < r i r i < r' i r' i < R (c i)) (LocallyFinite fun (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_locallyCompact_sigmaCompact_of_nhds_basis and exists_iUnion_ball_eq_radius_pos_lt or exists_locallyFinite_subset_iUnion_ball_radius_lt.