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