-
Notifications
You must be signed in to change notification settings - Fork 298
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/finset): new union, set difference, singleton lemmas #1702
Conversation
src/data/finset.lean
Outdated
@@ -546,6 +555,16 @@ set.ext $ λ _, mem_sdiff | |||
@[simp] lemma to_set_sdiff (s t : finset α) : (s \ t).to_set = s.to_set \ t.to_set := | |||
by apply finset.coe_sdiff | |||
|
|||
theorem union_sdiff_self_eq_union (s t : finset α) : s ∪ (t \ s) = s ∪ t := |
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 could be @[simp]
with a left and right version
src/data/finset.lean
Outdated
lemma union_sdiff_symm (s t : finset α) : s ∪ (t \ s) = t ∪ (s \ t) := | ||
by rw [union_sdiff_self_eq_union, union_sdiff_self_eq_union, union_comm] | ||
|
||
lemma sdiff_empty_iff_subset (s t : finset α) : s \ t = ∅ ↔ s ⊆ t := |
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.
lemma sdiff_empty_iff_subset (s t : finset α) : s \ t = ∅ ↔ s ⊆ t := | |
lemma sdiff_eq_empty_iff_subset {s t : finset α} : s \ t = ∅ ↔ s ⊆ t := |
src/data/finset.lean
Outdated
@@ -171,6 +171,15 @@ theorem singleton_inj {a b : α} : ι a = ι b ↔ a = b := | |||
|
|||
@[simp] lemma coe_singleton (a : α) : ↑(ι a) = ({a} : set α) := rfl | |||
|
|||
lemma singleton_iff_unique_mem (s : finset α) : (∃ a, s = finset.singleton a) ↔ ∃! a, a ∈ s := |
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 might be better stated in a slightly stronger way without the exists.
lemma eq_singleton_iff {s : finset α} {a : α} :
s = finset.singleton a ↔ a ∈ s ∧ ∀ x ∈ s, x = a
That way we know both the a
s are the same, and the stated theorem should be a trivial consequence of this, by simp only [eq_singleton_iff_unique_mem, exists_unique]
does the trick.
Thanks for the suggestions, I've implemented them all. |
…rover-community#1702) * Singleton iff unique element lemma * Set difference lemmas * Changes from review
…rover-community#1702) * Singleton iff unique element lemma * Set difference lemmas * Changes from review
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