measure_space): add lemma `measure_theory.measure.exists_mem_of_measure_ne_zero_of_ae` (#15812)

Commit

3 years ago

feat(measure_theory/measure/measure_space): add lemma `measure_theory.measure.exists_mem_of_measure_ne_zero_of_ae` (#15812) Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Author

ocfnash

Parents

3ed70184

mathlib 7e33e4f1 - feat(measure_theory/measure/measure_space): add lemma `measure_theory.measure.exists_mem_of_measure_ne_zero_of_ae` (#15812)

mathlib
7e33e4f1 - feat(measure_theory/measure/measure_space): add lemma `measure_theory.measure.exists_mem_of_measure_ne_zero_of_ae` (#15812)