mathlib
90cde5e1 - feat(measure_theory/measure/content): regular contents (#16289)

Commit
3 years ago
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 <105789986+ReimannJ@users.noreply.github.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Author
Parents
Loading