Instance of IsOrderedAddMonoid for Measures

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

We have MeasureTheory.Measure.instAddCommMonoid and MeasureTheory.Measure.instPartialOrder. We can use these instances to get IsOrderedAddMonoid (Measure α), and I can't find it in Mathlib. I want to double check whether we have this instance.

[Yongxi Lin (Aaron)]

https://github.com/leanprover-community/mathlib4/pull/30063

[Yury G. Kudryashov]

Thanks!

[Yury G. Kudryashov]

Please add an instance for OuterMeasures, then we can merge this PR. Also, Github warns about non-ASCII characters in the branch name. I hope that our automation will work fine with it, but I'm not 100% sure.

[Yongxi Lin (Aaron)]

Thank you for your comments. I just add this instance for OuterMeasures.