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 1, no. 1 (January 1, 2008): 51–89. Accessed February 8, 2023. https://jfr.unibo.it/article/view/1334.