Theorems · Definition · general topology

IsometryEquiv.trans

{α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] → [inst_2 : PseudoEMetricSpace γ] → α ≃ᵢ β → β ≃ᵢ γ → α ≃ᵢ γ

The composition of two isometric isomorphisms, as an isometric isomorphism.

Defined in

Mathlib.Topology.MetricSpace.Isometry

Cited by

8 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpacePseudoEMetricSpace