Re: Formalization of the Lebesgue measure in Mizar

Dear Amir,

Quoting Amir Livne Bar-on <[email protected]>:

> My working directory is publicly available at
> https://github.com/amirlb/mizar-lebesgue-measure
>
> 1. Is this really not covered? AFAICT, the Lebesgue measure only appears in
> two definitions in the end of MEASURE7. If it is covered, or if anyone else
> is in the process of formalizing this, I'll pick another area.

Have you looked at the MEASFUNC series of articles developed by prof.  
Shidama's group?
It seems that these articles use a slightly more general setting to  
Lebesgue integrability.

There is also a paper you might be interested to see:

http://logika.uwb.edu.pl/studies/download.php?volid=23&artid=se&format=PDF

Best regards,

Adam