Theorems · Theorem · algebraic topology

FiberBundle.continuousWithinAt_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) {s : Set X}
  {x₀ : X},
  ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧
      ContinuousWithinAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀

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

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundle