feat: add closed and compact corollaries of Lusin's theorem in global/local versions#4

mike1729 wants to merge 2 commits intoCoolRmal:lusinCoolRmal/mathlib4:lusinfrom

mike1729:coolrmal-lusinmike1729/mathlib4:coolrmal-lusinCopy head branch name to clipboard