Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-09 19:09 84c0132e

View on Github →

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'

Estimated changes

added theorem set.indicator_eq_self
added theorem set.indicator_eq_zero'
added theorem set.indicator_eq_zero
modified theorem set.indicator_indicator