Theorems · Definition · general topology

UniformSpace.Completion.mapEquiv

{α : Type u_1} →
  [inst : UniformSpace α] →
    {β : Type u_2} → [inst_1 : UniformSpace β] → α ≃ᵤ β → UniformSpace.Completion α ≃ᵤ UniformSpace.Completion β

The uniform isomorphism between two completions of isomorphic uniform spaces.

Defined in

Mathlib.Topology.UniformSpace.Completion

Cited by

3 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace