A compact hull for a convergent sequence of compact sets

A convergent sequence of compact sets and its limit fit inside a single compact set. The hull retains every point in every set; it is not a measure support. This lets varying compact carriers share one compact probability space in the GHP completeness argument.

Adapted from Freezing2/Geometry/CompactHausdorffHull.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

def BGW.MetricMeasure.compactSequenceHull {Z : Type u_1} [MetricSpace Z] (S : ℕ → TopologicalSpace.NonemptyCompacts Z) (L : TopologicalSpace.NonemptyCompacts Z) : Set Z

The union of a sequence of compact sets and its proposed limit.

Equations

• BGW.MetricMeasure.compactSequenceHull S L = ⋃ K ∈ insert L (Set.range S), ↑K

theorem BGW.MetricMeasure.subset_compactSequenceHull_limit {Z : Type u_1} [MetricSpace Z] (S : ℕ → TopologicalSpace.NonemptyCompacts Z) (L : TopologicalSpace.NonemptyCompacts Z) : ↑L ⊆ compactSequenceHull S L

theorem BGW.MetricMeasure.subset_compactSequenceHull {Z : Type u_1} [MetricSpace Z] (S : ℕ → TopologicalSpace.NonemptyCompacts Z) (L : TopologicalSpace.NonemptyCompacts Z) (n : ℕ) : ↑(S n) ⊆ compactSequenceHull S L

theorem BGW.MetricMeasure.isCompact_compactSequenceHull {Z : Type u_1} [MetricSpace Z] {S : ℕ → TopologicalSpace.NonemptyCompacts Z} {L : TopologicalSpace.NonemptyCompacts Z} (h : Filter.Tendsto S Filter.atTop (nhds L)) : IsCompact (compactSequenceHull S L)

theorem BGW.MetricMeasure.exists_common_compact_of_cauchySeq {Z : Type u_1} [MetricSpace Z] [CompleteSpace Z] (S : ℕ → TopologicalSpace.NonemptyCompacts Z) (hS : CauchySeq S) : ∃ (L : TopologicalSpace.NonemptyCompacts Z) (K : TopologicalSpace.NonemptyCompacts Z), Filter.Tendsto S Filter.atTop (nhds L) ∧ ↑L ⊆ ↑K ∧ ∀ (n : ℕ), ↑(S n) ⊆ ↑K

A Hausdorff-Cauchy sequence in a complete ambient metric space converges and all its full carriers lie in one common compact carrier.