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

[Jesse Alama <alama@stanford.edu>]

Freek Wiedijk <freek@cs.ru.nl> writes:

> I'm currently teaching a Mizar course, and a problem came up
> that I haven't been able to solve.  Please help me with this.
>
> I ask the students as an exercise to formalize the solution
> of a puzzle from the international mathematical olympiads
> that talks about a function from the positive real numbers
> to the positive real numbers:
>
> <http://www.cs.ru.nl/~freek/courses/pa-2007/exercises/exercise-mizar.pdf>
>
> 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.

What environment are you using?  (I can't count how many hours I've
been blocked by mystifying errors that are just due to something being
wrong or missing in my environment.  There has got to be a way to make
getting the environment right not so unpleasant!  Perhaps we can have
a separate discussion about that.)

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*950: Too many schemes (http://www.mizar.org)