setToL1SCLM_smul_left' — Mathlib

English

If T' s = c • T s for a fixed scalar c, then applying setToL1SCLM with T' is c times the original.

Русский

Если T' s = c • T s, тогда setToL1SCLM для hT' равен c раз оригинального.

LaTeX

$$$setToL1SCLM\;α\;E\;μ\;hT'\;f = c \cdot setToL1SCLM\;α\;E\;μ\;hT\;f$$$

Lean4

theorem setToL1SCLM_smul_left' (c : ℝ) (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C')
    (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) (f : α →₁ₛ[μ] E) :
    setToL1SCLM α E μ hT' f = c • setToL1SCLM α E μ hT f :=
  setToL1S_smul_left' T T' c h_smul f

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