REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/12390
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorYamazaki, Hiroshi-
dc.contributor.authorMiyajima, Keiichi-
dc.contributor.authorShidama, Yasunari-
dc.date.accessioned2022-01-04T06:48:52Z-
dc.date.available2022-01-04T06:48:52Z-
dc.date.issued2021-
dc.identifier.citationFormalized Mathematics, Volume 29, Issue 2, Pages 87-94pl
dc.identifier.issn1426-2630-
dc.identifier.urihttp://hdl.handle.net/11320/12390-
dc.description.abstractIn this article we formalize the Ascoli-Arzelà theorem [5], [6], [8] in Mizar [1], [2]. First, we gave definitions of equicontinuousness and equiboundedness of a set of continuous functions [12], [7], [3], [9]. Next, we formalized the Ascoli-Arzelà theorem using those definitions, and proved this theorem.pl
dc.description.sponsorshipThis work was supported by JSPS KAKENHI Grant Numbers JP17K00182.pl
dc.language.isoenpl
dc.publisherDeGruyter Openpl
dc.rightsAttribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)-
dc.rights.urihttps://creativecommons.org/licenses/by-sa/3.0/-
dc.subjectAscoli-Arzela’s theorempl
dc.subjectequicontinuousness of continuous functionspl
dc.subjectequiboundedness of continuous functionspl
dc.titleAscoli-Arzelà Theorempl
dc.typeArticlepl
dc.rights.holder© 2021 University of Białymstokupl
dc.rights.holderCC-BY-SA License ver. 3.0 or laterpl
dc.identifier.doi10.2478/forma-2021-0009-
dc.description.AffiliationHiroshi Yamazaki - Nagano Prefectural Institute of Technology, Nagano, Japanpl
dc.description.AffiliationKeiichi Miyajima - Ibaraki University Faculty of Engineering, Hitachi, Ibaraki, Japanpl
dc.description.AffiliationYasunari Shidama - Karuizawa Hotch 244-1, Nagano, Japanpl
dc.description.referencesGrzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, 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.pl
dc.description.referencesGrzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.pl
dc.description.referencesBruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003.pl
dc.description.referencesNoboru Endou, Yasunari Shidama, and Katsumasa Okamura. Baire’s category theorem and some spaces generated from real normed space. Formalized Mathematics, 14(4): 213–219, 2006. doi:10.2478/v10037-006-0024-x.pl
dc.description.referencesSerge Lang. Real and Functional Analysis (Texts in Mathematics). Springer-Verlag, 1993.pl
dc.description.referencesKazuo Matsuzaka. Sets and Topology (Introduction to Mathematics). IwanamiShoten, 2000.pl
dc.description.referencesTohru Ozawa. Ascoli-Arzelà theorem. 2012.pl
dc.description.referencesMichael Read and Barry Simon. Functional Analysis (Methods of Modern Mathematical Physics). Academic Press, 1980.pl
dc.description.referencesLaurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.pl
dc.description.referencesYasumasa Suzuki, Noboru Endou, and Yasunari Shidama. Banach space of absolute summable real sequences. Formalized Mathematics, 11(4):377–380, 2003.pl
dc.description.referencesHiroshi Yamazaki, Keiichi Miyajima, and Yasunari Shidama. Functional space consisted by continuous functions on topological space. Formalized Mathematics, 29(1):49–62, 2021. doi:10.2478/forma-2021-0005.pl
dc.description.referencesKôsaku Yosida. Functional Analysis. Springer, 1980.pl
dc.identifier.eissn1898-9934-
dc.description.volume29pl
dc.description.issue2pl
dc.description.firstpage87pl
dc.description.lastpage94pl
dc.identifier.citation2Formalized Mathematicspl
Występuje w kolekcji(ach):Formalized Mathematics, 2021, Volume 29, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
10.2478_forma-2021-0009.pdf256,79 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons