inner — Mathlib

English

If f,g are ContDiffOn Real n on s, then x ↦ ⟪f x, g x⟫ is ContDiffOn Real n on s.

Русский

Если f и g ContDiffOn Real n на области s, то x ↦ ⟪f x, g x⟫ тоже ContDiffOn Real n на s.

LaTeX

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

Lean4

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

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