mdifferentiableOn_symm_coordChangeL

English

The coordinate change map is differentiable on the base intersection, as a linear map.

Русский

Координатное преобразование гладко дифференцируемо на пересечении базовых множеств как линейное отображение.

LaTeX

$$$$MDifferentiableOn IB 𝓘(\mathbb{k}, F \to_L[\mathbb{k}] F) (fun b: B \mapsto (e.coordChangeL 𝕜 e' b)) (e.baseSet \cap e'.baseSet).$$$$

Lean4

theorem mdifferentiableOn_symm_coordChangeL :
    MDifferentiableOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B ↦ ((e.coordChangeL 𝕜 e' b).symm : F →L[𝕜] F))
      (e.baseSet ∩ e'.baseSet) :=
  (contMDiffOn_symm_coordChangeL e e').mdifferentiableOn le_rfl

Похожие утверждения