Add a hint for unfolding open_neighborhood

coq-community · Feb 14, 2022 · d6d78d9 · d6d78d9
1 parent 93086be
commit d6d78d9
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/Topology/Neighborhoods.v b/theories/Topology/Neighborhoods.v
@@ -5,6 +5,8 @@ Definition open_neighborhood {X:TopologicalSpace}
   (U:Ensemble X) (x:X) :=
   open U /\ In U x.
 
+Hint Unfold open_neighborhood : topology.
+
 Definition neighborhood {X:TopologicalSpace}
   (N:Ensemble X) (x:X) :=
   exists U:Ensemble X,