English
The contMDiff status of the section within a set translates to the contMDiff status of its trivialized fibre coordinate within that set.
Русский
Состояние гладкости секции внутри множества эквивалентно гладкости координаты волокна в этой же области при тривиализации.
LaTeX
$$$\displaystyle ContMDiffWithinAt IB (IB. prod 𝓘(𝕜, F)) n (\lambda x. TotalSpace.mk' F x (s x)) a x_0 \iff \dots$$$
Lean4
theorem contMDiff_zeroSection : ContMDiff IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) :=
by
intro x
unfold zeroSection
rw [contMDiffAt_section]
apply (contMDiffAt_const (c := 0)).congr_of_eventuallyEq
filter_upwards [(trivializationAt F E x).open_baseSet.mem_nhds (mem_baseSet_trivializationAt F E x)] with y hy using
congr_arg Prod.snd <| (trivializationAt F E x).zeroSection 𝕜 hy
