Detailed proofs of Lebesgue integration, to be formalized in Coq.


The full code is downloadable here for Coq >= 8.8.2 .


Browsable files below.