mathlib

4a63f3f2 - feat(data/indicator_function): add `indicator_range_comp` (#3343)

feat(data/indicator_function): add `indicator_range_comp` (#3343) Add * `comp_eq_of_eq_on_range`; * `piecewise_eq_on`; * `piecewise_eq_on_compl`; * `piecewise_compl`; * `piecewise_range_comp`; * `indicator_range_comp`.