文章基本信息

标题：A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
本地全文：下载
作者：Claudio Sacerdoti Coen ; Enrico Tassi
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2008
卷号：1
期号：1
页码：51-89
DOI：10.6092/issn.1972-5787/1334
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：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.