Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-09 21:17 4a63f3f2

View on Github →

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.

Estimated changes

modified theorem set.indicator_le_indicator
added theorem set.piecewise_compl
added theorem set.piecewise_eq_on