Ascoli-Arzelà Theorem

Hiroshi Yamazaki; Keiichi Miyajima; Yasunari Shidama

doi:10.2478/forma-2021-0009

.blurhash-client-img { display: none !important; }

Ascoli-Arzelà Theorem

Formalized Mathematics

Volume 29 (2021): Issue 2 (July 2021)

By: Hiroshi Yamazaki, Keiichi Miyajima and Yasunari Shidama

Open Access

|Dec 2021

Abstract

Summary. In 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.

References

Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, 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.10.1007/978-3-319-20615-8_17
Search in Google Scholar Back to article
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. 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.10.1007/s10817-017-9440-6604425130069070
Search in Google Scholar Back to article
Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003.
Search in Google Scholar Back to article
Noboru 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.10.2478/v10037-006-0024-x
Search in Google Scholar Back to article
Serge Lang. Real and Functional Analysis (Texts in Mathematics). Springer-Verlag, 1993.10.1007/978-1-4612-0897-6
Search in Google Scholar Back to article
Kazuo Matsuzaka. Sets and Topology (Introduction to Mathematics). IwanamiShoten, 2000.
Search in Google Scholar Back to article
Tohru Ozawa. Ascoli-Arzelà theorem. 2012.
Search in Google Scholar Back to article
Michael Read and Barry Simon. Functional Analysis (Methods of Modern Mathematical Physics). Academic Press, 1980.
Search in Google Scholar Back to article
Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.
Search in Google Scholar Back to article
Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama. Banach space of absolute summable real sequences. Formalized Mathematics, 11(4):377–380, 2003.
Search in Google Scholar Back to article
Hiroshi 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.10.2478/forma-2021-0005
Search in Google Scholar Back to article
Kôsaku Yosida. Functional Analysis. Springer, 1980.
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.2478/forma-2021-0009 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 87 - 94

Accepted on: Jun 30, 2021

Published on: Dec 30, 2021

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

46B50,

68V20

Related subjects:

Computer sciences,

Computer sciences, other,

Mathematics,

General mathematics

© 2021 Hiroshi Yamazaki, Keiichi Miyajima, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Volume 29 (2021): Issue 2 (July 2021)