bors d+

LGTM, thanks! Do you think it's worth having the _apply-free version too, mulIndicator (⋂ i, s i) f = ⨅ i, mulIndicator (s i) f?

✌️ kkytola can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors d+

LGTM, thanks! Do you think it's worth having the _apply-free version too, mulIndicator (⋂ i, s i) f = ⨅ i, mulIndicator (s i) f?

Thank you!

That is a good question! I don't have enough experience to have a clear opinion on that. (I guess that has to do with how canonical the sup/inf spelling of functions is considered.)

Based on just (1) the fact that the existing mulIndicator_iUnion_apply did not have this _apply-free version and (2) that when I noticed the missing lemma, I wanted the _apply-ful/pointwise version, I would default to not adding those _apply-free versions for now.

bors r+

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style