inner — Mathlib

English

If f and g are differentiable at x, then the map t ↦ ⟪f t, g t⟫ is differentiable at x.

Русский

Если функции f и g дифференцируемы в точке x, то отображение t ↦ ⟪f t, g t⟫ дифференцируемо в x.

LaTeX

$$$\\text{DifferentiableAt}_{\\mathbb{R}}\\ f\\ x \\text{ and } g\\text{ implies } t \\mapsto \\langle f t, g t\\rangle \\text{ is differentiable at } x.$$$

Lean4

theorem inner (hf : DifferentiableWithinAt ℝ f s x) (hg : DifferentiableWithinAt ℝ g s x) :
    DifferentiableWithinAt ℝ (fun x => ⟪f x, g x⟫) s x :=
  (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).differentiableWithinAt

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