Theorems · Definition · algebraic topology

MemTrivializationAtlas.casesOn

{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)] →
              [inst_4 : FiberBundle F E] →
                {e : Bundle.Trivialization F Bundle.TotalSpace.proj} →
                  {motive : MemTrivializationAtlas e → Sort u} →
                    (t : MemTrivializationAtlas e) → ((out : e ∈ trivializationAtlas F E) → motive ⋯) → motive t

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

3 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundle