Theorems · Theorem · global analysis
StructureGroupoid.mem_of_eqOnSource
∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) {e e' : OpenPartialHomeomorph H H},
e ∈ G → e' ≈ e → e' ∈ G- Cited by
- 9 results in Mathlib
- Foundations
- Depth 21 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.
Cites4
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
- OpenPartialHomeomorphstatement and proof · cited by 664
- StructureGroupoidstatement and proof · cited by 121
- StructureGroupoid.mem_of_eqOnSource'proof · cited by 1
Cited by9
Results whose statement or proof uses this declaration.
- StructureGroupoid.compatible_of_mem_maximalAtlasproof · cited by 2
- StructureGroupoid.mem_maximalAtlas_of_eqOnSourceproof · cited by 1
- OpenPartialHomeomorph.singleton_hasGroupoidproof · cited by 1
- StructureGroupoid.trans_restrictedproof · cited by 1
- closedUnderRestriction_iff_id_leproof · cited by 1
- symm_trans_mem_contDiffGroupoidproof · cited by 0
- StructureGroupoid.mem_iff_of_eqOnSourceproof · cited by 0
- StructureGroupoid.restr_mem_of_eqOnproof · cited by 0
- StructureGroupoid.HasGroupoid.compproof · cited by 0