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

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Jesse,

>What environment are you using?

The environment of my personal attempt at a solution (that
didn't work) was:

 vocabularies ARYTM, PARTFUN1, ARYTM_1, RELAT_1, ARYTM_3, FUNCT_1, ABSVALUE,
  FINSEQ_1, LIMFUNC1, ASYMPT_0, ORDINAL2, RCOMP_1, BORSUK_5, FUNCT_2;
 notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1,
  SEQ_1, RELSET_1, PARTFUN1, XXREAL_0, NAT_1, IRRAT_1, FUNCT_1,
  FUNCT_2, BORSUK_5, LIMFUNC1;
 constructors REAL_1, COMPLEX1, LIMFUNC1, POWER, SEQ_1, FUNCT_2;
 registrations XREAL_0, MEMBERED, XXREAL_0, NAT_1, REAL_1, PARTFUN1, FUNCT_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

>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.

We already had :-)  (Before you joined the list, I guess.)

Freek