Update theories/topology_theory/topology_structure.v

math-comp · Oct 30, 2024 · 7944741 · 7944741
1 parent 560b843
commit 7944741
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
@@ -899,7 +899,7 @@ End closure_interior_lemmas.
 Lemma closureC_deprecated (T : topologicalType) (E : set T) :
   ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x.
 Proof. by rewrite -interiorC interiorEbigcup. Qed.
-#[deprecated(since="mathcomp-analysis 1.6.1", note="use `interiorC` and `interiorEbigcup` instead")]
+#[deprecated(since="mathcomp-analysis 1.7.0", note="use `interiorC` and `interiorEbigcup` instead")]
 Notation closureC := closureC_deprecated (only parsing).
 
 Section DiscreteTopology.