Theorems · Definition · algebraic topology

FiberBundle.trivializationAtlas

{B : Type u_2} →
  (F : Type u_3) →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        (E : B → Type u_5) →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] →
              [FiberBundle F E] → Set (Bundle.Trivialization F Bundle.TotalSpace.proj)

Atlas of a fiber bundle.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

5 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundle