Commit 2020-07-27 11:35 8ba59d84
View on Github →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.