Theorems · Definition · algebraic topology

Bundle.Pretrivialization.symm

{B : Type u_1} →
  {F : Type u_2} →
    {E : B → Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [∀ (x : B), Nonempty (E x)] → Bundle.Pretrivialization F Bundle.TotalSpace.proj → (b : B) → F → E b

A fiberwise inverse to e. This is the function F → E b that induces a local inverse B × F → TotalSpace F E of e on e.baseSet. Outside of e.baseSet it takes on arbitrarily chosen junk values.

Defined in

Mathlib.Topology.FiberBundle.Trivialization

Cited by

26 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceNonempty