mathlib

37cf695a - feat(measure_theory/integral/set_to_l1): monotonicity properties of set_to_fun (#10714)

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`