mathlib

ff711a31 - feat(measure_theory/measure_space): Added lemmas for commuting restrict for outer measures and measures (#4673)

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`. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>