feat(topology/order): add nhds_true and nhds_false (#14082)

src/topology/order.lean

@@ -789,16 +789,22 @@ section sierpinski
 variables {α : Type*} [topological_space α]
 
 @[simp] lemma is_open_singleton_true : is_open ({true} : set Prop) :=
-topological_space.generate_open.basic _ (by simp)
+topological_space.generate_open.basic _ (mem_singleton _)
+
+@[simp] lemma nhds_true : 𝓝 true = pure true :=
+le_antisymm (le_pure_iff.2 $ is_open_singleton_true.mem_nhds $ mem_singleton _) (pure_le_nhds _)
+
+@[simp] lemma nhds_false : 𝓝 false = ⊤ :=
+topological_space.nhds_generate_from.trans $ by simp [@and.comm (_ ∈ _)]
 
 lemma continuous_Prop {p : α → Prop} : continuous p ↔ is_open {x | p x} :=
 ⟨assume h : continuous p,
   have is_open (p ⁻¹' {true}),
     from is_open_singleton_true.preimage h,
-  by simp [preimage, eq_true] at this; assumption,
+  by simpa [preimage, eq_true] using this,
   assume h : is_open {x | p x},
-  continuous_generated_from $ assume s (hs : s ∈ {{true}}),
-    by simp at hs; simp [hs, preimage, eq_true, h]⟩
+  continuous_generated_from $ assume s (hs : s = {true}),
+    by simp [hs, preimage, eq_true, h]⟩
 
 lemma is_open_iff_continuous_mem {s : set α} : is_open s ↔ continuous (λ x, x ∈ s) :=
 continuous_Prop.symm