Theorems · Definition · general topology

GromovHausdorff.OptimalGHCoupling

(X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [CompactSpace X] → [Nonempty X] → [inst : MetricSpace Y] → [CompactSpace Y] → [Nonempty Y] → Type (max v u)

A metric space which realizes the optimal coupling between X and Y

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Cited by

5 results in Mathlib

Foundations

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

Assumes

MetricSpaceCompactSpaceNonemptyMetricSpaceCompactSpaceNonempty