Sacerdoti Coen, C., & 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), 51–89. https://doi.org/10.6092/issn.1972-5787/1334