{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T13:58:31Z","timestamp":1648821511117},"reference-count":19,"publisher":"Walter de Gruyter GmbH","issue":"3","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,9,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p> First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fr\u00e9chet filters on \u2115 (F<jats:sub>1<\/jats:sub>) with the Fr\u00e9chet filter on \u2115 \u00d7 \u2115 (F<jats:sub>2<\/jats:sub>), we compare lim<jats:sub>F\u2081<\/jats:sub> and lim<jats:sub>F\u2082<\/jats:sub> for all double sequences in a non empty topological space.<\/jats:p>\n               <jats:p>Endou, Okazaki and Shidama formalized in [14] the \u201cconvergence in Pringsheim\u2019s sense\u201d for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/2016.24.3.173.jpg\" \/> converges in \u201cPringsheim\u2019s sense\u201d but not in Frechet filter on \u2115 \u00d7 \u2115 sense.<\/jats:p>\n               <jats:p>In the next section, we generalize some definitions: \u201cis convergent in the first coordinate\u201d, \u201cis convergent in the second coordinate\u201d, \u201cthe lim in the first coordinate of\u201d, \u201cthe lim in the second coordinate of\u201d according to [14], in Hausdorff space.<\/jats:p>\n               <jats:p>Finally, we generalize two theorems: (3) and (4) from [14] in the case of double sequences and we formalize the \u201citerated limit\u201d theorem (\u201cDouble limit\u201d [7], p. 81, par. 8.5 \u201cDouble limite\u201d [6] (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5) [17] and the corrections B.10 [18].<\/jats:p>","DOI":"10.1515\/forma-2016-0014","type":"journal-article","created":{"date-parts":[[2017,2,14]],"date-time":"2017-02-14T10:02:03Z","timestamp":1487066523000},"page":"173-186","source":"Crossref","is-referenced-by-count":0,"title":["Double Sequences and Iterated Limits in Regular Space"],"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":[[2017,2,21]]},"reference":[{"key":"2021040611133354921_j_forma-2016-0014_ref_1_w2aab2b8c12b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990."},{"key":"2021040611133354921_j_forma-2016-0014_ref_2_w2aab2b8c12b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93-107, 1997."},{"key":"2021040611133354921_j_forma-2016-0014_ref_3_w2aab2b8c12b1b7b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990."},{"key":"2021040611133354921_j_forma-2016-0014_ref_4_w2aab2b8c12b1b7b1ab1ab4Aa","unstructured":"[4] Grzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733-738, 2001."},{"key":"2021040611133354921_j_forma-2016-0014_ref_5_w2aab2b8c12b1b7b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Grzegorz Bancerek, Czes\u0142aw Bylinski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2021040611133354921_j_forma-2016-0014_ref_6_w2aab2b8c12b1b7b1ab1ab6Aa","doi-asserted-by":"crossref","unstructured":"[6] Nicolas Bourbaki. Topologie g\u00e9n\u00e9rale: Chapitres 1 \u00e0 4. El\u00e9ments de math\u00e9matique. Springer Science & Business Media, 2007.","DOI":"10.1007\/978-3-540-34486-5_1"},{"key":"2021040611133354921_j_forma-2016-0014_ref_7_w2aab2b8c12b1b7b1ab1ab7Aa","unstructured":"[7] Nicolas Bourbaki. General Topology: Chapters 1-4. Springer Science and Business Media, 2013."},{"key":"2021040611133354921_j_forma-2016-0014_ref_8_w2aab2b8c12b1b7b1ab1ab8Aa","unstructured":"[8] Czes\u0142aw Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990."},{"key":"2021040611133354921_j_forma-2016-0014_ref_9_w2aab2b8c12b1b7b1ab1ab9Aa","unstructured":"[9] Czes\u0142aw Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990."},{"key":"2021040611133354921_j_forma-2016-0014_ref_10_w2aab2b8c12b1b7b1ab1ac10Aa","unstructured":"[10] Czes\u0142aw Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990."},{"key":"2021040611133354921_j_forma-2016-0014_ref_11_w2aab2b8c12b1b7b1ab1ac11Aa","unstructured":"[11] Czes\u0142aw Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990."},{"key":"2021040611133354921_j_forma-2016-0014_ref_12_w2aab2b8c12b1b7b1ab1ac12Aa","doi-asserted-by":"crossref","unstructured":"[12] Roland Coghetto. Convergent filter bases. Formalized Mathematics, 23(3):189-203, 2015. doi:10.1515\/forma-2015-0016.","DOI":"10.1515\/forma-2015-0016"},{"key":"2021040611133354921_j_forma-2016-0014_ref_13_w2aab2b8c12b1b7b1ab1ac13Aa","doi-asserted-by":"crossref","unstructured":"[13] Roland Coghetto. Summable family in a commutative group. Formalized Mathematics, 23(4):279-288, 2015. doi:10.1515\/forma-2015-0022.","DOI":"10.1515\/forma-2015-0022"},{"key":"2021040611133354921_j_forma-2016-0014_ref_14_w2aab2b8c12b1b7b1ab1ac14Aa","doi-asserted-by":"crossref","unstructured":"[14] Noboru Endou, Hiroyuki Okazaki, and Yasunari Shidama. Double sequences and limits. Formalized Mathematics, 21(3):163-170, 2013. doi:10.2478\/forma-2013-0018.","DOI":"10.2478\/forma-2013-0018"},{"key":"2021040611133354921_j_forma-2016-0014_ref_15_w2aab2b8c12b1b7b1ab1ac15Aa","doi-asserted-by":"crossref","unstructured":"[15] Andrzej Owsiejczuk. Combinatorial Grassmannians. Formalized Mathematics, 15(2):27-33, 2007. doi:10.2478\/v10037-007-0004-9.","DOI":"10.2478\/v10037-007-0004-9"},{"key":"2021040611133354921_j_forma-2016-0014_ref_16_w2aab2b8c12b1b7b1ab1ac16Aa","unstructured":"[16] Karol Pak. Stirling numbers of the second kind. Formalized Mathematics, 13(2):337-345, 2005."},{"key":"2021040611133354921_j_forma-2016-0014_ref_17_w2aab2b8c12b1b7b1ab1ac17Aa","unstructured":"[17] Claude Wagschal. Topologie et analyse fonctionnelle. Hermann, 1995."},{"key":"2021040611133354921_j_forma-2016-0014_ref_18_w2aab2b8c12b1b7b1ab1ac18Aa","unstructured":"[18] Claude Wagschal. Topologie: Exercices et probl\u00e9mes corrig\u00e9s. Hermann, 1995."},{"key":"2021040611133354921_j_forma-2016-0014_ref_19_w2aab2b8c12b1b7b1ab1ac19Aa","unstructured":"[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/3\/article-p173.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0014","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T16:04:11Z","timestamp":1617725051000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0014"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,1]]},"references-count":19,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2017,2,21]]},"published-print":{"date-parts":[[2016,9,1]]}},"alternative-id":["10.1515\/forma-2016-0014"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0014","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,1]]}}}