Theorems · Definition · algebraic topology
Bundle.TotalSpace.snd
{B : Type u_1} → {F : Type u_4} → {E : B → Type u_5} → (self : Bundle.TotalSpace F E) → E self.proj- Defined in
- Mathlib.Data.Bundle
- Cited by
- 76 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- Bundle.TotalSpace.projstatement · cited by 447
Cited by88
Results whose statement or proof uses this declaration.
- Bundle.Pretrivialization.symmproof · cited by 26
- tangentMapproof · cited by 19
- tangentMapWithinproof · cited by 14
- Bundle.TotalSpace.toProdproof · cited by 11
- FiberBundleCore.localTrivAsPartialEquivproof · cited by 10
- Bundle.Pullback.liftproof · cited by 9
- equivTangentBundleProdproof · cited by 8
- Bundle.Pretrivialization.continuousAlternatingMapproof · cited by 5
- Bundle.Pretrivialization.continuousLinearMapproof · cited by 5
- Bundle.Trivialization.Prod.toFun'proof · cited by 4
- Bundle.Pretrivialization.mk_symmproof · cited by 4
- Bundle.Pretrivialization.symm_applystatement · cited by 4