setToL1S_smul — Mathlib

English

If T(s) ≤ T'(s) for all s, then setToL1S T f ≤ setToL1S T' f.

Русский

Если T(s) ≤ T'(s) для всех s, то setToL1S T f ≤ setToL1S T' f.

LaTeX

$$$$\forall s, MeasurableSet s, T(s) \le T'(s) \Rightarrow setToL1S T f \le setToL1S T' f.$$$$

Lean4

theorem setToL1S_smul [DistribSMul 𝕜 F] (T : Set α → E →L[ℝ] F) (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T) (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜) (f : α →₁ₛ[μ] E) :
    setToL1S T (c • f) = c • setToL1S T f := by
  simp_rw [setToL1S]
  rw [← SimpleFunc.setToSimpleFunc_smul T h_add h_smul c (SimpleFunc.integrable f)]
  refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_
  exact smul_toSimpleFunc c f

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