feat: add closed and compact corollaries of Lusin's theorem#5

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

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