Sacerdoti Coen, C. and Tassi, E. (2008) “A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita”, Journal of Formalized Reasoning, 1(1), pp. 51–89. doi: 10.6092/issn.1972-5787/1334.