bigcup and bigcap are not necessarily countable (#1961)

Author: mkerjean

classical/classical_sets.v

@@ -45,8 +45,8 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (* |            [set E \| x in P] |==| the set of E with x ranging in P       *)
 (* |                      range f |==| image by f of the full set             *)
 (* | \big[setU/set0]_(i <- s \| P i) f i |==| finite union                    *)
-(* |         \bigcup_(k in P) F k |==| countable union                        *)
-(* |         \bigcap_(k in P) F k |==| countable intersection                 *)
+(* |         \bigcup_(k in P) F k |==| arbitrary union                        *)
+(* |         \bigcap_(k in P) F k |==| arbitrary intersection                 *)
 (* |                 trivIset D F |==| F is a sequence of pairwise disjoint   *)
 (* |                              |  | sets indexed over the domain D         *)
 (*                                                                            *)