contMDiffOn — Mathlib

English

Given a VectorBundleCore with IsContMDiff, the coordinate change maps between two trivializations are C^n on their base intersection.

Русский

Переход координат гладок.

LaTeX

$$$$\\text{ContMDiffOn }\\big( Z.coordChange \\big)\\; (Z.baseSet i \\cap Z.baseSet j) $$$$

Lean4

theorem contMDiffOn (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n e e.source :=
  by
  have : ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id e.source := contMDiffOn_id
  rw [e.contMDiffOn_iff (mapsTo_id _)] at this
  exact (this.1.prodMk this.2).congr fun x hx ↦ (e.mk_proj_snd hx).symm

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