English
Continuity of a map into the total space is equivalent to the continuity of its base projection plus the fiber component in a local trivialization around the base point.
Русский
Непрерывность отображения в полное пространство эквивалентна непрерывности проекции на основание и непрерывности волоконной компоненты в окрестности базовой точки.
LaTeX
$$\( ContinuousWithinAt f s x0 \iff (ContinuousWithinAt(\lambda z. z.proj) s x0) ∧ (ContinuousWithinAt(\lambda z. ((\operatorname{trivializationAt}(F,E( f x0).proj)) (f x)).2) s x0) \)$$
Lean4
/-- Characterization of continuous functions (at a point, within a set) into a fiber bundle. -/
theorem continuousWithinAt_totalSpace (f : X → 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₀ :=
(trivializationAt F E (f x₀).proj).tendsto_nhds_iff mem_trivializationAt_proj_source
