Theorems · Theorem · general topology

Metric.glueDist_swap

∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x y : X ⊕ Y), Metric.glueDist Ψ Φ ε x.swap y.swap = Metric.glueDist Φ Ψ ε x y

Defined in

Mathlib.Topology.MetricSpace.Gluing

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpaceMetricSpace