Theorems · Inductive type · algebraic topology

FiberBundle

{B : Type u_2} →
  (F : Type u_3) →
    [TopologicalSpace B] →
      [TopologicalSpace F] →
        (E : B → Type u_5) →
          [TopologicalSpace (Bundle.TotalSpace F E)] → [(b : B) → TopologicalSpace (E b)] → Type (max (max u_2 u_3) u_5)

A (topological) fiber bundle with fiber F over a base B is a space projecting on B for which the fibers are all homeomorphic to F, such that the local situation around each point is a direct product.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

471 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpace