fixed a comment

inQWIRE · Jan 20, 2023 · c19d3e7 · c19d3e7
1 parent 61faba1
commit c19d3e7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Ctopology.v b/Ctopology.v
@@ -1785,7 +1785,7 @@ Proof. intros.
 Qed.
 
 
-(* now, we show compact -> open *)
+(* now, we show compact -> closed *)
 Definition bad_point_cover (c : C) : Ccover :=
   fun G => open G /\ exists r, r > 0 /\ G ⊂ (fun c' => Cmod (c' - c) > r).