inner — Mathlib

English

If f and g are ContDiff Real n, then x ↦ ⟪f x, g x⟫ is ContDiff Real n.

Русский

Если f и g — ContDiff Real n, то x ↦ ⟪f x, g x⟫ является ContDiff Real n.

LaTeX

$$$\\operatorname{ContDiff}_{\\mathbb{R}} n\\ (f,g) \\Rightarrow \\operatorname{ContDiff}_{\\mathbb{R}} n\\ (x \\mapsto \\langle f(x), g(x)\\rangle).$$$

Lean4

theorem inner (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x) :
    ContDiffWithinAt ℝ n (fun x => ⟪f x, g x⟫) s x :=
  contDiffAt_inner.comp_contDiffWithinAt x (hf.prodMk hg)

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