{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:08:30Z","timestamp":1783901310138,"version":"3.55.0"},"reference-count":16,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T00:00:00Z","timestamp":1722470400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,8,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We formulate and prove in Mizar the Ascoli-Arzel\u00e0\u2019s theorem, which gives necessary and sufficient conditions for a collection of continuous functions to be compact. We use the metric space setting, and the notions of equicontinuousness and equiboundedness of a set of continuous functions are utilized.<\/jats:p>","DOI":"10.2478\/forma-2024-0011","type":"journal-article","created":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T10:22:48Z","timestamp":1735726968000},"page":"141-147","source":"Crossref","is-referenced-by-count":0,"title":["Ascoli-Arzel\u00e0 Theorem (Metric Space Version)"],"prefix":"10.2478","volume":"32","author":[{"given":"Keiichi","family":"Miyajima","sequence":"first","affiliation":[{"name":"Ibaraki University, Faculty of Engineering Hitachi , Ibaraki , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hiroshi","family":"Yamazaki","sequence":"additional","affiliation":[{"name":"Nagano Prefectural Institute of Technology Nagano , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2024,12,31]]},"reference":[{"key":"2026071214473758102_j_forma-2024-0011_ref_001","unstructured":"Cesare Arzel\u00e0. Sulle funzioni di linee. Mem. Accad. Sci. Ist. Bologna Cl. Sci. Fis. Mat., 5(5):55\u201374, 1895."},{"key":"2026071214473758102_j_forma-2024-0011_ref_002","unstructured":"Giulio Ascoli. Le curve limite di una variet\u00e0 data di curve. Atti della R. Accad. Dei Lincei Memorie della Cl. Sci. Fis. Mat. Nat., 18(3):521\u2013586, 1883\u20131884."},{"key":"2026071214473758102_j_forma-2024-0011_ref_003","unstructured":"Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003."},{"key":"2026071214473758102_j_forma-2024-0011_ref_004","unstructured":"John L. Kelley. General Topology, volume I, II. von Nostrand, 1955."},{"key":"2026071214473758102_j_forma-2024-0011_ref_005","doi-asserted-by":"crossref","unstructured":"Serge Lang. Real and Functional Analysis (Texts in Mathematics). Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4612-0897-6"},{"key":"2026071214473758102_j_forma-2024-0011_ref_006","doi-asserted-by":"crossref","unstructured":"The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367\u2013381, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145\/3372885.3373824.","DOI":"10.1145\/3372885.3373824"},{"key":"2026071214473758102_j_forma-2024-0011_ref_007","unstructured":"Kazuo Matsuzaka. Sets and Topology (Introduction to Mathematics). IwanamiShoten, 2000."},{"key":"2026071214473758102_j_forma-2024-0011_ref_008","doi-asserted-by":"crossref","unstructured":"Keiichi Miyajima and Hiroshi Yamazaki. Compactness of neural networks. Formalized Mathematics, 30(1):13\u201321, 2022. doi:10.2478\/forma-2022-0002.","DOI":"10.2478\/forma-2022-0002"},{"key":"2026071214473758102_j_forma-2024-0011_ref_009","unstructured":"Tohru Ozawa. Ascoli-Arzel\u00e0 theorem. 2012."},{"key":"2026071214473758102_j_forma-2024-0011_ref_010","unstructured":"Michael Read and Barry Simon. Functional Analysis (Methods of Modern Mathematical Physics). Academic Press, 1980."},{"key":"2026071214473758102_j_forma-2024-0011_ref_011","doi-asserted-by":"crossref","unstructured":"Colin Rothgang, Artur Korni\u0142owicz, and Florian Rabe. A new export of the Mizar Mathematical Library. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 205\u2013210, Cham, 2021. Springer International Publishing. doi:10.1007\/978-3-030-81097-9 17.","DOI":"10.1007\/978-3-030-81097-9_17"},{"key":"2026071214473758102_j_forma-2024-0011_ref_012","unstructured":"Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991."},{"key":"2026071214473758102_j_forma-2024-0011_ref_013","unstructured":"Laurent Schwartz. Th\u00e9orie des ensembles et topologie, tome 1. Analyse. Hermann, 1997."},{"key":"2026071214473758102_j_forma-2024-0011_ref_014","unstructured":"Laurent Schwartz. Calcul diff\u00e9rentiel, tome 2. Analyse. Hermann, 1997."},{"key":"2026071214473758102_j_forma-2024-0011_ref_015","doi-asserted-by":"crossref","unstructured":"Hiroshi Yamazaki, Keiichi Miyajima, and Yasunari Shidama. Ascoli-Arzel\u00e0 theorem. Formalized Mathematics, 29(2):87\u201394, 2021. doi:10.2478\/forma-2021-0009.","DOI":"10.2478\/forma-2021-0009"},{"key":"2026071214473758102_j_forma-2024-0011_ref_016","unstructured":"K\u00f4saku Yosida. Functional Analysis. Springer, 1980."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2024-0011","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,12]],"date-time":"2026-07-12T23:25:05Z","timestamp":1783898705000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2024-0011"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,1]]},"references-count":16,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2024,12,31]]},"published-print":{"date-parts":[[2024,8,1]]}},"alternative-id":["10.2478\/forma-2024-0011"],"URL":"https:\/\/doi.org\/10.2478\/forma-2024-0011","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,1]]}}}