Theorems · Theorem · algebraic topology
Bundle.Trivialization.lift_self
∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
[inst_2 : TopologicalSpace Z] {T : Bundle.Trivialization F proj} {z : Z}, proj z ∈ T.baseSet → T.lift z (proj z) = z- Cited by
- 1 results in Mathlib
- Foundations
- Depth 70 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.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Bundle.Trivializationstatement and proof · cited by 324
- Bundle.Trivialization.baseSetstatement and proof · cited by 268
- Bundle.Trivialization.mem_sourceproof · cited by 24
- Bundle.Trivialization.symm_apply_mk_projproof · cited by 4
- Bundle.Trivialization.liftstatement · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- Bundle.Trivialization.clift_selfproof · cited by 0