comp₂_contDiffAt — Mathlib

English

If g: E1 × E2 × E3 → G is ContDiffAt and f1, f2, f3 are ContDiffAt, then x ↦ g(f1(x), f2(x), f3(x)) is ContDiffAt.

Русский

Если g: E1 × E2 × E3 → G гладко порядка n в точке, и f1, f2, f3 гладкие порядка n, то x ↦ g(f1(x), f2(x), f3(x)) гладко порядка n.

LaTeX

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

Lean4

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

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