Theorems · Definition · algebraic topology

Bundle.Trivialization.symm

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

A fiberwise inverse to e'. The function F → E x that induces a local inverse B × F → TotalSpace F E of e' on e'.baseSet. It takes on junk values chosen using Classical.arbitrary outside e'.baseSet.

Defined in

Mathlib.Topology.FiberBundle.Trivialization

Cited by

37 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceNonempty