-
Notifications
You must be signed in to change notification settings - Fork 299
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.
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
[Merged by Bors] - feat(data/list/*): subperm_singleton_iff #11680
Conversation
ericrbg
commented
Jan 27, 2022
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
src/data/list/count.lean
Outdated
@@ -131,6 +131,9 @@ lemma le_count_iff_repeat_sublist {a : α} {l : list α} {n : ℕ} : | |||
by rw ← this; apply filter_sublist, | |||
λ h, by simpa only [count_repeat] using h.count_le a⟩ | |||
|
|||
@[simp] lemma one_le_count_iff_mem {a : α} {l : list α} : 1 ≤ count a l ↔ a ∈ l := | |||
by { convert list.le_count_iff_repeat_sublist, simp } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there an easier proof of this via count_pos
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ahh, yes, I knew it had to be there already. i also made count_pos
a simp-lemma - I'm fairly unsure whether we should do that for both, or not.
✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Pull request successfully merged into master. Build succeeded: |