English
The local smoothness of a section at a point x0 (in bundle total space coordinates) is equivalent to the smoothness of its base projection and its fiber coordinate in the trivialization.
Русский
Гладкость секции в точке равна сочетанию гладкости проекции и волокна.
LaTeX
$$$$\\text{contMDiffAt }(f) \\iff (\\text{contMDiffAt }(f.fst) \\wedge \\text{contMDiffAt }(f.snd))$$$$
Lean4
/-- Smoothness of a `C^n` section at `x₀` can be determined
using any trivialisation whose `baseSet` contains `x₀`. -/
theorem contMDiffAt_section_iff {s : ∀ x, E x} {x₀ : B}
(e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B)) [MemTrivializationAtlas e]
(hx₀ : x₀ ∈ e.baseSet) :
ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x₀ ↔
ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (e ⟨x, s x⟩).2) x₀ :=
by
simp_rw [← contMDiffWithinAt_univ]
exact e.contMDiffWithinAt_section univ hx₀
