{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T21:56:35Z","timestamp":1649109395106},"reference-count":12,"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> In this article, using mostly Pervin [9], Kunzi [6], [8], [7], Williams [11] and Bourbaki [3] works, we formalize in Mizar [2] the notions of quasiuniform space, semi-uniform space and locally uniform space.<\/jats:p>\n               <jats:p>We define the topology induced by a quasi-uniform space. Finally we formalize from the sets of the form ((X \\ \u03a9) \u00d7 X) \u222a (X \u00d7 \u03a9), the Csaszar-Pervin quasi-uniform space induced by a topological space.<\/jats:p>","DOI":"10.1515\/forma-2016-0017","type":"journal-article","created":{"date-parts":[[2017,2,14]],"date-time":"2017-02-14T10:02:03Z","timestamp":1487066523000},"page":"205-214","source":"Crossref","is-referenced-by-count":1,"title":["Quasi-uniform 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":"2021040801354962055_j_forma-2016-0017_ref_1_w2aab2b8b6b1b7b1ab1ab1Aa","unstructured":"[1] William W. Armstrong, Yatsuka Nakamura, and Piotr Rudnicki. Armstrong\u2019s axioms. Formalized Mathematics, 11(1):39-51, 2003."},{"key":"2021040801354962055_j_forma-2016-0017_ref_2_w2aab2b8b6b1b7b1ab1ab2Aa","doi-asserted-by":"crossref","unstructured":"[2] 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":"2021040801354962055_j_forma-2016-0017_ref_3_w2aab2b8b6b1b7b1ab1ab3Aa","unstructured":"[3] Nicolas Bourbaki. General Topology: Chapters 1-4. Springer Science and Business Media, 2013."},{"key":"2021040801354962055_j_forma-2016-0017_ref_4_w2aab2b8b6b1b7b1ab1ab4Aa","unstructured":"[4] Czes\u0142aw Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990."},{"key":"2021040801354962055_j_forma-2016-0017_ref_5_w2aab2b8b6b1b7b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] 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":"2021040801354962055_j_forma-2016-0017_ref_6_w2aab2b8b6b1b7b1ab1ab6Aa","unstructured":"[6] Hans-Peter A. K\u00fcnzi. Quasi-uniform spaces - eleven years later. In Topology Proceedings, volume 18, pages 143-171, 1993."},{"key":"2021040801354962055_j_forma-2016-0017_ref_7_w2aab2b8b6b1b7b1ab1ab7Aa","doi-asserted-by":"crossref","unstructured":"[7] Hans-Peter A. K\u00fcnzi. An introduction to quasi-uniform spaces. Beyond Topology, 486: 239-304, 2009.","DOI":"10.1090\/conm\/486\/09511"},{"key":"2021040801354962055_j_forma-2016-0017_ref_8_w2aab2b8b6b1b7b1ab1ab8Aa","unstructured":"[8] Hans-Peter A. K\u00fcnzi and Carolina Ryser. The Bourbaki quasi-uniformity. In Topology Proceedings, volume 20, pages 161-183, 1995."},{"key":"2021040801354962055_j_forma-2016-0017_ref_9_w2aab2b8b6b1b7b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] William J. Pervin. Quasi-uniformization of topological spaces. Mathematische Annalen, 147(4):316-317, 1962.","DOI":"10.1007\/BF01440953"},{"key":"2021040801354962055_j_forma-2016-0017_ref_10_w2aab2b8b6b1b7b1ab1ac10Aa","unstructured":"[10] Alexander Yu. Shibakov and Andrzej Trybulec. The Cantor set. Formalized Mathematics, 5(2):233-236, 1996."},{"key":"2021040801354962055_j_forma-2016-0017_ref_11_w2aab2b8b6b1b7b1ab1ac11Aa","doi-asserted-by":"crossref","unstructured":"[11] James Williams. Locally uniform spaces. Transactions of the American Mathematical Society, 168:435-469, 1972.","DOI":"10.1090\/S0002-9947-1972-0296891-5"},{"key":"2021040801354962055_j_forma-2016-0017_ref_12_w2aab2b8b6b1b7b1ab1ac12Aa","unstructured":"[12] Miros\u0142aw Wysocki and Agata Darmochwa\u0142. Subsets of topological spaces. Formalized Mathematics, 1(1):231-237, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/3\/article-p205.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0017","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T09:28:52Z","timestamp":1617874132000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0017"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,1]]},"references-count":12,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2017,2,21]]},"published-print":{"date-parts":[[2016,9,1]]}},"alternative-id":["10.1515\/forma-2016-0017"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0017","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,1]]}}}