(1)
Sacerdoti Coen, C.; Tassi, E. A Constructive and Formal Proof of Lebesgue’s Dominated Convergence Theorem in the Interactive Theorem Prover Matita. JFR 2008, 1, 51-89.