-
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
feat(data/set/basic): more lemmas about set.nonempty
#1780
Conversation
Could you rebase this on master (and solve the conflict) so that seeing the additions of this PR becomes easier? Thanks! |
@sgouezel Done. |
src/data/set/basic.lean
Outdated
theorem insert_ne_empty (a : α) (s : set α) : insert a s ≠ ∅ := | ||
by safe [ext_iff, iff_def]; have h' := a_1 a; finish | ||
(insert_nonempty).ne_empty |
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.
missing explicit arguments
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.
This fix was lost while git rebase
ing. That's one of the reasons I'd prefer if mathlib did proper git merge
instead of squashing the history (then git merge
would work).
…mmunity#1780) * feat(data/set/basic): more lemmas about `set.nonempty` * Fix compile
…mmunity#1780) * feat(data/set/basic): more lemmas about `set.nonempty` * Fix compile
Some lemmas missing in #1779
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list