comp_contMDiff — Mathlib

English

Let g: F → F' be ContDiff of order n and f: M → F be ContMDiff of order n. Then the composition g ∘ f: M → F' is ContMDiff of order n.

Русский

Пусть g: F → F' гладко(n) и f: M → F гладко(n). Тогда композиция g ∘ f: M → F' гладкая порядка n.

LaTeX

$$$\\displaystyle \\text{If } g: F \\to^{} F' \\text{ is ContDiff } 𝕜\\, n \\text{ and } f: M \\to F \\text{ is ContMDiff } I \\; 𝓘(𝕜,F)\\, n,\\ \\text{then } g \\circ f: M \\to F' \\text{ is ContMDiff } I \\; 𝓘(𝕜,F')\\, n.$$$

Lean4

theorem comp_contMDiff {g : F → F'} {f : M → F} (hg : ContDiff 𝕜 n g) (hf : ContMDiff I 𝓘(𝕜, F) n f) :
    ContMDiff I 𝓘(𝕜, F') n (g ∘ f) := fun x => hg.contDiffAt.comp_contMDiffAt (hf x)

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