Cousin’s Lemma

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 1892the lemma, published in 1895states that:(In the plane YOX letbe a connected area bounded by a closed contour, simple or complex; one supposes that at each point ofor its perimeter there is a circle, of non-zero radius, having this point as its centre; it is then always possible to subdivideinto regions, finite in number and sufficiently small for each one of them to be entirely inside a circle corresponding to a suitably chosen point inor on its perimeter). [18] [9] [23]

“Soit, sur le plan YOX, une aire connexelimitée par un contour fermé simple ou complexe; on suppose qu’à chaque point deou de son périmètre correspond un cercle, de rayon non nul, ayant ce point pour centre : il est alors toujours possible de subdiviseren 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 dansou sur son périmètre.” S S S S

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].