English
The smoothness around a point is characterized by the combination of base projection smoothness and fiber-slice smoothness through the trivialization.
Русский
Гладкость локально задается через проекцию и координаты волокна.
LaTeX
$$$$\\text{contMDiffAt }(f)\\iff \\text{contMDiffWithinAt }(f.fst) \\land \\text{contMDiffWithinAt }(f.snd).$$$$
Lean4
/-- Smoothness of a `C^n` section on `s` can be determined
using any trivialisation whose `baseSet` contains `s`. -/
theorem contMDiffOn_section_iff {s : ∀ x, E x} {a : Set B}
(e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B)) [MemTrivializationAtlas e]
(ha : IsOpen a) (ha' : a ⊆ e.baseSet) :
ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a ↔
ContMDiffOn IB 𝓘(𝕜, F) n (fun x ↦ (e ⟨x, s x⟩).2) a :=
by
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩ <;> have := (h x hx).contMDiffAt <| ha.mem_nhds hx
· exact ((e.contMDiffAt_section_iff (ha' hx)).mp this).contMDiffWithinAt
· exact ((e.contMDiffAt_section_iff (ha' hx)).mpr this).contMDiffWithinAt
