comp_contMDiffWithinAt — Mathlib

English

A map f between model-with-corners spaces is ContMDiff of order n iff it is ContDiff of order n globally.

Русский

Отображение между моделями с углами является ContMDiff порядка n тогда и тогда, когда оно глобально ContDiff порядка n.

LaTeX

$$$\ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f \iff \ContDiff 𝕜 n f$$$

Lean4

theorem comp_contMDiffWithinAt {g : F → F'} {f : M → F} {s : Set M} {x : M} (hg : ContDiff 𝕜 n g)
    (hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x) : ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s x :=
  hg.contDiffAt.comp_contMDiffWithinAt hf

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