English
If a vector bundle has a zero section, then it is ContMDiff under a broad class of differentiability assumptions globally.
Русский
Если существует нулевая секция, то она гладкая в глобальном смысле под соответствующими предположениями.
LaTeX
$$$\text{ContMDiff } IB \; (IB. prod 𝓘(𝕜, F))\; n (zeroSection F E)$$$
Lean4
protected theorem coordChange (hf : ContMDiffWithinAt IM IB n f s x) (hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x)
(he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) :
ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ e.coordChange e' (f y) (g y)) s x :=
by
refine ((hf.coordChangeL he he').clm_apply hg).congr_of_eventuallyEq ?_ ?_
· have : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x) := (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨he, he'⟩
filter_upwards [hf.continuousWithinAt this] with y hy
exact (Trivialization.coordChangeL_apply' e e' hy (g y)).symm
· exact (Trivialization.coordChangeL_apply' e e' ⟨he, he'⟩ (g x)).symm
