disjoint in algebra.big_operators

Stream: new members

[Anne Baanen]

Hi everyone, I've noticed that the definitions in algebra.big_operators don't use disjoint to indicate disjoint sets, instead writing out s₁ ∩ s₂ = ∅ (which is slightly incompatible with disjoint, which reduces to s₁ ∩ s₂ ≤ ∅. Is there a reason for this choice?

[Johan Commelin]

@Tim Baanen My guess would be history...

[Johan Commelin]

But I didn't check

[Anne Baanen]

Ok, I can change it to use disjoint instead. Might be a nice first contribution to mathlib :)

[Chris Hughes]

disjoint came after these lemmas I believe.

[Anne Baanen]

I created a pull request: https://github.com/leanprover-community/mathlib/pull/1456

[Johan Commelin]

Thanks!

[Rob Lewis]

FYI, @Tim Baanen just joined our group in Amsterdam as a PhD student. Thanks Tim, looking forward to many future PRs!

[Patrick Massot]

Welcome Tim!

[Anne Baanen]

Thank you all! :big_smile:

[Johan Commelin]

@Tim Baanen Voila... it's on the merge queue.