Theorems · Definition · algebraic topology

FiberPrebundle.pretrivializationAtlas

{B : Type u_2} →
  {F : Type u_3} →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            FiberPrebundle F E → Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)

Defined in: Mathlib.Topology.FiberBundle.Basic
Cited by: 7 results in Mathlib
Foundations: Depth 2 from the axioms · uses no axioms
Assumes: TopologicalSpace TopologicalSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

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.TotalSpacestatement · cited by 766
Bundle.TotalSpace.projstatement · cited by 447
Bundle.Pretrivializationstatement · cited by 111
FiberPrebundlestatement and proof · cited by 16

Cited by10

Results whose statement or proof uses this declaration.

FiberPrebundle.totalSpaceTopologyproof · cited by 7
FiberPrebundle.trivializationOfMemPretrivializationAtlasstatement and proof · cited by 5
FiberPrebundle.pretrivialization_mem_atlasstatement · cited by 3
FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlasstatement and proof · cited by 1
FiberPrebundle.isOpen_sourceproof · cited by 1
VectorPrebundle.toVectorBundleproof · cited by 1
FiberPrebundle.toFiberBundleproof · cited by 1
FiberPrebundle.continuous_trivChangestatement · cited by 0
FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_interstatement and proof · cited by 0
VectorPrebundle.contMDiffVectorBundleproof · cited by 0