Theorems · Theorem · algebraic topology

FiberBundleCore.continuous_proj

∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F), Continuous Z.proj

The projection on the base of a fiber bundle created from core is continuous

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

1 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace