forgot to add docs for sets_of

math-comp · Mar 1, 2022 · f54d0ed · f54d0ed
1 parent 5d9ac7a
commit f54d0ed
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/theories/topology.v b/theories/topology.v
@@ -107,6 +107,9 @@ Require Import mathcomp_extra boolp reals classical_sets posnum functions.
 (*                                     domain D.                              *)
 (*                subset_filter F D == similar to within D F, but with        *)
 (*                                     dependent types.                       *)
+(*                        sets_of F == The filter of downward closed subsets  *)
+(*                                     of F. Enables use of near notation to  *)
+(*                                     pick suitably small members of F       *)
 (*                      in_filter F == interface type for the sets that       *)
 (*                                     belong to the set of sets F.           *)
 (*                      InFilter FP == packs a set P with a proof of F P to   *)