Measurable of constant on intervals

Stream: Is there code for X?

[Bhavik Mehta]

I have a (real-valued) function which is constant on each interval of the form Ico z (z+1) for integers z. What's the easiest way in mathlib to show this function is measurable?

[Yury G. Kudryashov]

I'm not sure about the easiest way but I have an opinion about the right way to do it. IMHO, you should generalize docs#measurable_of_measurable_union_cover to the case of a countable union, then use it.

[Bhavik Mehta]

I realised I can write my function as a composition of a function from N and nat.floor, which makes it easy. Your way looks more general for sure though

[Yury G. Kudryashov]

And we have docs#nat.measurable_floor