comp_contMDiffAt — Mathlib

English

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

Русский

Если g гладко в точке и f гладко в точке в смысле MDiff, то композиция g∘f гладко в точке.

LaTeX

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

Lean4

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

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