Theorems · Definition · general topology
OpenPartialHomeomorph.ofSet
{X : Type u_1} → [inst : TopologicalSpace X] → (s : Set X) → IsOpen s → OpenPartialHomeomorph X XThe identity partial equivalence on a set s
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- IsOpenstatement and proof · cited by 2,400
- OpenPartialHomeomorphstatement · cited by 664
- PartialEquivproof · cited by 335
- PartialEquiv.ofSetproof · cited by 9
Cited by21
Results whose statement or proof uses this declaration.
- OpenPartialHomeomorph.ofSet_applystatement and proof · cited by 4
- OpenPartialHomeomorph.symm_trans_selfstatement · cited by 3
- idRestrGroupoidproof · cited by 3
- OpenPartialHomeomorph.ofSet_transstatement and proof · cited by 3
- OpenPartialHomeomorph.self_trans_symmstatement · cited by 2
- OpenPartialHomeomorph.trans_ofSetstatement and proof · cited by 2
- OpenPartialHomeomorph.trans_of_set'statement · cited by 2
- StructureGroupoid.compatible_of_mem_maximalAtlasproof · cited by 2
- idRestrGroupoid_memstatement and proof · cited by 2
- OpenPartialHomeomorph.ofSet_trans'statement · cited by 1
- OpenPartialHomeomorph.singleton_hasGroupoidproof · cited by 1
- ofSet_mem_contDiffGroupoidstatement and proof · cited by 1