Theorems · Theorem · algebraic topology
Bundle.Trivialization.open_baseSet
∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace Z] {proj : Z → B} (self : Bundle.Trivialization F proj), IsOpen self.baseSet- Cited by
- 43 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- IsOpenstatement · cited by 2,400
- Bundle.Trivializationstatement and proof · cited by 324
- Bundle.Trivialization.baseSetstatement · cited by 268
Cited by46
Results whose statement or proof uses this declaration.
- Bundle.Trivialization.toPretrivializationproof · cited by 42
- Bundle.contMDiff_zeroSectionproof · cited by 7
- mdifferentiableWithinAt_totalSpaceproof · cited by 5
- Bundle.contMDiffWithinAt_totalSpaceproof · cited by 5
- Bundle.mdifferentiable_zeroSectionproof · cited by 5
- ContMDiffWithinAt.add_sectionproof · cited by 4
- ContMDiffWithinAt.clm_apply_of_inCoordinatesproof · cited by 4
- mdifferentiableWithinAt_add_sectionproof · cited by 4
- ContMDiffWithinAt.mpullbackWithin_vectorField_interproof · cited by 4
- mdifferentiableAt_localFrameCoeffproof · cited by 4
- Bundle.Trivialization.tendsto_nhds_iffproof · cited by 3
- MDifferentiableWithinAt.mpullbackWithin_vectorField_interproof · cited by 3