Theorems · Definition · general topology

GromovHausdorff.optimalGHInjr

(X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [inst_1 : CompactSpace X] →
        [inst_2 : Nonempty X] →
          [inst_3 : MetricSpace Y] →
            [inst_4 : CompactSpace Y] → [inst_5 : Nonempty Y] → Y → GromovHausdorff.OptimalGHCoupling X Y

Injection of Y in the optimal coupling between X and Y

Defined in

Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Cited by

4 results in Mathlib

Foundations

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

Assumes

MetricSpaceCompactSpaceNonemptyMetricSpaceCompactSpaceNonempty