From 67fcd6a48022c7678f96307ca408bc349131c1b6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 21 Jun 2024 00:30:07 +0900 Subject: [PATCH] voc --- theories/measure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/measure.v b/theories/measure.v index 61f01cac00..c6bd133a39 100644 --- 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 *)