{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,7]],"date-time":"2026-04-07T17:15:08Z","timestamp":1775582108423,"version":"3.50.1"},"reference-count":27,"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>In [21], Marco Riccardi formalized that \u211dN-basis <jats:italic>n<\/jats:italic> is a basis (in the algebraic sense defined in [26]) of <jats:inline-formula>\n                     <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2016-0010_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                           <m:mrow>\n                              <m:msubsup>\n                                 <m:mi>\u2130<\/m:mi>\n                                 <m:mi>T<\/m:mi>\n                                 <m:mi>n<\/m:mi>\n                              <\/m:msubsup>\n                           <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>${\\cal E}_T^n $<\/jats:tex-math>\n                     <\/jats:alternatives>\n                  <\/jats:inline-formula> and in [20] he has formalized that <jats:inline-formula>\n                     <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2016-0010_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                           <m:mrow>\n                              <m:msubsup>\n                                 <m:mi>\u2130<\/m:mi>\n                                 <m:mi>T<\/m:mi>\n                                 <m:mi>n<\/m:mi>\n                              <\/m:msubsup>\n                           <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>${\\cal E}_T^n $<\/jats:tex-math>\n                     <\/jats:alternatives>\n                  <\/jats:inline-formula> is second-countable, we build (in the topological sense defined in [23]) a denumerable base of <jats:inline-formula>\n                     <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2016-0010_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                           <m:mrow>\n                              <m:msubsup>\n                                 <m:mi>\u2130<\/m:mi>\n                                 <m:mi>T<\/m:mi>\n                                 <m:mi>n<\/m:mi>\n                              <\/m:msubsup>\n                           <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>${\\cal E}_T^n $<\/jats:tex-math>\n                     <\/jats:alternatives>\n                  <\/jats:inline-formula>.<\/jats:p>\n               <jats:p>Then we introduce the <jats:italic>n<\/jats:italic>-dimensional intervals (interval in <jats:italic>n<\/jats:italic>-dimensional Euclidean space, <jats:italic>pav\u00e9 (born\u00e9) de<\/jats:italic> \u211d<jats:italic>\n                     <jats:sup>n<\/jats:sup>\n                  <\/jats:italic>[16], <jats:italic>semi-intervalle (born\u00e9) de<\/jats:italic> \u211d<jats:italic>\n                     <jats:sup>n<\/jats:sup>\n                  <\/jats:italic>[22]).<\/jats:p>\n               <jats:p>We conclude with the definition of Chebyshev distance [11].<\/jats:p>","DOI":"10.1515\/forma-2016-0010","type":"journal-article","created":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T10:01:46Z","timestamp":1481536906000},"page":"121-141","source":"Crossref","is-referenced-by-count":39,"title":["Chebyshev Distance"],"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":"2021040619214482400_j_forma-2016-0010_ref_001_w2aab2b8b7b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. K\u00f6nig\u2019s theorem. Formalized Mathematics, 1(3):589\u2013593, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_002_w2aab2b8b7b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. On powers of cardinals. Formalized Mathematics, 3(1):89\u201393, 1992."},{"key":"2021040619214482400_j_forma-2016-0010_ref_003_w2aab2b8b7b1b7b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_004_w2aab2b8b7b1b7b1ab1ab4Aa","unstructured":"[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107\u2013114, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_005_w2aab2b8b7b1b7b1ab1ab5Aa","unstructured":"[5] Czes\u0142aw Byli\u0144ski. The complex numbers. Formalized Mathematics, 1(3):507\u2013513, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_006_w2aab2b8b7b1b7b1ab1ab6Aa","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":"2021040619214482400_j_forma-2016-0010_ref_007_w2aab2b8b7b1b7b1ab1ab7Aa","unstructured":"[7] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55\u201365, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_008_w2aab2b8b7b1b7b1ab1ab8Aa","unstructured":"[8] Czes\u0142aw Byli\u0144ski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661\u2013668, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_009_w2aab2b8b7b1b7b1ab1ab9Aa","unstructured":"[9] Czes\u0142aw Byli\u0144ski. Some basic properties of sets. Formalized Mathematics, 1(1):47\u201353, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_010_w2aab2b8b7b1b7b1ab1ac10Aa","unstructured":"[10] Agata Darmochwa\u0142. The Euclidean space. Formalized Mathematics, 2(4):599\u2013603, 1991."},{"key":"2021040619214482400_j_forma-2016-0010_ref_011_w2aab2b8b7b1b7b1ab1ac11Aa","unstructured":"[11] Michel Marie Deza and Elena Deza. Encyclopedia of distances. Springer, 2009."},{"key":"2021040619214482400_j_forma-2016-0010_ref_012_w2aab2b8b7b1b7b1ab1ac12Aa","unstructured":"[12] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definitions and basic properties of measurable functions. Formalized Mathematics, 9(3):495\u2013500, 2001."},{"key":"2021040619214482400_j_forma-2016-0010_ref_013_w2aab2b8b7b1b7b1ab1ac13Aa","unstructured":"[13] Adam Grabowski. On the subcontinua of a real line. Formalized Mathematics, 11(3): 313\u2013322, 2003."},{"key":"2021040619214482400_j_forma-2016-0010_ref_014_w2aab2b8b7b1b7b1ab1ac14Aa","unstructured":"[14] Adam Grabowski. On the Borel families of subsets of topological spaces. Formalized Mathematics, 13(4):453\u2013461, 2005."},{"key":"2021040619214482400_j_forma-2016-0010_ref_015_w2aab2b8b7b1b7b1ab1ac15Aa","doi-asserted-by":"crossref","unstructured":"[15] Artur Korni\u0142owicz. The correspondence between n-dimensional Euclidean space and the product of n real lines. Formalized Mathematics, 18(1):81\u201385, 2010. doi:10.2478\/v10037-010-0011-0.","DOI":"10.2478\/v10037-010-0011-0"},{"key":"2021040619214482400_j_forma-2016-0010_ref_016_w2aab2b8b7b1b7b1ab1ac16Aa","unstructured":"[16] Jean Mawhin. Analyse: fondements, techniques, \u00e9volution. De Boeck, 1992."},{"key":"2021040619214482400_j_forma-2016-0010_ref_017_w2aab2b8b7b1b7b1ab1ac17Aa","unstructured":"[17] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147\u2013152, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_018_w2aab2b8b7b1b7b1ab1ac18Aa","doi-asserted-by":"crossref","unstructured":"[18] Karol Pak. Tietze extension theorem for n-dimensional spaces. Formalized Mathematics, 22(1):11\u201319, 2014. doi:10.2478\/forma-2014-0002.","DOI":"10.2478\/forma-2014-0002"},{"key":"2021040619214482400_j_forma-2016-0010_ref_019_w2aab2b8b7b1b7b1ab1ac19Aa","unstructured":"[19] Jan Popio\u0142ek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263\u2013264, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_020_w2aab2b8b7b1b7b1ab1ac20Aa","doi-asserted-by":"crossref","unstructured":"[20] Marco Riccardi. The definition of topological manifolds. Formalized Mathematics, 19(1): 41\u201344, 2011. doi:10.2478\/v10037-011-0007-4.","DOI":"10.2478\/v10037-011-0007-4"},{"key":"2021040619214482400_j_forma-2016-0010_ref_021_w2aab2b8b7b1b7b1ab1ac21Aa","doi-asserted-by":"crossref","unstructured":"[21] Marco Riccardi. Planes and spheres as topological manifolds. Stereographic projection. Formalized Mathematics, 20(1):41\u201345, 2012. doi:10.2478\/v10037-012-0006-0.","DOI":"10.2478\/v10037-012-0006-0"},{"key":"2021040619214482400_j_forma-2016-0010_ref_022_w2aab2b8b7b1b7b1ab1ac22Aa","unstructured":"[22] Jean Schmets. Analyse mathematique. Notes de cours, Universit\u00e9 de Li\u00e8ge, 337 pages, 2004."},{"key":"2021040619214482400_j_forma-2016-0010_ref_023_w2aab2b8b7b1b7b1ab1ac23Aa","unstructured":"[23] Alexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233\u2013236, 1996."},{"key":"2021040619214482400_j_forma-2016-0010_ref_024_w2aab2b8b7b1b7b1ab1ac24Aa","unstructured":"[24] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329\u2013334, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_025_w2aab2b8b7b1b7b1ab1ac25Aa","unstructured":"[25] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575\u2013579, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_026_w2aab2b8b7b1b7b1ab1ac26Aa","unstructured":"[26] Wojciech A. Trybulec. Basis of real linear space. Formalized Mathematics, 1(5):847\u2013850, 1990."},{"key":"2021040619214482400_j_forma-2016-0010_ref_027_w2aab2b8b7b1b7b1ab1ac27Aa","unstructured":"[27] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181\u2013186, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/2\/article-p121.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0010","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T00:25:38Z","timestamp":1617755138000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0010"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,1]]},"references-count":27,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,12,8]]},"published-print":{"date-parts":[[2016,6,1]]}},"alternative-id":["10.1515\/forma-2016-0010"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0010","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]]}}}