Theorems · Theorem · general topology

GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv

∀ {X : Type u} [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X] {Y : Type v}
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  GromovHausdorff.toGHSpace X = GromovHausdorff.toGHSpace Y ↔ Nonempty (X ≃ᵢ Y)

Two nonempty compact spaces have the same image in GHSpace if and only if they are isometric.

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorff

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpaceCompactSpaceNonemptyMetricSpaceCompactSpaceNonempty