English
If a ContMDiff structure holds on the base and fiberwise linear maps, the induced global transformation on the product B×F is ContMDiff of class n; the fiberwise structure respects the base identity.
Русский
Если есть структура гладкости типа C^n на основании и по волокнам, индуцированное глобальное преобразование на произведении B×F гладко в классе n; волокновая структура совместима с идентичностью по основанию.
LaTeX
$$$\\{e\\} \\text{ is a ContMDiff fiberwise linear partial homeomorphism }$$$
Lean4
theorem contMDiffOn_continuousLinearMapCoordChange [ContMDiffVectorBundle n F₁ E₁ IB] [ContMDiffVectorBundle n F₂ E₂ IB]
[MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] :
ContMDiffOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n (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 := n)
have h₂ := contMDiffOn_coordChangeL (IB := IB) e₂ e₂' (n := n)
refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_) <;> mfld_set_tac
