Theorems · Definition · general topology
CompactlyGenerated.homeoOfIso
{X Y : CompactlyGenerated} → (X ≅ Y) → ↑X.toTop ≃ₜ ↑Y.toTopConstruct a homeomorphism from an isomorphism.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CategoryTheory.Iso.homproof · cited by 7,684
- CategoryTheory.Iso.invproof · cited by 6,514
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- CategoryTheory.Isostatement and proof · cited by 3,963
- TopCat.carrierstatement · cited by 3,184
- Homeomorphstatement · cited by 725
- CompactlyGeneratedstatement and proof · cited by 11
- CompactlyGenerated.toTopstatement · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- CompactlyGenerated.isoEquivHomeoproof · cited by 2
- CompactlyGenerated.homeoOfIso_applystatement and proof · cited by 0
- CompactlyGenerated.homeoOfIso_symm_applystatement and proof · cited by 0
- CompactlyGenerated.isoEquivHomeo_applystatement · cited by 0