TY - JOUR AU - Sacerdoti Coen, Claudio AU - Tassi, Enrico PY - 2008/01/01 Y2 - 2024/03/28 TI - A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita JF - Journal of Formalized Reasoning JA - JFR VL - 1 IS - 1 SE - Articles DO - 10.6092/issn.1972-5787/1334 UR - https://jfr.unibo.it/article/view/1334 SP - 51-89 AB - We present a formalisation of a constructive proof of Lebesgue’s Dominated Convergence Theorem given by the Sacerdoti Coen and Zoli in [CSCZ]. The proof is done in the abstract setting of ordered uniformities, also introduced by the two authors as a simplification of Weber’s lattice uniformities given in [Web91, Web93]. The proof is fully constructive, in the sense that it is done in Bishop’s style and, under certain assumptions, it is also fully predicative. The formalisation is done in the Calculus of (Co)Inductive Constructions using the interactive theorem prover Matita [ASTZ07]. It exploits some peculiar features of Matita and an advanced technique to represent algebraic hierarchies previously introduced by the authors in [ST07]. Moreover, we introduce a new technique to cope with duality to halve the formalisation effort. ER -