Commit 2023-01-22 10:47 0b8f22d9

View on Github →

feat: port Algebra.IndicatorFunction (#1752) Some mathport warning to pay attention to, and some proofs required some work explicitly using split_ifs which was not necessary in lean3, but otherwise straightforward.

Estimated changes

added theorem Set.comp_mulIndicator
added theorem Set.eqOn_mulIndicator
added theorem Set.indicator_compl
added theorem Set.indicator_diff
added theorem Set.indicator_mul
added theorem Set.indicator_mul_left
added theorem Set.indicator_one_inj
added theorem Set.indicator_prod_one
added theorem Set.indicator_smul
added theorem Set.le_mulIndicator
added theorem Set.mulIndicator_apply
added theorem Set.mulIndicator_compl
added theorem Set.mulIndicator_congr
added theorem Set.mulIndicator_diff
added theorem Set.mulIndicator_div'
added theorem Set.mulIndicator_div
added theorem Set.mulIndicator_empty
added theorem Set.mulIndicator_image
added theorem Set.mulIndicator_inv'
added theorem Set.mulIndicator_inv
added theorem Set.mulIndicator_le'
added theorem Set.mulIndicator_le
added theorem Set.mulIndicator_mul'
added theorem Set.mulIndicator_mul
added theorem Set.mulIndicator_one'
added theorem Set.mulIndicator_one
added theorem Set.mulIndicator_univ