English
Characterize when a section x ↦ TotalSpace.mk' F x (s x) of a vector bundle is C^n on a subset a of the base space. This occurs precisely when, in a fixed base point x0, the map x ↦ (trivializationAt F E x0 ⟨x, s x⟩).2 is C^n on a.
Русский
Характеризуйте, когда секция x ↦ TotalSpace.mk' F x (s x) векторного расслоения является C^n на подмножестве a базового пространства: это происходит тогда, когда в точке x0 отображение x ↦ (trivializationAt F E x0 ⟨x, s x⟩).2 является C^n на a.
LaTeX
$$$\displaystyle \operatorname{ContMDiffWithinAt} IB (IB. prod \; 𝓘(\mathit{𝕜}, F))\; n\; (\\lambda x, TotalSpace.mk' F x (s x))\ a\ x_0 \,\leftrightarrow\, \operatorname{ContMDiffWithinAt} IB 𝓘(\mathit{𝕜}, F)\; n\; (\\lambda x, (trivializationAt F E x_0 \, ⟨x, s x⟩).2)\ a\ x_0.$$
Lean4
/-- Characterization of `C^n` sections within a set at a point of a vector bundle. -/
theorem contMDiffWithinAt_section {s : ∀ x, E x} {a : Set B} {x₀ : B} :
ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a x₀ ↔
ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (trivializationAt F E x₀ ⟨x, s x⟩).2) a x₀ :=
by simp_rw [contMDiffWithinAt_totalSpace, and_iff_right_iff_imp]; intro; exact contMDiffWithinAt_id
