Re: [mizar] real number vs. Element of REAL

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

On Fri, 11 May 2012, trybulec@math.uwb.edu.pl wrote:

> There is known problem: which one to use? The denotation is the same, however 
> technically the type 'real number' is more general than 'Element of REAL'
> Therefore one likes to have theorems about real numbers and one likes to 
> prove theorems about elements of reals. The same goes for other kinds of 
> numbers.
> However short notation (expandable type) is used as a rule for 'number' with 
> an adjective:
>
> ORDINAL1:
>  mode Nat is natural number;
> INT_1:
>  mode Integer is integer number;
> RAT_1:
>  mode Rational is rational number;
> CFUNCT_1:
>  mode Complex is complex number;
>
> not so in the case of 'Real':
>
> REAL_1:
>  mode Real is Element of REAL;



We should also remember about 'extended reals'.

SUPINF_1:
 mode R_eal is Element of ExtREAL;

Regards
Artur



> If there are some arguments for both types, it is unacceptable that the user 
> must look to the abstracts to check which type had been used in the theorem 
> to which he wants to refer to. And if we have to choose, 'real number' is 
> preferable.
>
> Changing the definition of the mode 'Real' causes too many errors, co some 
> preparatory work is necessary. In the new version many occurrences of
> 'Real' are changed to 'real number'. With more than 600 articles modified we 
> decided to publish this new version of MML, even if the revolution is not 
> completed. Sorry for the (even bigger) mess, we will correct it ASAP.
>
> Regards,
> Andrzej


==========================================================================

Artur Kornilowicz                          e-mail: arturk@math.uwb.edu.pl

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Informatics                   tel. +48 (85) 745-7662
University of Bialystok                    fax. +48 (85) 745-7662
Sosnowa 64, 15-887 Bialystok, Poland