Theorems · Definition · algebraic topology

FiberPrebundle.pretrivializationAt

{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 → B → 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.

Cites5

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

Cited by7

Results whose statement or proof uses this declaration.

FiberPrebundle.mem_pretrivializationAt_sourcestatement and proof · cited by 3
FiberPrebundle.pretrivialization_mem_atlasstatement · cited by 3
FiberPrebundle.mem_base_pretrivializationAtstatement · cited by 2
FiberPrebundle.totalSpaceMk_preimage_sourcestatement · cited by 2
FiberPrebundle.totalSpaceMk_isInducingstatement · cited by 1
FiberPrebundle.inducing_totalSpaceMk_of_inducing_compstatement and proof · cited by 0
FiberPrebundle.continuousOn_of_comp_rightstatement and proof · cited by 0