Theorems · Inductive type · algebraic topology

MemTrivializationAtlas

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

Given a type E equipped with a fiber bundle structure, this is a Prop typeclass for trivializations of E, expressing that a trivialization is in the designated atlas for the bundle. This is needed because lemmas about the linearity of trivializations or the continuity (as functions to F →L[R] F, where F is the model fiber) of the transition functions are only expected to hold for trivializations in the designated atlas.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

108 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 6 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundle