setToSimpleFunc_mono_left — Mathlib

English

If T and T' are pointwise equal on all measurable s with μ(s) finite, f is integrable, then setToSimpleFunc T f = setToSimpleFunc T' f.

Русский

Если T и T' равны по точкам на всех измеримых s с конечной μ(s), f интегрируема, тогда setToSimpleFunc T f = setToSimpleFunc T' f.

LaTeX

$$$ \forall s, MeasurableSet s, μ s < \infty \Rightarrow T s = T' s \Rightarrow setToSimpleFunc T f = setToSimpleFunc T' f $$$

Lean4

theorem setToSimpleFunc_mono_left {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] G'') (hTT' : ∀ s x, T s x ≤ T' s x)
    (f : α →ₛ F) : setToSimpleFunc T f ≤ setToSimpleFunc T' f := by simp_rw [setToSimpleFunc];
  exact sum_le_sum fun i _ => hTT' _ i

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