English
If T ≤ T' pointwise, then for any integrable f, setToFun μ T hT f ≤ setToFun μ T' hT' f.
Русский
Если T(s,x) ≤ T'(s,x) по всем s,x, то для интегрируемого f выполняется setToFun(μ,T) hT f ≤ setToFun(μ,T') hT' f.
LaTeX
$$$\forall f,\;\text{Integrable } f\; \Rightarrow \mathrm{setToFun}(\mu, T) h_T f \le \mathrm{setToFun}(\mu, T') h_{T'} f$$$
Lean4
theorem setToFun_mono [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f g : α → G'} (hf : Integrable f μ)
(hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) : setToFun μ T hT f ≤ setToFun μ T hT g :=
by
rw [← sub_nonneg, ← setToFun_sub hT hg hf]
refine setToFun_nonneg hT hT_nonneg (hfg.mono fun a ha => ?_)
rw [Pi.sub_apply, Pi.zero_apply, sub_nonneg]
exact ha
