setToL1_smul — Mathlib

English

If for all measurable s with finite measure, T' s = c · T s, then for f ∈ L1, setToL1 hT' f = c · setToL1 hT f.

Русский

Если для каждой измеримой области s с μ(s)<∞ выполняется T' s = c · T s, тогда для f ∈ L1 имеет место setToL1 hT' f = c · setToL1 hT f.

LaTeX

$$$setToL1\, h_T'\, f = c \,\cdot setToL1\, h_T\, f,$$$

Lean4

theorem setToL1_smul (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜)
    (f : α →₁[μ] E) : setToL1 hT (c • f) = c • setToL1 hT f :=
  by
  rw [setToL1_eq_setToL1' hT h_smul, setToL1_eq_setToL1' hT h_smul]
  exact ContinuousLinearMap.map_smul _ _ _

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