Re: [mizar] Functions between the positive real numbers?

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

On Wed, 4 Apr 2007, Freek Wiedijk wrote:

> In the solution to this exercise, we would like to be able
> to use the notions from LIMFUNC1.  So the simplest approach
> is just to use something like
>
>  reserve f for PartFunc of REAL,REAL
>
> and then have conditions like
>
>  for x being positive Real holds x in dom f
>
> and
>
>  for x being positive Real holds f.x is positive Real
>
> That works.  However, it is not very elegant.
>
> So both me and two of my students have tried to make
> redefinitions and clusters such that we could use
>
>  reserve f for Function of posREAL,posREAL
>
> where
>
>  posREAL -> Subset of REAL
>
> is the set of positive real numbers, and then -- because of
> those redefinitions/clusters -- have f _also_ automatically
> be of type "PartFunc of REAL,REAL".  However, we have
> failed dismally.  Worse, we got _very_ mystifying errors.

Apparently we've already discussed this problem (typical ;-)) - please see 
the following archival thread and its follow-ups:

http://mizar.uwb.edu.pl/forum/archive/0609/msg00001.html

But I'm affraid no satisfying solution was offered then, and the library 
and the system haven't changed yet to support the proposed "future" 
solutions...

Best,
Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================