feat(topology/basic): Singleton sets are not open (#16843)

An immediate consequence of `dense_compl_singleton_iff_not_open` and `dense_compl_singleton`.
leanprover-community · Oct 10, 2022 · 4f56937 · 4f56937
1 parent 3441411
commit 4f56937
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/topology/basic.lean b/src/topology/basic.lean
@@ -1041,6 +1041,9 @@ space. -/
   interior {x} = (∅ : set α) :=
 interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x)
 
+lemma not_is_open_singleton (x : α) [ne_bot (𝓝[≠] x)] : ¬ is_open ({x} : set α) :=
+dense_compl_singleton_iff_not_open.1 (dense_compl_singleton x)
+
 lemma closure_eq_cluster_pts {s : set α} : closure s = {a | cluster_pt a (𝓟 s)} :=
 set.ext $ λ x, mem_closure_iff_cluster_pt