Theorems · Theorem · general topology
OpenPartialHomeomorph.open_target
∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
(self : OpenPartialHomeomorph X Y), IsOpen self.target- Cited by
- 38 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
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.
- TopologicalSpacestatement and proof · cited by 24,529
- IsOpenstatement · cited by 2,400
- PartialHomeomorph.toPartialEquivstatement · cited by 917
- OpenPartialHomeomorph.toPartialHomeomorphstatement · cited by 851
- OpenPartialHomeomorphstatement and proof · cited by 664
- PartialEquiv.targetstatement · cited by 650
Cited by45
Results whose statement or proof uses this declaration.
- OpenPartialHomeomorph.symmproof · cited by 460
- OpenPartialHomeomorph.transproof · cited by 98
- OpenPartialHomeomorph.lift_openEmbeddingproof · cited by 14
- differentiableWithinAt_localInvariantPropproof · cited by 13
- OpenPartialHomeomorph.eventually_right_inverseproof · cited by 9
- OpenPartialHomeomorph.trans'proof · cited by 8
- Homeomorph.transOpenPartialHomeomorphproof · cited by 7
- OpenPartialHomeomorph.isOpen_image_of_subset_sourceproof · cited by 6
- OpenPartialHomeomorph.isOpen_inter_preimage_symmproof · cited by 5
- IsLocalHomeomorphOn.mkproof · cited by 5
- OpenPartialHomeomorph.extend_image_target_mem_nhdsproof · cited by 4
- OpenPartialHomeomorph.contDiffAt_symmproof · cited by 3