comp₂ — Mathlib

English

If g is C^n, and f1, f2 are C^n, then x ↦ g(f1(x), f2(x)) is C^n.

Русский

Если g — C^n, а f1, f2 — C^n, то x ↦ g(f1(x), f2(x)) — C^n.

LaTeX

$$$\mathrm{ContDiff}_{\mathbb{k}}\ n\ g \land \mathrm{ContDiff}_{\mathbb{k}}\ n\ f_1 \land \mathrm{ContDiff}_{\mathbb{k}}\ n\ f_2 \Rightarrow \mathrm{ContDiff}_{\mathbb{k}}\ n\ (x \mapsto g(f_1(x), f_2(x))).$$$

Lean4

theorem comp₂ {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} (hg : ContDiff 𝕜 n g) (hf₁ : ContDiff 𝕜 n f₁)
    (hf₂ : ContDiff 𝕜 n f₂) : ContDiff 𝕜 n fun x => g (f₁ x, f₂ x) :=
  hg.comp <| hf₁.prodMk hf₂

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