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.