Lusin'a Approximation Theorem

Stream: new members

[Rahul Soni]

Is Lusin's Approximation theorem defined in Mathlib? I was able to find Egorov's theorem #MeasureTheory.tendstoUniformlyOn_of_ae_tendsto but couldn't find Luzin's theorem on Mathlib. Does one need to formalize that?

[Johan Commelin]

I don't think it's there.