comp_contMDiffWithinAt — Mathlib

English

If g is ContDiffAt and f is ContMDiffWithinAt, then g∘f is ContMDiffWithinAt.

Русский

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

LaTeX

$$$\text{hg: ContDiffAt } 𝕜 n g (f x)\;\land\; \text{hf: ContMDiffWithinAt } I 𝓘(𝕜, F) n f s x\Rightarrow\; \ContMDiffWithinAt I 𝓘(𝕜, F') n (g \circ f) s x$$$

Lean4

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

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