Commit 2020-10-23 05:47 ff711a31

feat(measure_theory/measure_space): Added lemmas for commuting restrict for outer measures and measures (#4673) This also adds of_function_apply and Inf_apply (for outer_measure). I had some difficulty getting these functions to expand (as represented by the length of Inf_apply) in a clean way. I also think Inf_apply is instructive in terms of making it clear what the definition of Inf is. Once Inf is rewritten, then the large set of operations available for infi_le and le_infi (and ennreal.tsum_le_tsum) can be used. measure.restrict_Inf_eq_Inf_restrict will be helpful in getting more results about the subtraction of measures, specifically writing down the result of (a - b) when a is not less than or equal to b and b is not less than or equal to a.