smul_apply' — Mathlib

English

For f ∈ C(α,R) and g ∈ C(α,M), (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

/-- Evaluation of a scalar-valued continuous map multiplying a vector-valued one
(as opposed to `ContinuousMap.smul_apply` which is multiplication by a constant scalar). -/
-- (this doesn't need to be @[simp] since it can be derived from `coe_smul'` and `Pi.smul_apply'`)

theorem smul_apply' (f : C(α, R)) (g : C(α, M)) (x : α) : (f • g) x = f x • g x :=
  rfl

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