Theorems · Definition · algebraic topology

FiberBundleCore.TotalSpace

{ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → Type (max u_2 u_3)

The total space of the fiber bundle, as a convenience function for dot notation. It is by definition equal to Bundle.TotalSpace F Z.Fiber.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

23 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace