<abstract xmlns="http://www.w3.org/1999/xhtml">We formalize, in two different ways, that “the <italic>n</italic>-dimensional Euclidean metric space is a complete metric space” (version 1. with the results obtained in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_013_w2aab2b8b5b1b7b1ab1ac13Aa">[13]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_026_w2aab2b8b5b1b7b1ab1ac26Aa">[26]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_025_w2aab2b8b5b1b7b1ab1ac25Aa">[25]</xref> and version 2., the results obtained in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_013_w2aab2b8b5b1b7b1ab1ac13Aa">[13]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_014_w2aab2b8b5b1b7b1ab1ac14Aa">[14]</xref>, (<italic>registrations</italic>) <xref ref-type="bibr" rid="j_forma-2016-0009_ref_024_w2aab2b8b5b1b7b1ab1ac24Aa">[24]</xref>).With the Cantor’s theorem - in complete metric space (proof by Karol Pąk in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_022_w2aab2b8b5b1b7b1ab1ac22Aa">[22]</xref>), we formalize “The Nested Intervals Theorem in 1-dimensional Euclidean metric space”.Pierre Cousin’s proof in 1892 <xref ref-type="bibr" rid="j_forma-2016-0009_ref_018_w2aab2b8b5b1b7b1ab1ac18Aa">[18]</xref> the lemma, published in 1895 <xref ref-type="bibr" rid="j_forma-2016-0009_ref_009_w2aab2b8b5b1b7b1ab1ab9Aa">[9]</xref> states that:
<disp-quote>“Soit, sur le plan YOX, une aire connexe <italic>S</italic> limitée par un contour fermé simple ou complexe; on suppose qu’à chaque point de <italic>S</italic> 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 <italic>S</italic> 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 <italic>S</italic> ou sur son périmètre.”</disp-quote>
(In the plane YOX let <italic>S</italic> be a connected area bounded by a closed contour, simple or complex; one supposes that at each point of <italic>S</italic> or its perimeter there is a circle, of non-zero radius, having this point as its centre; it is then always possible to subdivide <italic>S</italic> 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 <italic>S</italic> or on its perimeter) <xref ref-type="bibr" rid="j_forma-2016-0009_ref_023_w2aab2b8b5b1b7b1ab1ac23Aa">[23]</xref>.Cousin’s Lemma, used in Henstock and Kurzweil integral <xref ref-type="bibr" rid="j_forma-2016-0009_ref_029_w2aab2b8b5b1b7b1ab1ac29Aa">[29]</xref> (generalized Riemann integral), state that: “for any gauge <italic>δ</italic>, there exists at least one <italic>δ</italic>-fine tagged partition”. In the last section, we formalize this theorem. We use the suggestions given to the Cousin’s Theorem p.11 in <xref ref-type="bibr" rid="j_forma-2016-0009_ref_005_w2aab2b8b5b1b7b1ab1ab5Aa">[5]</xref> and with notations: <xref ref-type="bibr" rid="j_forma-2016-0009_ref_004_w2aab2b8b5b1b7b1ab1ab4Aa">[4]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_029_w2aab2b8b5b1b7b1ab1ac29Aa">[29]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_019_w2aab2b8b5b1b7b1ab1ac19Aa">[19]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0009_ref_028_w2aab2b8b5b1b7b1ab1ac28Aa">[28]</xref> and <xref ref-type="bibr" rid="j_forma-2016-0009_ref_012_w2aab2b8b5b1b7b1ab1ac12Aa">[12]</xref>.</abstract>

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

Cousin’s Lemma

Rue de la Brasserie 5, 7100 La Louvière,

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Cousin\u2019s 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],...

Cousin’s Lemma

Online veröffentlicht: 08. Dez. 2016

Seitenbereich: 107 - 119

Eingereicht: 31. Dez. 2015

DOI: https://doi.org/10.1515/forma-2016-0009

Schlüsselwörter
Cousin’s lemma, Cousin’s theorem, nested intervals theorem

© 2016 Roland Coghetto, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Cousin’s Lemma

Online veröffentlicht: 08. Dez. 2016

Seitenbereich: 107 - 119

Eingereicht: 31. Dez. 2015

DOI: https://doi.org/10.1515/forma-2016-0009

SchlüsselwörterCousin’s lemma, Cousin’s theorem, nested intervals theorem

© 2016 Roland Coghetto, published by De Gruyter Open

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Schlüsselwörter
Cousin’s lemma, Cousin’s theorem, nested intervals theorem