English
Continuity of the projection map on the total space is inherited from the fiber bundle construction.
Русский
Непрерывность проекции на основание наследуется от конструкции фибер-бандла.
LaTeX
$$$ \text{Continuous } Z.proj $$$
Lean4
/-- For a fiber bundle `E` over `B` constructed using the `FiberPrebundle` mechanism,
continuity of a function `TotalSpace F E → X` on an open set `s` can be checked by precomposing at
each point with the pretrivialization used for the construction at that point. -/
theorem continuousOn_of_comp_right {X : Type*} [TopologicalSpace X] {f : TotalSpace F E → X} {s : Set B} (hs : IsOpen s)
(hf :
∀ b ∈ s,
ContinuousOn (f ∘ (a.pretrivializationAt b).toPartialEquiv.symm)
((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ (Set.univ : Set F))) :
@ContinuousOn _ _ a.totalSpaceTopology _ f (π F E ⁻¹' s) :=
by
letI := a.totalSpaceTopology
intro z hz
let e : Trivialization F (π F E) := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas z.proj)
refine (e.continuousAt_of_comp_right ?_ ((hf z.proj hz).continuousAt (IsOpen.mem_nhds ?_ ?_))).continuousWithinAt
· exact a.mem_base_pretrivializationAt z.proj
· exact (hs.inter (a.pretrivializationAt z.proj).open_baseSet).prod isOpen_univ
refine ⟨?_, mem_univ _⟩
rw [e.coe_fst]
· exact ⟨hz, a.mem_base_pretrivializationAt z.proj⟩
· rw [e.mem_source]
exact a.mem_base_pretrivializationAt z.proj
