rename `cvg_mu_inc`

Open affeldt-aist opened this issue 3 years ago • 1 comments

https://github.com/math-comp/analysis/blob/82e29a05dfc54f40bf576961bec7fdd6bdfb5c34/theories/measure.v#L2278-L2282

maybe it'd better be cvg_measure_inc to avoid using the name of the variable mu

May 26 '22 05:05 affeldt-aist

maybe it'd better be cvg_measure_inc to avoid using the name of the variable mu

That's not clear because there are other lemmas that use the "mu" substring. Rather, this is the suffix _inc that is wrong; we should use nondecreasing.

Aug 02 '22 08:08 affeldt-aist