setToFun_mono_left — Mathlib

English

If hT and hT' are dominated FinMeasAdditive measures, and hTT' gives T ≤ T' pointwise, then for f ∈ α → E (μ-a.e.), setToFun μ T hT f ≤ setToFun μ T' hT' f.

Русский

Если hT и hT' задают ограниченные меры типа dominated FinMeasAdditive, и T ≤ T' по точкам, то для любого f ∈ L¹(μ) выполняется неравенство setToFun μ T hT f ≤ setToFun μ T' hT' f.

LaTeX

$$$$ \mathrm{setToFun}\ \mu\ T\ hT\ f \le \mathrm{setToFun}\ \mu\ T'\ hT'\ f. $$$$

Lean4

theorem setToFun_mono_left {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ s x, T s x ≤ T' s x) (f : α →₁[μ] E) :
    setToFun μ T hT f ≤ setToFun μ T' hT' f :=
  setToFun_mono_left' hT hT' (fun s _ _ x => hTT' s x) f

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