setToSimpleFunc_smul_left — Mathlib

English

Scaling on the left commutes with setToSimpleFunc: setToSimpleFunc (c • T) f = c • setToSimpleFunc T f.

Русский

Умножение слева на T переносится через setToSimpleFunc: setToSimpleFunc (c • T) f = c • setToSimpleFunc T f.

LaTeX

$$$ setToSimpleFunc (\lambda s, c \cdot T s) f = c \cdot setToSimpleFunc T f $$$

Lean4

theorem setToSimpleFunc_smul_left {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (c : ℝ) (f : α →ₛ F) :
    setToSimpleFunc (fun s => c • T s) f = c • setToSimpleFunc T f := by
  simp_rw [setToSimpleFunc, ContinuousLinearMap.smul_apply, smul_sum]

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