Ascoli-Arzelà Theorem (Metric Space Version)

Keiichi Miyajima; Hiroshi Yamazaki

doi:10.2478/forma-2024-0011

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

Ascoli-Arzelà Theorem (Metric Space Version)

Formalized Mathematics

Volume 32 (2024): Issue 1 (August 2024)

By: Keiichi Miyajima and Hiroshi Yamazaki

Open Access

|Dec 2024

Abstract

We formulate and prove in Mizar the Ascoli-Arzelà’s 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.

References

Cesare Arzelà. Sulle funzioni di linee. Mem. Accad. Sci. Ist. Bologna Cl. Sci. Fis. Mat., 5(5):55–74, 1895.
Search in Google Scholar Back to article
Giulio Ascoli. Le curve limite di una varietà data di curve. Atti della R. Accad. Dei Lincei Memorie della Cl. Sci. Fis. Mat. Nat., 18(3):521–586, 1883–1884.
Search in Google Scholar Back to article
Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003.
Search in Google Scholar Back to article
John L. Kelley. General Topology, volume I, II. von Nostrand, 1955.
Search in Google Scholar Back to article
Serge Lang. Real and Functional Analysis (Texts in Mathematics). Springer-Verlag, 1993.
Search in Google Scholar Back to article
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–381, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145/3372885.3373824.
Open DOI Search in Google Scholar Back to article
Kazuo Matsuzaka. Sets and Topology (Introduction to Mathematics). IwanamiShoten, 2000.
Search in Google Scholar Back to article
Keiichi Miyajima and Hiroshi Yamazaki. Compactness of neural networks. Formalized Mathematics, 30(1):13–21, 2022. doi:10.2478/forma-2022-0002.
Open DOI 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
Colin Rothgang, Artur Korniłowicz, and Florian Rabe. A new export of the Mizar Mathematical Library. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 205–210, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-81097-9 17.
Open DOI Search in Google Scholar Back to article
Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
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
Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.
Search in Google Scholar Back to article
Hiroshi Yamazaki, Keiichi Miyajima, and Yasunari Shidama. Ascoli-Arzelà theorem. Formalized Mathematics, 29(2):87–94, 2021. doi:10.2478/forma-2021-0009.
Open DOI 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-2024-0011 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 141 - 147

Submitted on: Nov 28, 2024

Published on: Dec 31, 2024

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

Ascoli-Arzelà theorem,

equicontinuousness of continuous functions,

equiboundedness of continuous functions

Related subjects:

Mathematics,

Logic and set theory,

Computer sciences,

Artificial intelligence

© 2024 Keiichi Miyajima, Hiroshi Yamazaki, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Volume 32 (2024): Issue 1 (August 2024)