Theorems · Theorem · general topology

GromovHausdorff.totallyBounded

∀ {t : Set GromovHausdorff.GHSpace} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ},
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ p ∈ t, Metric.diam Set.univ ≤ C) →
      (∀ p ∈ t, ∀ (n : ℕ), ∃ s, Cardinal.mk ↑s ≤ ↑(K n) ∧ Set.univ ⊆ ⋃ x ∈ s, Metric.ball x (u n)) → TotallyBounded t

Compactness criterion: a closed set of compact metric spaces is compact if the spaces have a uniformly bounded diameter, and for all ε the number of balls of radius ε required to cover the spaces is uniformly bounded. This is an equivalence, but we only prove the interesting direction that these conditions imply compactness.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorff

Cited by

0 results in Mathlib

Foundations

Depth 249 from the axioms · uses propext, Classical.choice, Quot.sound