English
Both local trivializations generate an equivalence of the appropriate partial domains, respecting the coordinate changes.
Русский
Обе локальные тривиализации порождают эквиваленцию на соответствующих частичных областях, соблюдая координатные изменения.
LaTeX
$$$(Z.localTrivAsPartialEquiv i).trans (Z.localTrivAsPartialEquiv j) \\approx (Z.trivChange i j).toPartialEquiv$$$
Lean4
/-- If an element of `F` is invariant under all coordinate changes, then one can define a
corresponding section of the fiber bundle, which is continuous. This applies in particular to the
zero section of a vector bundle. Another example (not yet defined) would be the identity
section of the endomorphism bundle of a vector bundle. -/
theorem continuous_const_section (v : F) (h : ∀ i j, ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v) :
Continuous (show B → Z.TotalSpace from fun x => ⟨x, v⟩) :=
by
refine continuous_iff_continuousAt.2 fun x => ?_
have A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x := IsOpen.mem_nhds (Z.isOpen_baseSet (Z.indexAt x)) (Z.mem_baseSet_at x)
refine ((Z.localTrivAt x).toOpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_
· exact A
· apply continuousAt_id.prodMk
simp only [mfld_simps]
have : ContinuousOn (fun _ : B => v) (Z.baseSet (Z.indexAt x)) := continuousOn_const
refine (this.congr fun y hy ↦ ?_).continuousAt A
exact h _ _ _ ⟨mem_baseSet_at _ _, hy⟩
