-
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(topology): a few more results about compact sets #11905
Conversation
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.
Thanks!
bors d+
@@ -872,6 +874,9 @@ theorem compl_inter (s t : set α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ := compl_inf | |||
|
|||
@[simp] lemma compl_univ_iff {s : set α} : sᶜ = univ ↔ s = ∅ := compl_eq_top | |||
|
|||
lemma compl_ne_univ : sᶜ ≠ univ ↔ s.nonempty := |
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 compl_ne_univ : sᶜ ≠ univ ↔ s.nonempty := | |
@[simp] lemma compl_ne_univ : sᶜ ≠ univ ↔ s.nonempty := |
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.
See linter error before last commit
@@ -856,6 +856,8 @@ theorem not_mem_of_mem_compl {s : set α} {x : α} (h : x ∈ sᶜ) : x ∉ s := | |||
|
|||
theorem mem_compl_iff (s : set α) (x : α) : x ∈ sᶜ ↔ x ∉ s := iff.rfl | |||
|
|||
lemma not_mem_compl_iff {x : α} : x ∉ sᶜ ↔ x ∈ s := not_not |
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 not_mem_compl_iff {x : α} : x ∉ sᶜ ↔ x ∈ s := not_not | |
@[simp] lemma not_mem_compl_iff {x : α} : x ∉ sᶜ ↔ x ∈ s := not_not |
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
Neither suggestions would be simp-lemmas accepted by the linter (the LHS is not in simp-normal form). bors merge |
* Also a few lemmas about sets and `mul_support`.
Pull request successfully merged into master. Build succeeded: |
mul_support
.