contMDiff_iff — Mathlib

English

Re-states the contMDiffOn property for the symmetric trans map between trivializations on their intersection.

Русский

Проверяется гладкость перехода на пересечении.

LaTeX

$$$$\\text{ContMDiffOn }(e^{\\mathrm{symm}}\\circ e'^{-1})\\;\\text{on }(e.baseSet \\cap e'.baseSet).$$$$

Lean4

theorem contMDiff_iff {f : M → TotalSpace F E} (he : ∀ x, f x ∈ e.source) :
    ContMDiff IM (IB.prod 𝓘(𝕜, F)) n f ↔
      ContMDiff IM IB n (fun x => (f x).proj) ∧ ContMDiff IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) :=
  (forall_congr' fun x ↦ e.contMDiffAt_iff (he x)).trans forall_and

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