English
Equivalence of differentiability of the fiber-coordinate map under two trivializations at a point when the base point lies in both base sets.
Русский
Эквивалентность дифференцируемости координатного отображения волокна при двух тривиализациях в точке, если основание принадлежит обоим базовым множествам.
LaTeX
$$$\displaystyle MDifferentiableAt IM 𝓘(\mathbb{K}, F) (\lambda x. (e (f x)).2) x \iff MDifferentiableAt IM 𝓘(\mathbb{K}, F) (\lambda x. (e' (f x)).2) x.$$$
Lean4
/-- Differentiability of a section on `s` can be determined
using any trivialisation whose `baseSet` contains `s`. -/
theorem mdifferentiableOn_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) :
MDifferentiableOn IB (IB.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (s x)) a ↔
MDifferentiableOn IB 𝓘(𝕜, F) (fun x ↦ (e ⟨x, s x⟩).2) a :=
by
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩ <;> have := (h x hx).mdifferentiableAt <| ha.mem_nhds hx
· exact ((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mp this).mdifferentiableWithinAt
· exact ((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mpr this).mdifferentiableWithinAt
