Theorems · Definition · general topology

AbstractCompletion.mapEquiv

{α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) →
      {β : Type uβ} →
        [inst_1 : UniformSpace β] → (pkg' : AbstractCompletion.{vβ, uβ} β) → α ≃ᵤ β → pkg.space ≃ᵤ pkg'.space

The uniform isomorphism between two completions of isomorphic uniform spaces.

Defined in

Mathlib.Topology.UniformSpace.AbstractCompletion

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace