Commit 2022-01-15 17:32 37cf695a

feat(measure_theory/integral/set_to_l1): monotonicity properties of set_to_fun (#10714) We prove that in a normed_lattice_add_comm_group, if T is such that 0 ≤ T s x for 0 ≤ x, then set_to_fun μ T verifies

• set_to_fun_mono_left (h : ∀ s x, T' s x ≤ T'' s x) : set_to_fun μ T' hT' f ≤ set_to_fun μ T'' hT'' f
• set_to_fun_nonneg (hf : 0 ≤ᵐ[μ] f) : 0 ≤ set_to_fun μ T hT f
• set_to_fun_mono (hfg : f ≤ᵐ[μ] g) : set_to_fun μ T hT f ≤ set_to_fun μ T hT g