Theorems · Definition · general topology
Homeomorph.symm
{X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → Y ≃ₜ XInverse of a homeomorphism.
- Defined in
- Mathlib.Topology.Homeomorph.Defs
- Cited by
- 365 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 46 definitions · uses no axioms
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.
- TopologicalSpacestatement and proof · cited by 24,529
- Equivproof · cited by 8,337
- Equiv.symmproof · cited by 3,681
- Homeomorphstatement and proof · cited by 725
- Homeomorph.toEquivproof · cited by 77
- Homeomorph.continuous_toFunproof · cited by 4
- Homeomorph.continuous_invFunproof · cited by 3
Cited by409
Results whose statement or proof uses this declaration.
- Homeomorph.isInducingproof · cited by 33
- Homeomorph.comap_nhds_eqstatement and proof · cited by 23
- Homeomorph.isQuotientMapproof · cited by 22
- Homeomorph.symm_apply_applystatement · cited by 18
- Homeomorph.apply_symm_applystatement · cited by 18
- Homeomorph.image_symmstatement and proof · cited by 13
- TopCat.isoOfHomeoproof · cited by 12
- MeasureTheory.Measure.toSphereproof · cited by 12
- Homeomorph.preimage_symmstatement · cited by 9
- Homeomorph.isClosed_imageproof · cited by 8
- Topology.IsQuotientMap.isStrictMap_iffproof · cited by 8
- Homeomorph.isCompact_preimageproof · cited by 7
Showing the 200 most cited of 409.