inner — Mathlib

English

If f,g are differentiable on s, then x ↦ ⟪f x, g x⟫ is differentiable on s.

Русский

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

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{R}} f s \\ \\wedge\\ \\text{DifferentiableOn}_{\\mathbb{R}} g s \\Rightarrow \\text{DifferentiableOn}_{\\mathbb{R}} (x \\mapsto \\langle f x, g x\\rangle) s$$$

Lean4

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

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