Doc: definitions expressed as a table in constructive_ereal.v (#1452)

---------

Co-authored-by: Reynald Affeldt <[email protected]>

Author: yoshihiro503

classical/classical_sets.v

@@ -34,7 +34,7 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*   set (i.e., of type set rT)                                               *)
 (* - indexed sets are rather named F                                          *)
 (*                                                                            *)
-(* Example of notations:                                                      *)
+(* Examples of notations:                                                     *)
 (* | Coq notations                |   | Meaning                             | *)
 (* |-----------------------------:|---|:------------------------------------  *)
 (* |                         set0 |==| $\emptyset$                            *)

reals/constructive_ereal.v

@@ -16,14 +16,43 @@ From mathcomp Require Import mathcomp_extra signed.
 (**md**************************************************************************)
 (* # Extended real numbers $\overline{R}$                                     *)
 (*                                                                            *)
-(* Given a type R for numbers, \bar R is the type R extended with symbols     *)
-(* -oo and +oo (notation scope: %E), suitable to represent extended real      *)
-(* numbers. When R is a numDomainType, \bar R is equipped with a canonical    *)
-(* porderType and operations for addition/opposite. When R is a               *)
-(* realDomainType, \bar R is equipped with a Canonical orderType.             *)
+(* Given a type R for numbers, `\bar R` is the type `R` extended with symbols *)
+(* `-oo` and `+oo` (notation scope: `%E`), suitable to represent extended     *)
+(* real numbers. When `R` is a `numDomainType`, `\bar R` is equipped with a   *)
+(* canonical `porderType` and operations for addition/opposite. When `R` is a *)
+(* `realDomainType`, `\bar R` is equipped with a canonical `orderType`.       *)
 (*                                                                            *)
 (* Naming convention: in definition/lemma identifiers, "e" stands for an      *)
-(* extended number and "y" and "Ny" for +oo ad -oo respectively.              *)
+(* extended number and "y" and "Ny" for `+oo` and `-oo` respectively.         *)
+(*                                                                            *)
+(* Examples of notations:                                                     *)
+(* | Coq definitions        |  | Meaning                                    | *)
+(* |-----------------------:|--|--------------------------------------------| *)
+(* |               `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$| *)
+(* |                        |  | notation for `extended (R:Type)`           | *)
+(* |                 `r%:E` |==| injects real numbers into `\bar R`         | *)
+(* |        `+%E, -%E, *%E` |==| addition/opposite/multiplication for       | *)
+(* |                        |  | extended reals                             | *)
+(* | `er_map (f : T -> T')` |==| the `\bar T -> \bar T'` lifting of `f`     | *)
+(* |                `sqrte` |==| square root for extended reals             | *)
+(* |       `` `\| x \|%E `` |==| the absolute value of `x`                  | *)
+(* |               `x ^+ n` |==| iterated multiplication                    | *)
+(* |               `x *+ n` |==| iterated addition                          | *)
+(* |    `+%dE, (x *+ n)%dE` |==| dual addition/dual iterated addition       | *)
+(* |                        |  | ($-\infty + +\infty = +\infty$)            | *)
+(* |                        |  | Import DualAddTheory for related lemmas    | *)
+(* |               `x +? y` |==| the addition of `x` and `y` is defined     | *)
+(* |                        |  | it is neither $+\infty - \infty$           | *)
+(* |                        |  | nor $-\infty + \infty$                     | *)
+(* |               `x *? y` |==| the multiplication of `x` and `y` is not   | *)
+(* |                        |  | of the form $0 * +\infty$ or $0 * -\infty$ | *)
+(* | `(_ <= _)%E`, `(_ < _)%E`,|==| comparison relations for extended reals | *)
+(* | `(_ >= _)%E`, `(_ > _)%E` |  |                                         | *)
+(* | `(\sum_(i in A) f i)%E`|==| bigop-like notation in scope `%E`          | *)
+(* |`(\prod_(i in A) f i)%E`|==| bigop-like notation in scope `%E`          | *)
+(* |   `maxe x y, mine x y` |==| notation for the maximum/minimum           | *)
+(*                                                                            *)
+(* Detailed documentation:                                                    *)
 (* ```                                                                        *)
 (*                  \bar R == coproduct of R and {+oo, -oo};                  *)
 (*                            notation for extended (R:Type)                  *)