coe_smul' — Mathlib

English

The pointwise smul of a scalar-valued map f with a vector-valued map g equals the map obtained by smul-ing their values pointwise: (f • g)(x) = f(x) • g(x).

Русский

Пусть f ∈ C(α,R) и g ∈ C(α,M). Тогда (f • g)(x) = f(x) • g(x).

LaTeX

$$$ (f \\cdot g)(x) = f(x) \\cdot g(x). $$$

Lean4

/-- Coercion to a function for a scalar-valued continuous map multiplying a vector-valued one
(as opposed to `ContinuousMap.coe_smul` which is multiplication by a constant scalar). -/
@[simp]
theorem coe_smul' (f : C(α, R)) (g : C(α, M)) : ⇑(f • g) = ⇑f • ⇑g :=
  rfl

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