Theorems · Definition · general topology

GromovHausdorff.auxGluing

(X : ℕ → Type) →
  [inst : (n : ℕ) → MetricSpace (X n)] →
    [∀ (n : ℕ), CompactSpace (X n)] → [∀ (n : ℕ), Nonempty (X n)] → (n : ℕ) → GromovHausdorff.AuxGluingStruct (X n)

Auxiliary sequence of metric spaces, containing copies of X 0, ..., X n, where each X i is glued to X (i+1) in an optimal way. The space at step n+1 is obtained from the space at step n by adding X (n+1), glued in an optimal way to the X n already sitting there.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorff

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpaceCompactSpaceNonempty