Theorems · Theorem · algebraic topology

FiberBundle.continuousAt_totalSpace

∀ {B : Type u_2} (F : Type u_3) {X : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace F] {E : B → Type u_5} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (b : B) → TopologicalSpace (E b)] [inst_5 : FiberBundle F E] (f : X → Bundle.TotalSpace F E) {x₀ : X},
  ContinuousAt f x₀ ↔
    ContinuousAt (fun x => (f x).proj) x₀ ∧ ContinuousAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Characterization of continuous functions (at a point) into a fiber bundle.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundle