Theorems · Definition · category theory
Sequential.isoOfHomeo
{X Y : Sequential} → ↑X.toTop ≃ₜ ↑Y.toTop → (X ≅ Y)Construct an isomorphism from a homeomorphism.
- Defined in
- Mathlib.Topology.Category.Sequential
- 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.Isostatement · cited by 3,963
- TopCat.carrierstatement and proof · cited by 3,184
- Homeomorphstatement and proof · cited by 725
- Homeomorph.symmproof · cited by 365
- TopCat.ofHomproof · cited by 44
- CategoryTheory.InducedCategory.homMkproof · cited by 33
- Sequentialstatement and proof · cited by 11
- Sequential.toTopstatement and proof · cited by 8
Cited by5
Results whose statement or proof uses this declaration.
- Sequential.isoEquivHomeoproof · cited by 2
- Sequential.isoEquivHomeo_symm_applystatement · cited by 0
- Sequential.isoOfHomeo_homstatement and proof · cited by 0
- Sequential.isoOfHomeo_invstatement and proof · cited by 0
- LightCondSet.sequentialAdjunctionCounitIsoproof · cited by 0