[Merged by Bors] - feat(combinatorics/set_family/shadow): Shadow of a set family #10223
Conversation
YaelDillies
added
the
awaiting-review
|
|
||
| ## Notation | ||
|
|
||
| `∂ 𝒜` is notation for `shadow 𝒜`. It is situated in locale `finset_family`. |
There was a problem hiding this comment.
I used the mathscr unicode A through this file for finset families to match my notes (I was very new to Lean when the first version of this file was made), perhaps more sensible choices should be considered?
There was a problem hiding this comment.
I personally like that choice. In general, your branch was very nice-looking notation-wise, but the notation was pretty obscure. Another idea would be to use s and t for the finsets and A for the family.
There was a problem hiding this comment.
Yeah s and t for the finsets would match nicely with data/finset as well
There was a problem hiding this comment.
Do we want to adjust to A, B : finset (finset α) before merging?
There was a problem hiding this comment.
I quite like it like that. But I can change if you really want to.
Co-authored-by: David Wärn <codwarn@gmail.com>
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
One more down! bors merge |
This defines `shadow 𝒜` where `𝒜 : finset (finset α))`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This defines
shadow 𝒜where𝒜 : finset (finset α)).The shadow of a set family is its projection (hence the name) down the membership hypercube. Combinatorics of set families are interested in the size of shadows and ways to make it smaller (through so-called compressions).
Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com, Alena Gusakov @agusakov