Commit 2021-09-24 11:04 854e5c6b

refactor(measure_theory/measure/regular): add inner_regular, outer_regular, generalize (#9283)

Regular measures

• add a non-class predicate inner_regular to prove some lemmas once, not twice;
• add TC outer_regular, drop primed lemmas;
• consistently use ≠ ∞, ≠ 0 in the assumptions;
• drop some typeclass requirements.

Other changes

• add a few lemmas about subtraction to data.real.ennreal;
• add ennreal.add_lt_add_left, ennreal.add_lt_add_right, and use them;