Theorems · Inductive type · algebraic topology

Bundle.Pretrivialization

{B : Type u_1} →
  (F : Type u_2) → {Z : Type u_4} → [TopologicalSpace B] → [TopologicalSpace F] → (Z → B) → Type (max (max u_1 u_2) u_4)

This structure contains the information left for a local trivialization (which is implemented below as Trivialization F proj) if the total space has not been given a topology, but we have a topology on both the fiber and the base space. Through the construction topological_fiber_prebundle F proj it will be possible to promote a Pretrivialization F proj to a Trivialization F proj.

Defined in

Mathlib.Topology.FiberBundle.Trivialization

Cited by

111 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace