fun_comp_contDiffOn — Mathlib

English

If hg : ContDiffOn 𝕜 n g s and hf : ContDiffOn 𝕜 n f s, and MapsTo f s t, then ContDiffOn 𝕜 n (g ∘ f) s.

Русский

Если g и f — C^n на s, и MapsTo f s t, тогда g∘f — C^n на s.

LaTeX

$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} g\,t \land \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f\,s \land (mapsTo\ f\ s\ t) \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} (g \circ f)\,s$$$

Lean4

@[fun_prop]
theorem fun_comp_contDiffOn {s : Set E} {g : F → G} {f : E → F} (hg : ContDiff 𝕜 n g) (hf : ContDiffOn 𝕜 n f s) :
    ContDiffOn 𝕜 n (fun x => g (f x)) s :=
  (contDiffOn_univ.2 hg).comp hf (mapsTo_univ _ _)

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