setToL1S_smul_real — Mathlib

English

If T ≤ T' pointwise, then setToL1S T f ≤ setToL1S T' f.

Русский

Если T ≤ T' по точкам, то setToL1S T f ≤ setToL1S T' f.

LaTeX

$$$$\text{If } T(s,x) \le T'(s,x) \text{ for all } s,x,\; \text{then } setToL1S(T,f) \le setToL1S(T',f).$$$$

Lean4

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

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