contMDiffOn_symm_coordChangeL — Mathlib

English

The symmetrized coordChangeL map is ContMDiffOn, mapping base points to continuous linear maps on the fibre.

Русский

Симметрированное отображение coordChangeL гладко на базе, отображая точку в линейный преобразователь волокна.

LaTeX

$$$\operatorname{contMDiffOn_coordChangeL} e' e\;:\; \text{Set}$$$

Lean4

theorem contMDiffOn_symm_coordChangeL :
    ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => ((e.coordChangeL 𝕜 e' b).symm : F →L[𝕜] F))
      (e.baseSet ∩ e'.baseSet) :=
  by
  rw [inter_comm]
  refine (ContMDiffVectorBundle.contMDiffOn_coordChangeL e' e).congr fun b hb ↦ ?_
  rw [e.symm_coordChangeL e' hb]

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