[Merged by Bors] - feat(finset/basic): downward induction for finsets #7379
Conversation
YaelDillies
commented
Apr 27, 2021
•
YaelDillies
commented
YaelDillies
added
the
awaiting-review
|
I didn't manage to get an equivalent of |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
src/data/finset/basic.lean
Outdated
| by { dunfold strong_downward_induction_on, rw strong_downward_induction } | ||
|
|
||
| /-- Analogue of `strong_downward_induction_on` but over a set. -/ | ||
| def strong_downward_induction_on_set {p : finset α → Sort*} {A : set (finset α)} |
There was a problem hiding this comment.
Is this really necessary? We don't have analogues of this lemma for any other induction principle.
There was a problem hiding this comment.
I don't know. I found it handy in my case, but it's true that it's mostly strong_downward_induction_on applied to λ s, s ∈ A → p s with s ∈ A → s.card ≤ n factored out.
There was a problem hiding this comment.
Okay, I've removed it. We'll see whether I can do without it.
github-actions
bot
added
ready-to-merge
|
This PR was included in a batch that was canceled, it will be automatically retried |
|
Build failed (retrying...): |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
