analysis icon indicating copy to clipboard operation
analysis copied to clipboard

naming discrete_measurable

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

https://github.com/math-comp/analysis/blob/593c2448923f9b1577fbc97a871f75a8b43ac233/theories/measure.v#L866

shouldn't be this better named discrete_measurable_nat or measurable_nat?

affeldt-aist avatar Jul 22 '22 14:07 affeldt-aist