feat(topology/order): discrete_topology_bot (#6163)

From `lean-liquid`
leanprover-community · Feb 11, 2021 · 58632ac · 58632ac
1 parent fdace95
commit 58632ac
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/topology/order.lean b/src/topology/order.lean
@@ -194,6 +194,10 @@ instance : complete_lattice (topological_space α) :=
 class discrete_topology (α : Type*) [t : topological_space α] : Prop :=
 (eq_bot [] : t = ⊥)
 
+@[priority 100]
+instance discrete_topology_bot (α : Type*) : @discrete_topology α ⊥ :=
+{ eq_bot := rfl }
+
 @[simp] lemma is_open_discrete [topological_space α] [discrete_topology α] (s : set α) :
   is_open s :=
 (discrete_topology.eq_bot α).symm ▸ trivial