Theorems · Inductive type · algebraic topology

FiberPrebundle

{B : Type u_2} →
  (F : Type u_3) →
    (E : B → Type u_5) →
      [TopologicalSpace B] → [TopologicalSpace F] → [(x : B) → TopologicalSpace (E x)] → Type (max (max u_2 u_3) u_5)

This structure permits to define a fiber bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the partial equivalences are also open partial homeomorphisms and hence local trivializations.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

16 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace