Theorems · Definition · algebraic topology
Bundle.TotalSpace.proj
{B : Type u_1} → {F : Type u_4} → {E : B → Type u_5} → Bundle.TotalSpace F E → BBundle.TotalSpace.proj is the canonical projection Bundle.TotalSpace F E → B from the
total space to the base space.
- Defined in
- Mathlib.Data.Bundle
- Cited by
- 447 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bundle.TotalSpacestatement and proof · cited by 766
Cited by534
Results whose statement or proof uses this declaration.
- MemTrivializationAtlasstatement · cited by 108
- FiberBundle.trivializationAtstatement · cited by 95
- Bundle.TotalSpace.sndstatement · cited by 76
- Bundle.Trivialization.IsLinearstatement · cited by 70
- Bundle.Trivialization.coordChangeLstatement and proof · cited by 38
- Bundle.Trivialization.symmstatement and proof · cited by 37
- Bundle.Trivialization.continuousLinearMapAtstatement and proof · cited by 33
- Bundle.Trivialization.localFrameCoeffstatement and proof · cited by 33
- Bundle.Trivialization.symmLstatement and proof · cited by 32
- Bundle.Trivialization.continuousLinearEquivAtstatement and proof · cited by 27
- Bundle.Pretrivialization.symmstatement and proof · cited by 26
- Bundle.Pretrivialization.IsLinearstatement · cited by 21
Showing the 200 most cited of 534.