English
Under the same setup, the differentiability of the composed fiber-section remains preserved after adjusting via different trivializations, given appropriate conditions on x and base sets.
Русский
При той же конфигурации сохраняется дифференцируемость секции после перехода через другую тривиализацию, при условии корректных попаданий в базовые множества.
LaTeX
$$$\text{If } hf : MDifferentiableWithinAt IM IB f s x,\; he, he' \text{ as base-set conditions, then } MDifferentiableWithinAt IM 𝓘(\mathbb{K}, F) (\lambda y. e' (f y)) s x.$$$
Lean4
theorem change_section_trivialization {e : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e]
{e' : Trivialization F TotalSpace.proj} [MemTrivializationAtlas e'] {f : M → TotalSpace F E} {s : Set M} {x₀ : M}
(hf : MDifferentiableWithinAt IM IB (π F E ∘ f) s x₀)
(he'f : MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) s x₀) (he : f x₀ ∈ e.source)
(he' : f x₀ ∈ e'.source) : MDifferentiableWithinAt IM 𝓘(𝕜, F) (fun x ↦ (e' (f x)).2) s x₀ :=
by
rw [Trivialization.mem_source] at he he'
refine (hf.coordChange he'f he he').congr_of_eventuallyEq ?_ ?_
· filter_upwards [hf.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
rw [Function.comp_apply, e.coordChange_apply_snd e' hy]
· rw [Function.comp_apply, e.coordChange_apply_snd _ he]
