fix

math-comp · Jan 8, 2024 · 2f6c482 · 2f6c482
1 parent ed17518
commit 2f6c482
Showing 1 changed file with 21 additions and 21 deletions.
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
@@ -33,29 +33,29 @@ From mathcomp Require Import mathcomp_extra boolp.
 (*   set (i.e., of type set rT)                                               *)
 (* - indexed sets are rather named F                                          *)
 (*                                                                            *)
-(* Sample notations:                                                          *)
+(* Example of notations:                                                      *)
 (* | Coq notations                |   | Meaning                             | *)
-(* |-----------------------------:|---|:------------------------------------| *)
-(* |                         set0 |==| $\emptyset$                          | *)
-(* |                     [set: A] |==| the full set of elements of type A   | *)
-(* |                   `` `\|` `` |==| $\cup$                               | *)
-(* |                    `` `&` `` |==| $\cap$                               | *)
-(* |                    `` `\` `` |==| set difference                       | *)
-(* |                     `` ~` `` |==| set complement                       | *)
-(* |                   `` `<=` `` |==| $\subseteq$                          | *)
-(* |                 `` f @` A `` |==| image by f of A                      | *)
-(* |              `` f @^-1` A `` |==| preimage by f of A                   | *)
-(* |                      [set x] |==| the singleton set $\{x\}$            | *)
-(* |                     [set~ x] |==| the complement of $\{x\}$            | *)
-(* |            [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               | *)
-(* |                 trivIset D F |==| F is a sequence of pairwise disjoint | *)
-(* |                              |  | sets indexed over the domain D       | *)
+(* |-----------------------------:|---|:------------------------------------  *)
+(* |                         set0 |==| $\emptyset$                            *)
+(* |                     [set: A] |==| the full set of elements of type A     *)
+(* |                   `` `\|` `` |==| $\cup$                                 *)
+(* |                    `` `&` `` |==| $\cap$                                 *)
+(* |                    `` `\` `` |==| set difference                         *)
+(* |                     `` ~` `` |==| set complement                         *)
+(* |                   `` `<=` `` |==| $\subseteq$                            *)
+(* |                 `` f @` A `` |==| image by f of A                        *)
+(* |              `` f @^-1` A `` |==| preimage by f of A                     *)
+(* |                      [set x] |==| the singleton set $\{x\}$              *)
+(* |                     [set~ x] |==| the complement of $\{x\}$              *)
+(* |            [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                 *)
+(* |                 trivIset D F |==| F is a sequence of pairwise disjoint   *)
+(* |                              |  | sets indexed over the domain D         *)
 (*                                                                            *)
-(* Details:                                                                   *)
+(* Detailed documentation:                                                                   *)
 (* ## Sets                                                                    *)
 (* ```                                                                        *)
 (*                       set T == type of sets on T                           *)