{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T20:05:22Z","timestamp":1648929922790},"reference-count":29,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2016,6,1]],"date-time":"2016-06-01T00:00:00Z","timestamp":1464739200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,6,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>We formalize, in two different ways, that \u201cthe <jats:italic>n<\/jats:italic>-dimensional Euclidean metric space is a complete metric space\u201d (version 1. with the results obtained in [13], [26], [25] and version 2., the results obtained in [13], [14], (<jats:italic>registrations<\/jats:italic>) [24]).<\/jats:p>\n               <jats:p>With the Cantor\u2019s theorem - in complete metric space (proof by Karol P\u0105k in [22]), we formalize \u201cThe Nested Intervals Theorem in 1-dimensional Euclidean metric space\u201d.<\/jats:p>\n               <jats:p>Pierre Cousin\u2019s proof in 1892 [18] the lemma, published in 1895 [9] states that:\n<jats:disp-quote>\n                     <jats:p xml:lang=\"fr\">\u201cSoit, sur le plan YOX, une aire connexe <jats:italic>S<\/jats:italic> limit\u00e9e par un contour ferm\u00e9 simple ou complexe; on suppose qu\u2019\u00e0 chaque point de <jats:italic>S<\/jats:italic> ou de son p\u00e9rim\u00e8tre correspond un cercle, de rayon non nul, ayant ce point pour centre : il est alors toujours possible de subdiviser <jats:italic>S<\/jats:italic> en r\u00e9gions, en nombre fini et assez petites pour que chacune d\u2019elles soit compl\u00e9tement int\u00e9rieure au cercle correspondant \u00e0 un point convenablement choisi dans <jats:italic>S<\/jats:italic> ou sur son p\u00e9rim\u00e8tre.\u201d<\/jats:p>\n                  <\/jats:disp-quote>\n(In the plane YOX let <jats:italic>S<\/jats:italic> be a connected area bounded by a closed contour, simple or complex; one supposes that at each point of <jats:italic>S<\/jats: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 <jats:italic>S<\/jats: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 <jats:italic>S<\/jats:italic> or on its perimeter) [23].<\/jats:p>\n               <jats:p>Cousin\u2019s Lemma, used in Henstock and Kurzweil integral [29] (generalized Riemann integral), state that: \u201cfor any gauge <jats:italic>\u03b4<\/jats:italic>, there exists at least one <jats:italic>\u03b4<\/jats:italic>-fine tagged partition\u201d. In the last section, we formalize this theorem. We use the suggestions given to the Cousin\u2019s Theorem p.11 in [5] and with notations: [4], [29], [19], [28] and [12].<\/jats:p>","DOI":"10.1515\/forma-2016-0009","type":"journal-article","created":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T10:01:46Z","timestamp":1481536906000},"page":"107-119","source":"Crossref","is-referenced-by-count":1,"title":["Cousin\u2019s Lemma"],"prefix":"10.1515","volume":"24","author":[{"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"Rue de la Brasserie 5, 7100 La Louvi\u00e8re, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2016,12,8]]},"reference":[{"key":"2021040611441877763_j_forma-2016-0009_ref_001_w2aab2b8b5b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. K\u00f6nig\u2019s theorem. Formalized Mathematics, 1(3):589\u2013593, 1990."},{"key":"2021040611441877763_j_forma-2016-0009_ref_002_w2aab2b8b5b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040611441877763_j_forma-2016-0009_ref_003_w2aab2b8b5b1b7b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107\u2013114, 1990."},{"key":"2021040611441877763_j_forma-2016-0009_ref_004_w2aab2b8b5b1b7b1ab1ab4Aa","doi-asserted-by":"crossref","unstructured":"[4] Robert G. Bartle. Return to the Riemann integral. American Mathematical Monthly, pages 625\u2013632, 1996.","DOI":"10.1080\/00029890.1996.12004798"},{"key":"2021040611441877763_j_forma-2016-0009_ref_005_w2aab2b8b5b1b7b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Robert G. Bartle. A modern theory of integration, volume 32. American Mathematical Society Providence, 2001.","DOI":"10.1090\/gsm\/032"},{"key":"2021040611441877763_j_forma-2016-0009_ref_006_w2aab2b8b5b1b7b1ab1ab6Aa","unstructured":"[6] Czes\u0142aw Byli\u0144ski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529\u2013536, 1990."},{"key":"2021040611441877763_j_forma-2016-0009_ref_007_w2aab2b8b5b1b7b1ab1ab7Aa","unstructured":"[7] Czes\u0142aw Byli\u0144ski. Some properties of restrictions of finite sequences. Formalized Mathematics, 5(2):241\u2013245, 1996."},{"key":"2021040611441877763_j_forma-2016-0009_ref_008_w2aab2b8b5b1b7b1ab1ab8Aa","unstructured":"[8] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55\u201365, 1990."},{"key":"2021040611441877763_j_forma-2016-0009_ref_009_w2aab2b8b5b1b7b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] Pierre Cousin. Sur les fonctions de n variables complexes. Acta Mathematica, 19(1):1\u201361, 1895. doi:10.1007\/BF02402869.","DOI":"10.1007\/BF02402869"},{"key":"2021040611441877763_j_forma-2016-0009_ref_010_w2aab2b8b5b1b7b1ab1ac10Aa","unstructured":"[10] Agata Darmochwa\u0142. The Euclidean space. Formalized Mathematics, 2(4):599\u2013603, 1991."},{"key":"2021040611441877763_j_forma-2016-0009_ref_011_w2aab2b8b5b1b7b1ab1ac11Aa","unstructured":"[11] Agata Darmochwa\u0142 and Yatsuka Nakamura. Metric spaces as topological spaces \u2013 fundamental concepts. Formalized Mathematics, 2(4):605\u2013608, 1991."},{"key":"2021040611441877763_j_forma-2016-0009_ref_012_w2aab2b8b5b1b7b1ab1ac12Aa","unstructured":"[12] Noboru Endou and Artur Korni\u0142owicz. The definition of the Riemann definite integral and some related lemmas. Formalized Mathematics, 8(1):93\u2013102, 1999."},{"key":"2021040611441877763_j_forma-2016-0009_ref_013_w2aab2b8b5b1b7b1ab1ac13Aa","unstructured":"[13] Noboru Endou and Yasunari Shidama. Completeness of the real Euclidean space. Formalized Mathematics, 13(4):577\u2013580, 2005."},{"key":"2021040611441877763_j_forma-2016-0009_ref_014_w2aab2b8b5b1b7b1ab1ac14Aa","doi-asserted-by":"crossref","unstructured":"[14] Noboru Endou, Yasunari Shidama, and Katsumasa Okamura. Baire\u2019s category theorem and some spaces generated from real normed space. Formalized Mathematics, 14(4): 213\u2013219, 2006. doi:10.2478\/v10037-006-0024-x.","DOI":"10.2478\/v10037-006-0024-x"},{"key":"2021040611441877763_j_forma-2016-0009_ref_015_w2aab2b8b5b1b7b1ab1ac15Aa","unstructured":"[15] Adam Grabowski and Yatsuka Nakamura. Some properties of real maps. Formalized Mathematics, 6(4):455\u2013459, 1997."},{"key":"2021040611441877763_j_forma-2016-0009_ref_016_w2aab2b8b5b1b7b1ab1ac16Aa","unstructured":"[16] Artur Korni\u0142owicz. Properties of connected subsets of the real line. Formalized Mathematics, 13(2):315\u2013323, 2005."},{"key":"2021040611441877763_j_forma-2016-0009_ref_017_w2aab2b8b5b1b7b1ab1ac17Aa","unstructured":"[17] Rafa\u0142 Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887\u2013890, 1990."},{"key":"2021040611441877763_j_forma-2016-0009_ref_018_w2aab2b8b5b1b7b1ab1ac18Aa","unstructured":"[18] Bernard Maurey and Jean-Pierre Tacchi. La gen\u00e8se du th\u00e9or\u00e8me de recouvrement de Borel. Revue d\u2019histoire des math\u00e9matiques, 11(2):163\u2013204, 2005."},{"key":"2021040611441877763_j_forma-2016-0009_ref_019_w2aab2b8b5b1b7b1ab1ac19Aa","unstructured":"[19] Jean Mawhin. L\u2019\u00e9ternel retour des sommes de Riemann-Stieltjes dans l\u2019\u00e9volution du calcul int\u00e9gral. Bulletin de la Soci\u00e9t\u00e9 Royale des Sciences de Li\u00e8ge, 70(4\u20136):345\u2013364, 2001."},{"key":"2021040611441877763_j_forma-2016-0009_ref_020_w2aab2b8b5b1b7b1ab1ac20Aa","unstructured":"[20] Yatsuka Nakamura and Andrzej Trybulec. A decomposition of a simple closed curves and the order of their points. Formalized Mathematics, 6(4):563\u2013572, 1997."},{"key":"2021040611441877763_j_forma-2016-0009_ref_021_w2aab2b8b5b1b7b1ab1ac21Aa","doi-asserted-by":"crossref","unstructured":"[21] Robin Nittka. Conway\u2019s games and some of their basic properties. Formalized Mathematics, 19(2):73\u201381, 2011. doi:10.2478\/v10037-011-0013-6.","DOI":"10.2478\/v10037-011-0013-6"},{"key":"2021040611441877763_j_forma-2016-0009_ref_022_w2aab2b8b5b1b7b1ab1ac22Aa","doi-asserted-by":"crossref","unstructured":"[22] Karol P\u0105k. Complete spaces. Formalized Mathematics, 16(1):35\u201343, 2008. doi:10.2478\/v10037-008-0006-2.","DOI":"10.2478\/v10037-008-0006-2"},{"key":"2021040611441877763_j_forma-2016-0009_ref_023_w2aab2b8b5b1b7b1ab1ac23Aa","doi-asserted-by":"crossref","unstructured":"[23] Manya Raman-Sundstr\u00f6m. A pedagogical history of compactness. The American Mathematical Monthly, 122(7):619\u2013635, 2015.","DOI":"10.4169\/amer.math.monthly.122.7.619"},{"key":"2021040611441877763_j_forma-2016-0009_ref_024_w2aab2b8b5b1b7b1ab1ac24Aa","doi-asserted-by":"crossref","unstructured":"[24] Hideki Sakurai, Hisayoshi Kunimune, and Yasunari Shidama. Uniform boundedness principle. Formalized Mathematics, 16(1):19\u201321, 2008. doi:10.2478\/v10037-008-0003-5.","DOI":"10.2478\/v10037-008-0003-5"},{"key":"2021040611441877763_j_forma-2016-0009_ref_025_w2aab2b8b5b1b7b1ab1ac25Aa","unstructured":"[25] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39\u201348, 2004."},{"key":"2021040611441877763_j_forma-2016-0009_ref_026_w2aab2b8b5b1b7b1ab1ac26Aa","unstructured":"[26] Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama. Banach space of absolute summable real sequences. Formalized Mathematics, 11(4):377\u2013380, 2003."},{"key":"2021040611441877763_j_forma-2016-0009_ref_027_w2aab2b8b5b1b7b1ab1ac27Aa","unstructured":"[27] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569\u2013573, 1990."},{"key":"2021040611441877763_j_forma-2016-0009_ref_028_w2aab2b8b5b1b7b1ab1ac28Aa","unstructured":"[28] Lee Peng Yee. The integral \u00e0 la Henstock. Scientiae Mathematicae Japonicae, 67(1): 13\u201321, 2008."},{"key":"2021040611441877763_j_forma-2016-0009_ref_029_w2aab2b8b5b1b7b1ab1ac29Aa","unstructured":"[29] Lee Peng Yee and Rudolf Vyborny. Integral: an easy approach after Kurzweil and Henstock, volume 14. Cambridge University Press, 2000."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/2\/article-p107.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0009","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T18:10:10Z","timestamp":1617732610000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0009"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,1]]},"references-count":29,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,12,8]]},"published-print":{"date-parts":[[2016,6,1]]}},"alternative-id":["10.1515\/forma-2016-0009"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0009","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2016,6,1]]}}}