Theorems · Definition · algebraic topology

FiberBundle.trivializationAt

{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] → B → Bundle.Trivialization F Bundle.TotalSpace.proj

Trivialization of a fiber bundle at a point.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

95 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 7 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundle