inner — Mathlib

English

For f,g: G→E, ContDiffAt Real n f x and ContDiffAt Real n g x imply ContDiffAt Real n (λx, ⟪f x, g x⟫) x.

Русский

Для функций f,g: G→E, если f и g ContDiffAt Real n в точке x, то ⟪f,g⟫ на точке x также ContDiffAt Real n.

LaTeX

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

Lean4

nonrec theorem inner (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) : ContDiffAt ℝ n (fun x => ⟪f x, g x⟫) x :=
  hf.inner 𝕜 hg

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