%0 Journal Article
%T A constructive and formal proof of Lebesgue¡¯s Dominated Convergence Theorem in the interactive theorem prover Matita
%A Claudio Sacerdoti Coen
%A Enrico Tassi
%J Journal of Formalized Reasoning
%D 2008
%I University of Bologna
%X 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.
%K Matita
%K Lebesgue¡¯s Dominated Convergence Theorem
%U http://jfr.cib.unibo.it/article/view/1334/747