Theorems · Definition · general topology

Metric.toGlueL

{X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : Nonempty Z] →
        [inst_1 : MetricSpace Z] →
          [inst_2 : MetricSpace X] →
            [inst_3 : MetricSpace Y] →
              {Φ : Z → X} → {Ψ : Z → Y} → (hΦ : Isometry Φ) → (hΨ : Isometry Ψ) → X → Metric.GlueSpace hΦ hΨ

The canonical map from X to the space obtained by gluing isometric subsets in X and Y.

Defined in

Mathlib.Topology.MetricSpace.Gluing

Cited by

2 results in Mathlib

Foundations

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

Assumes

NonemptyMetricSpaceMetricSpaceMetricSpace