Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat (data/multiset/powerset): add bind_powerset_len #15824

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat (data/multiset/powerset): add bind_powerset_len #15824

wants to merge 15 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Aug 2, 2022 •
edited by github-actions bot
Loading

We prove the following result

lemma multiset.bind_powerset_len {α : Type*} (S : multiset α) :
  bind (multiset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset

From flt-regular

Open in Gitpod

@xroblot xroblot marked this pull request as ready for review August 3, 2022 06:43
@xroblot xroblot mentioned this pull request Aug 3, 2022
Closed
2 tasks
@xroblot xroblot added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR labels Aug 3, 2022
@eric-wieser
Copy link
Member

I wonder if we can derive any of these results from #15834...

@xroblot
Copy link
Collaborator Author

xroblot commented Aug 3, 2022

It does look like the sum version could be derived from range_bind_sublists_len in some way. I have to go now but I can try to make it work tomorrow.

@xroblot xroblot changed the title feat (nat/choose/sum): add sum_powerset_len feat (data/multiset/bind): add bind_powerset_len Aug 4, 2022
@xroblot xroblot changed the title feat (data/multiset/bind): add bind_powerset_len feat (data/multiset/powerset): add bind_powerset_len Aug 4, 2022
@xroblot
Copy link
Collaborator Author

xroblot commented Aug 4, 2022 •
edited
Loading

Ok. So I was able to prove an equivalent version of the sum lemma using the results of #15834. I still have to do the sup version, that should be easy but I have to go to bed now. The results have moved to data/multiset/powerset due to the different dependencies.

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 4, 2022
@xroblot
Copy link
Collaborator Author

xroblot commented Aug 5, 2022

Everything is in place now with the new version of sup_powerset_len

@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 5, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 9, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

eric-wieser and others added 3 commits August 9, 2022 19:02
@eric-wieser
Update src/data/multiset/powerset.lean
6716514
@xroblot @eric-wieser
Update src/algebra/big_operators/basic.lean
010e179 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@xroblot @eric-wieser
Update src/algebra/big_operators/basic.lean
7347aa8 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
jcommelin
jcommelin approved these changes Aug 11, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 11, 2022
bors bot pushed a commit that referenced this pull request Aug 11, 2022
@xroblot @eric-wieser
feat (data/multiset/powerset): add bind_powerset_len (#15824)
87e9e26 
We prove the following result
```lean
lemma multiset.bind_powerset_len {α : Type*} (S : multiset α) :
  bind (multiset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset
```

From flt-regular



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Aug 11, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat (data/multiset/powerset): add bind_powerset_len [Merged by Bors] - feat (data/multiset/powerset): add bind_powerset_len Aug 11, 2022
@bors bors bot closed this Aug 11, 2022
@bors bors bot deleted the xfr_powerset branch August 11, 2022 18:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@xroblot @eric-wieser @mathlib-dependent-issues-bot @jcommelin @leanprover-community-bot-assistant