Theorems · Theorem · general topology

Metric.toGlue_commute

∀ {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 Ψ),
  Metric.toGlueL hΦ hΨ ∘ Φ = Metric.toGlueR hΦ hΨ ∘ Ψ

Defined in

Mathlib.Topology.MetricSpace.Gluing

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonemptyMetricSpaceMetricSpaceMetricSpace