comp₂_contDiffWithinAt — Mathlib

English

If g is ContDiffAt, and f1, f2 are ContDiffAt, then x ↦ g(f1(x), f2(x)) is ContDiffAt.

Русский

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

LaTeX

$$$\mathrm{ContDiffAt}_{\mathbb{k}}\ n\ g \Rightarrow \mathrm{ContDiffAt}_{\mathbb{k}}\ n\ (x \mapsto g(f_1(x), f_2(x)))$ при условиях на f1, f2.$$

Lean4

theorem comp₂_contDiffWithinAt {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {s : Set F} {x : F}
    (hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x)) (hf₁ : ContDiffWithinAt 𝕜 n f₁ s x) (hf₂ : ContDiffWithinAt 𝕜 n f₂ s x) :
    ContDiffWithinAt 𝕜 n (fun x => g (f₁ x, f₂ x)) s x :=
  hg.comp_contDiffWithinAt x (hf₁.prodMk hf₂)

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