Commit 2023-07-24 14:02 4d06c76f
View on Github →feat(Algebra/IndicatorFunction): add indicator_iInter_apply as a counterpart to indicator_iUnion_apply. (#6078)
Add lemma mulIndicator_iInter_apply and its additive version indicator_iInter_apply. These are entirely parallel to the existing mulIndicator_iUnion_apply and its additive version indicator_iUnion_apply.