-
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
[Merged by Bors] - chore(topology/separation): prove that {y | y ≠ x}
is open
#2506
Conversation
src/topology/separation.lean
Outdated
@@ -120,10 +120,12 @@ class t1_space (α : Type u) [topological_space α] : Prop := | |||
lemma is_closed_singleton [t1_space α] {x : α} : is_closed ({x} : set α) := | |||
t1_space.t1 x | |||
|
|||
lemma is_open_ne [t1_space α] {x : α} : is_open {y | y ≠ x} := | |||
by simpa using is_open_neg (t1_space.t1 x) |
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.
Was there a PR that changed the naming convention, so is_open_neg
should now be is_open_compl
?
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_open_neg
uses set_of
. We also have is_open_compl_iff
.
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.
After e8a68de is_open_neg
is never used in mathlib
.
bors merge |
Pull request successfully merged into master. Build succeeded: |
{y | y ≠ x}
is open{y | y ≠ x}
is open
No description provided.