comp_contMDiffWithinAt — Mathlib

English

If g is ContDiffWithinAt and f is ContMDiffWithinAt, then g∘f is ContMDiffWithinAt provided the domain aligns (s ⊆ f^{-1}(t)).

Русский

Если g гладко дифференцируема внутри и f тоже, то композиция g∘f гладко дифференцируема внутри, при условии совместимости областей.

LaTeX

$$$\text{hg: ContDiffWithinAt } 𝕜 n g t (f x)\;\land\; \text{hf: ContMDiffWithinAt } I 𝓘(𝕜,F) n f s x\;\land\; s \subseteq f^{-1}' t \;\Rightarrow\; \ContMDiffWithinAt I 𝓘(𝕜,F') n (g \circ f) s x$$$

Lean4

theorem comp_contMDiffWithinAt {g : F → F'} {f : M → F} {s : Set M} {t : Set F} {x : M}
    (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x) (h : s ⊆ f ⁻¹' t) :
    ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s x :=
  hg.contMDiffWithinAt.comp x hf h

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