English
If a map f: M → LE1E2 is mdifferentiable within a set s at x0, then the pair of its components are mdifferentiable within at x0 on s, and the coordinates are mdifferentiable too.
Русский
Если отображение f: M → LE1E2 дифференцируемо внутри множества s в точке x0, то оба компонента и координаты дифференцируемы внутри на x0.
LaTeX
$$$\\text{mdiffWithinAt}(f,x0) \\iff \\text{mdiffWithinAt}(f|_{base},x0) \\land \\text{mdiffWithinAt}(coordinates, x0)$$$
Lean4
theorem mdifferentiableOn_continuousLinearMapCoordChange [ContMDiffVectorBundle 1 F₁ E₁ IB]
[ContMDiffVectorBundle 1 F₂ E₂ IB] [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁']
[MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] :
MDifferentiableOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂)
(continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
(e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)) :=
by
have h₁ := contMDiffOn_coordChangeL (IB := IB) e₁' e₁ (n := 1) |>.mdifferentiableOn le_rfl
have h₂ := contMDiffOn_coordChangeL (IB := IB) e₂ e₂' (n := 1) |>.mdifferentiableOn le_rfl
refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_) <;> mfld_set_tac
