contMDiffAt_iff — Mathlib

English

For a trivialization e, the ContMDiffWithinAt condition for a function pulled back via the total space decomposes into the pair: base projection regularity and fiber coordinate regularity with respect to e.

Русский

Гладкость секции внутри множества определяется через проекцию и волокно-базисную координату.

LaTeX

$$$$\\text{ContMDiffWithinAt }(f)\\iff (\\text{ContMDiffWithinAt }(f.{proj})\\wedge \\text{ContMDiffWithinAt }(f.snd))$$$$

Lean4

theorem contMDiffAt_iff {f : M → TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) :
    ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔
      ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧ ContMDiffAt IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) x₀ :=
  e.contMDiffWithinAt_iff he

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