English
If a C^n section f, written in total space coordinates, is ContMDiff within a set s, then changing the section via a trivialization yields a C^n section with respect to the new trivialization, provided the basepoint lies in the source region of the trivialization.
Русский
Гладкость секции сохраняется под сменой секции через тривиализацию.
LaTeX
$$$$\\text{ContMDiffWithinAt }(\\text{section change})\\text{ по тривиализации}$$$$
Lean4
theorem change_section_trivialization {f : M → TotalSpace F E} (hp : ContMDiffWithinAt IM IB n (π F E ∘ f) s x)
(hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (e (f y)).2) s x) (he : f x ∈ e.source) (he' : f x ∈ e'.source) :
ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (e' (f y)).2) s x :=
by
rw [Trivialization.mem_source] at he he'
refine (hp.coordChange hf he he').congr_of_eventuallyEq ?_ ?_
· filter_upwards [hp.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
rw [Function.comp_apply, e.coordChange_apply_snd _ hy]
· rw [Function.comp_apply, e.coordChange_apply_snd _ he]
