Theorems · Inductive type · general topology
PartialHomeomorph
(X : Type u_7) → (Y : Type u_8) → [TopologicalSpace X] → [TopologicalSpace Y] → Type (max u_7 u_8)
Partial homeomorphisms, defined on subsets of the space
- Defined in
- Mathlib.Topology.PartialHomeomorph.Defs
- Cited by
- 73 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by106
Results whose statement or proof uses this declaration.
- PartialHomeomorph.toPartialEquivstatement and proof · cited by 917
- OpenPartialHomeomorph.toPartialHomeomorphstatement · cited by 851
- OpenPartialHomeomorph.symmproof · cited by 460
- PartialHomeomorph.toFun'statement and proof · cited by 57
- PartialHomeomorph.symmstatement and proof · cited by 38
- OpenPartialHomeomorph.prod_toPartialHomeomorphstatement · cited by 13
- PartialHomeomorph.continuousOn_toFunstatement and proof · cited by 10
- PartialHomeomorph.continuousOn_invFunstatement and proof · cited by 9
- Homeomorph.toPartialHomeomorphOfImageEqstatement · cited by 7
- PartialHomeomorph.ofContinuousOpenRestrictstatement · cited by 6
- Topology.IsEmbedding.toPartialHomeomorphstatement · cited by 6
- OpenPartialHomeomorph.toPartialHomeomorph_injectivestatement and proof · cited by 5