Sacerdoti Coen, Claudio, and Enrico Tassi. 2008. “A Constructive and Formal Proof of Lebesgue’s Dominated Convergence Theorem in the Interactive Theorem Prover Matita”. Journal of Formalized Reasoning 1 (1):51-89. https://doi.org/10.6092/issn.1972-5787/1334.