dotProduct — Mathlib

English

If A,B: X → n → R are continuous, then their dot product A(x) ⬝ᵥ B(x) is continuous in x.

Русский

Если A,B: X → n → R непрерывны, то их скалярное произведение A(x) ⬝ᵥ B(x) непрерывно по x.

LaTeX

$$$\\operatorname{Continuous}(A) \\rightarrow \\operatorname{Continuous}(B) \\rightarrow \\operatorname{Continuous}(x \\mapsto A(x) \\;\\cdot\\; B(x)).$$$

Lean4

@[continuity, fun_prop]
protected theorem dotProduct [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A : X → n → R}
    {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun x => A x ⬝ᵥ B x :=
  by
  dsimp only [dotProduct]
  fun_prop

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