mathlib
84c0132e - chore(data/indicator_function): a few more `simp` lemmas (#5293)

Commit
5 years ago
chore(data/indicator_function): a few more `simp` lemmas (#5293) * drop `indicator_of_support_subset` in favor of the new `indicator_eq_self`; * add a few more lemmas: `indicator_apply_eq_self`, `indicator_apply_eq_zero`, `indicator_eq_zero`, `indicator_eq_zero'`
Author
Parents
Loading