Theorems · Definition · general topology
Topology.IsQuotientMap.homeomorph
{X : Type u_1} →
{Y : Type u_2} →
[inst : TopologicalSpace X] →
[inst_1 : TopologicalSpace Y] → {f : C(X, Y)} → Topology.IsQuotientMap ⇑f → Quotient (Setoid.ker ⇑f) ≃ₜ YThe homeomorphism from the quotient of a quotient map to its codomain. This is
Setoid.quotientKerEquivOfSurjective as a homeomorphism.
- Defined in
- Mathlib.Topology.ContinuousMap.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- Equivproof · cited by 8,337
- ContinuousMapstatement and proof · cited by 2,491
- Homeomorphstatement · cited by 725
- Topology.IsQuotientMapstatement and proof · cited by 124
- Setoid.kerstatement and proof · cited by 43
- Setoid.quotientKerEquivOfSurjectiveproof · cited by 1
Cited by6
Results whose statement or proof uses this declaration.
- Topology.IsQuotientMap.liftproof · cited by 6
- Topology.IsQuotientMap.lift_compproof · cited by 2
- Topology.IsQuotientMap.lift_applystatement · cited by 1
- Topology.IsQuotientMap.homeomorph_symm_applystatement and proof · cited by 1
- Topology.IsQuotientMap.homeomorph.congr_simpstatement and proof · cited by 0
- Topology.IsQuotientMap.homeomorph_applystatement and proof · cited by 0