English
Continuity at a point for a map into the total space is equivalent to the continuity of its base projection at that point, together with the fiber coordinate in the corresponding trivialization at the base.
Русский
Непрерывность в точке отображения в полное пространство эквивалентна непрерывности базовой проекции в точке и волоконной координаты в соответствующей тривиализации над базой.
LaTeX
$$\( ContinuousAt f x0 \iff (ContinuousAt(\lambda x. x.proj) x0) \land (ContinuousAt(\lambda x. ((\operatorname{trivializationAt}(F,E,(f x0).proj).toFun' (f x)).snd)) x0) \)$$
Lean4
/-- Characterization of continuous functions (at a point) into a fiber bundle. -/
theorem continuousAt_totalSpace (f : X → 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₀ :=
(trivializationAt F E (f x₀).proj).tendsto_nhds_iff mem_trivializationAt_proj_source
