Theorems · Definition · algebraic topology

FiberBundleCore.Fiber

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

The fiber of a fiber bundle core, as a convenience function for dot notation and typeclass inference

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

16 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace