Theorems · Theorem · algebraic topology
FiberBundle.isQuotientMap_proj
∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
[inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
[Nonempty F], Topology.IsQuotientMap Bundle.TotalSpace.projThe projection from a fiber bundle with a nonempty fiber to its base is a quotient map.
- Defined in
- Mathlib.Topology.FiberBundle.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Bundle.TotalSpacestatement and proof · cited by 766
- FiberBundlestatement and proof · cited by 471
- Bundle.TotalSpace.projstatement · cited by 447
- Topology.IsQuotientMapstatement · cited by 124
- IsOpenMap.isQuotientMapproof · cited by 10
- FiberBundle.continuous_projproof · cited by 6
- FiberBundle.isOpenMap_projproof · cited by 2
- FiberBundle.surjective_projproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.