contMDiffWithinAt_iff — Mathlib

English

Reiterates that the symmetric trans map between trivializations is C^n on the intersection of their targets.

Русский

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

LaTeX

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

Lean4

theorem contMDiffWithinAt_iff {f : M → TotalSpace F E} {s : Set M} {x₀ : M} (he : f x₀ ∈ e.source) :
    ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔
      ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧
        ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) s x₀ :=
  contMDiffWithinAt_totalSpace.trans <|
    and_congr_right fun h ↦
      Trivialization.contMDiffWithinAt_snd_comp_iff₂ h FiberBundle.mem_trivializationAt_proj_source he

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