Theorems · Definition · general topology
UniformEquiv.symm
{α : Type u} → {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → α ≃ᵤ β → β ≃ᵤ αInverse of a uniform isomorphism.
- Defined in
- Mathlib.Topology.UniformSpace.Equiv
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
- Assumes
- UniformSpaceUniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivproof · cited by 8,337
- Equiv.symmproof · cited by 3,681
- UniformSpacestatement and proof · cited by 2,040
- UniformEquivstatement and proof · cited by 80
- UniformEquiv.toEquivproof · cited by 21
- UniformEquiv.uniformContinuous_invFunproof · cited by 1
- UniformEquiv.uniformContinuous_toFunproof · cited by 1
Cited by33
Results whose statement or proof uses this declaration.
- UniformEquiv.isUniformInducingproof · cited by 3
- Padic.withValUniformEquivproof · cited by 3
- AbstractCompletion.mapEquivproof · cited by 2
- UniformEquiv.apply_symm_applystatement · cited by 1
- UniformEquiv.arrowCongrproof · cited by 1
- UniformEquiv.symm_apply_applystatement · cited by 1
- UniformEquiv.symm_comp_selfstatement · cited by 1
- AbstractCompletion.mapEquiv_symmstatement · cited by 1
- UniformEquiv.uniformContinuous_symmstatement · cited by 1
- AbstractCompletion.uniformContinuous_compareEquiv_symmstatement · cited by 1
- UniformSpace.Completion.mapEquiv_symmstatement · cited by 0