feat(measure_theory/measure/content): regular contents (#16289)
feat(measure_theory/measure/content): regular contents (#16289)

Define regular contents and prove that regular contents agree with their induced measures on compact sets. 



Co-authored-by: ReimannJ <d2f5ae5092546c61798b2fb31684b6f620a22272@users.noreply.github.com>
Co-authored-by: Floris van Doorn <04eee3258902297ef5081ba8b0786f6ab1274795@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib