Inclusion-Exclusion

Stream: Is there code for X?

[Christoph Spiegel]

Did I overlook something or is there no code for basic Inclusion-Exclusion in mathlib4? The only thing I could find is this and a comment by @Neil Strickland from 2019 that he will eventually add it to mathlib.

[Floris van Doorn]

that is the only hit of the word "exclusion" I find in Mathlib, so I think that is also the current state...

[Christoph Spiegel]

Any idea what the reason is? Not needed anywhere so far or always needed in some custom formulation? Would it make sense to try and set something up and make a PR? if so, would Combinatorics be a good place for it (similar to DoubleCounting) or Data.Finset? @Yaël Dillies

[Christoph Spiegel]

Or is it perhaps just a specific form of a more general result that's in mathlib?

[Bryan Gin-ge Chen]

@Yaël Dillies has various forms of the Möbius inversion formula for incidence algebras in the LeanCamCombi project, but I'm not sure if it's been specialized to inclusion-exclusion.

[Yaël Dillies]

It hasn't been specialised to inclusion-exclusion, no. I would highly welcome a PR going that!

[Jz Pan]

I think we only have the inclusion-exclusion for two sets: docs#Finset.card_union and which is added only a few months ago.

[Yaël Dillies]

No, this was added ages ago

[Yaël Dillies]

https://github.com/leanprover-community/mathlib/pull/327/files#diff-fd77aa96ec298b1175c1276d9a781626c2f550716ec372db859990be481fd341R940-R942