fixes math-comp#838

affeldt-aist · Feb 24, 2023 · f533185 · f533185
1 parent 113afa6
commit f533185
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/topology.v b/theories/topology.v
@@ -188,6 +188,8 @@ Require Import reals signed.
 (*                                     a pointedType, as well as the carrier. *)
 (*                                     nbhs_of_open \o open_from must be      *)
 (*                                     used to declare a filterType           *)
+(*                    finI_from D f == set of \bigcap_(i in E) f i where E is *)
+(*                                     a finite subset of D                   *)
 (*       topologyOfSubbaseMixin D b == builds the mixin for a topological     *)
 (*                                     space from a subbase of open sets b    *)
 (*                                     indexed on domain D; the type of       *)