instSMul' — Mathlib

English

There is a natural SMul action of C(α,R) on C(α,M) defined pointwise: (f · g)(x) = f(x) · g(x).

Русский

Существует естественное действие скаляров: C(α,R) на C(α,M), определяемое по точкам: (f · g)(x) = f(x) · g(x).

LaTeX

$$$\\text{instSMul'}: SMul\\ (C(α,R))\\ (C(α,M))$, \\; (f,g) \\mapsto (x \\mapsto f(x) \\cdot g(x)).$$$

Lean4

instance instSMul' : SMul C(α, R) C(α, M) :=
  ⟨fun f g => ⟨fun x => f x • g x, Continuous.smul f.2 g.2⟩⟩

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