mathlib

2d47d0cb - chore(measure_theory/indicator_function): split into 2 files deps: 3503 (#3509)

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. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>