Theorems · Theorem · general topology
IsOpenQuotientMap.isQuotientMap
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
IsOpenQuotientMap f → Topology.IsQuotientMap fAn open quotient map is a quotient map.
- Defined in
- Mathlib.Topology.Maps.OpenQuotient
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Topology.IsQuotientMapstatement · cited by 124
- IsOpenQuotientMapstatement and proof · cited by 65
- IsOpenQuotientMap.isOpenMapproof · cited by 16
- IsOpenQuotientMap.surjectiveproof · cited by 16
- IsOpenQuotientMap.continuousproof · cited by 15
- IsOpenMap.isQuotientMapproof · cited by 10
Cited by12
Results whose statement or proof uses this declaration.
- coinduced_eq_induced_of_isOpenQuotientMap_of_isInducingproof · cited by 2
- ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrictproof · cited by 2
- MonoidHom.isOpenQuotientMap_iff_isQuotientMapproof · cited by 1
- IsOpenQuotientMap.continuous_comp_iffproof · cited by 1
- IsOpenQuotientMap.iff_isOpenMap_isQuotientMapproof · cited by 1
- AddMonoidHom.isOpenQuotientMap_iff_isQuotientMapproof · cited by 1
- isQuotientMap_fstproof · cited by 0
- isQuotientMap_sndproof · cited by 0
- QuotientRing.isQuotientMap_coe_coeproof · cited by 0
- IsOpenQuotientMap.of_comp_iffproof · cited by 0
- SeparationQuotient.isQuotientMap_prodMap_mkproof · cited by 0
- Topology.IsInducing.isQuotientMap_of_surjectiveproof · cited by 0