Theorems · Definition · general topology
IsometryEquiv.toEquiv
{α : Type u} → {β : Type v} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → α ≃ᵢ β → α ≃ β- Defined in
- Mathlib.Topology.MetricSpace.Isometry
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- PseudoEMetricSpacestatement and proof · cited by 1,536
- IsometryEquivstatement and proof · cited by 177
Cited by41
Results whose statement or proof uses this declaration.
- IsometryEquiv.symmproof · cited by 75
- IsometryEquiv.toHomeomorphproof · cited by 16
- Delone.DeloneSet.mapIsometryproof · cited by 9
- IsometryEquiv.transproof · cited by 8
- IsometryEquiv.preimage_symmproof · cited by 7
- IsometryEquiv.apply_symm_applyproof · cited by 7
- IsometryEquiv.toDilationEquivproof · cited by 6
- IsometryEquiv.image_symmproof · cited by 4
- IsometryEquiv.surjectiveproof · cited by 4
- IsometryEquiv.withLpProdCongrproof · cited by 2
- LinearIsometryEquiv.withLpProdAssocproof · cited by 2
- IsometryEquiv.symm_apply_applyproof · cited by 2