Cousin’s Lemma
Roland Coghetto
Formalized Mathematics, Tome 24 (2016), p. 107-119 / Harvested from The Polish Digital Mathematics Library

We formalize, in two different ways, that “the n-dimensional Euclidean metric space is a complete metric space” (version 1. with the results obtained in [13], [26], [25] and version 2., the results obtained in [13], [14], (registrations) [24]). With the Cantor’s theorem - in complete metric space (proof by Karol Pąk in [22]), we formalize “The Nested Intervals Theorem in 1-dimensional Euclidean metric space”. Pierre Cousin’s proof in 1892 [18] the lemma, published in 1895 [9] states that: “Soit, sur le plan YOX, une aire connexe S limitée par un contour fermé simple ou complexe; on suppose qu’à chaque point de S ou de son périmètre correspond un cercle, de rayon non nul, ayant ce point pour centre : il est alors toujours possible de subdiviser S en régions, en nombre fini et assez petites pour que chacune d’elles soit complétement intérieure au cercle correspondant à un point convenablement choisi dans S ou sur son périmètre.” (In the plane YOX let S be a connected area bounded by a closed contour, simple or complex; one supposes that at each point of S or its perimeter there is a circle, of non-zero radius, having this point as its centre; it is then always possible to subdivide S into regions, finite in number and sufficiently small for each one of them to be entirely inside a circle corresponding to a suitably chosen point in S or on its perimeter) [23]. Cousin’s Lemma, used in Henstock and Kurzweil integral [29] (generalized Riemann integral), state that: “for any gauge δ, there exists at least one δ-fine tagged partition”. In the last section, we formalize this theorem. We use the suggestions given to the Cousin’s Theorem p.11 in [5] and with notations: [4], [29], [19], [28] and [12].

Publié le : 2016-01-01
EUDML-ID : urn:eudml:doc:287134
@article{bwmeta1.element.doi-10_1515_forma-2016-0009,
     author = {Roland Coghetto},
     title = {Cousin's Lemma},
     journal = {Formalized Mathematics},
     volume = {24},
     year = {2016},
     pages = {107-119},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0009}
}
Roland Coghetto. Cousin’s Lemma. Formalized Mathematics, Tome 24 (2016) pp. 107-119. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0009/