setToL1S_mono — Mathlib

English

If c ∈ R, then setToL1S (c • T) f = c • setToL1S T f.

Русский

Если c вещественное, то setToL1S (c • T) f = c • setToL1S T f.

LaTeX

$$$$setToL1S (\lambda s. c \cdot T(s)) (f) = c \cdot setToL1S T f.$$$$

Lean4

theorem setToL1S_mono (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T)
    (hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f g : α →₁ₛ[μ] G''} (hfg : f ≤ g) :
    setToL1S T f ≤ setToL1S T g := by
  rw [← sub_nonneg] at hfg ⊢
  rw [← setToL1S_sub h_zero h_add]
  exact setToL1S_nonneg h_zero h_add hT_nonneg hfg

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