Mathlib Map

Theorems · Definition · general topology

Homeomorph.ulift

{X : Type v} → [inst : TopologicalSpace X] → ULift.{u, v} X ≃ₜ X

ULift X is homeomorphic to X.

Defined in
Mathlib.Topology.Homeomorph.Lemmas
Cited by
6 results in Mathlib
Foundations
Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TopCat.I.homeomorph · cited by 11I.homeomorphTopCat.toSSetObjEquiv · cited by 9TopCat.toSSetObjEquivTopCat.stdSimplexHomeomorphI · cited by 6TopCat.stdSimplexHomeomor…SimplexCategory.toTopHomeo · cited by 6SimplexCategory.toTopHomeoCompHaus.epi_iff_surjective · cited by 2CompHaus.epi_iff_surjecti…TopCat.uliftFunctorObjHomeo · cited by 2TopCat.uliftFunctorObjHom…Topology.IsOpenEmbedding.uliftMap · cited by 1IsOpenEmbedding.uliftMapSSet.stdSimplex.δ_one_toSSetObjI · cited by 1stdSimplex.δ_one_toSSetOb…SSet.stdSimplex.δ_zero_toSSetObjI · cited by 1stdSimplex.δ_zero_toSSetO…Topology.IsEmbedding.uliftMap · cited by 0IsEmbedding.uliftMapTopology.IsClosedEmbedding.uliftMap · cited by 0IsClosedEmbedding.uliftMapTopologicalSpace · cited by 24529TopologicalSpaceEquiv · cited by 8337EquivHomeomorph · cited by 725HomeomorphEquiv.ulift · cited by 115Equiv.uliftHomeomorph.uliftCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by11

Results whose statement or proof uses this declaration.