measure_space): there exists a ball of positive measure (#14449)

Commit

3 years ago

feat(measure_theory/measure/measure_space): there exists a ball of positive measure (#14449) Motivated by #12933 Co-authored-by: Mantas Bakšys <baksysmantas@gmail.com>

Author

urkud

Parents

cfcc3a1b

mathlib b5973ba9 - feat(measure_theory/measure/measure_space): there exists a ball of positive measure (#14449)

mathlib
b5973ba9 - feat(measure_theory/measure/measure_space): there exists a ball of positive measure (#14449)