fun_comp — Mathlib

English

The composition of C^n functions is C^n: if hg : ContDiff 𝕜 n g and hf : ContDiff 𝕜 n f, then ContDiff 𝕜 n (g ∘ f).

Русский

Тождество гладкости: если g и f — C^n, то g∘f — C^n.

LaTeX

$$$ \operatorname{ContDiff}_{\mathbb{K}}^{n} g \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n} f \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n} (g \circ f)$$$

Lean4

@[fun_prop]
theorem fun_comp {g : F → G} {f : E → F} (hg : ContDiff 𝕜 n g) (hf : ContDiff 𝕜 n f) :
    ContDiff 𝕜 n (fun x => g (f x)) :=
  hg.comp hf

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