voc

math-comp · Jul 18, 2024 · 768c10d · 768c10d
1 parent b1368a4
commit 768c10d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/measure.v b/theories/measure.v
@@ -186,7 +186,7 @@ From HB Require Import structures.
 (*                       intersection                                         *)
 (*      setU_closed G == the set of sets G is closed under finite union       *)
 (*      setC_closed G == the set of sets G is closed under complement         *)
-(*     setSD_closed G == the set of sets G is closed under relative           *)
+(*     setSD_closed G == the set of sets G is closed under proper             *)
 (*                       difference                                           *)
 (*     setDI_closed G == the set of sets G is closed under difference         *)
 (*     ndseq_closed G == the set of sets G is closed under non-decreasing     *)