smul_comp — Mathlib

English

Left-multiplication by a scalar commutes with composition of continuous maps: (r • f) ∘ g = r • (f ∘ g).

Русский

Умножение слева скаляром и композиция функций совместимы: (r • f) ∘ g = r • (f ∘ g).

LaTeX

$$$ (r \cdot f) \circ g = r \cdot (f \circ g). $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_comp [SMul R M] [ContinuousConstSMul R M] (r : R) (f : C(β, M)) (g : C(α, β)) :
    (r • f).comp g = r • f.comp g :=
  rfl

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