A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita

Claudio Sacerdoti Coen, Enrico Tassi. A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita. J. Formalized Reasoning, 1(1):51-89, 2008. [doi]

Abstract

Abstract is missing.