inner — Mathlib

English

If f,g are differentiable at x, then their inner product is differentiable at x.

Русский

Если f,g дифференцируемы в x, то их скалярное произведение dx — дифференцируемо в x.

LaTeX

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

Lean4

theorem inner (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    DifferentiableAt ℝ (fun x => ⟪f x, g x⟫) x :=
  (hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).differentiableAt

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