feat(measure_theory/measure_space): 2 lemmas about compact sets (#3573)
feat(measure_theory/measure_space): 2 lemmas about compact sets (#3573)

A compact set `s` has finite (resp., zero) measure if every point of
`s` has a neighborhood within `s` of finite (resp., zero) measure.





leanprover-community/mathlib,leanprover-community/mathlib