contMDiffOn_iff — Mathlib

English

The two implications form an equivalence between ContMDiffWithinAt statements for the fiber coordinates with respect to e and e'.

Русский

Согласованы два условия гладкости при двух тривиализациях.

LaTeX

$$$$\\text{ContMDiffWithinAt }(f)\\text{ по }(e\\,f)\\iff \\text{ContMDiffWithinAt }(f)\\text{ по }(e'\\,f).$$$$

Lean4

theorem contMDiffOn_iff {f : M → TotalSpace F E} {s : Set M} (he : MapsTo f s e.source) :
    ContMDiffOn IM (IB.prod 𝓘(𝕜, F)) n f s ↔
      ContMDiffOn IM IB n (fun x => (f x).proj) s ∧ ContMDiffOn IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) s :=
  by
  simp only [ContMDiffOn, ← forall_and]
  exact forall₂_congr fun x hx ↦ e.contMDiffWithinAt_iff (he hx)

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