Commit 2020-07-24 11:07 2d47d0cb
View on Github →chore(measure_theory/indicator_function): split into 2 files deps: 3503 (#3509)
Split measure_theory/indicator_function into 2 files.
This file formulated all lemmas for measure.ae but they hold for any filter.