References
- Cesare Arzelà. Sulle funzioni di linee. Mem. Accad. Sci. Ist. Bologna Cl. Sci. Fis. Mat., 5(5):55–74, 1895.
- 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.
- Bruce K. Driver. Analysis Tools with Applications. Springer, Berlin, 2003.
- John L. Kelley. General Topology, volume I, II. von Nostrand, 1955.
- Serge Lang. Real and Functional Analysis (Texts in Mathematics). Springer-Verlag, 1993.
- 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.
- Kazuo Matsuzaka. Sets and Topology (Introduction to Mathematics). IwanamiShoten, 2000.
- Keiichi Miyajima and Hiroshi Yamazaki. Compactness of neural networks. Formalized Mathematics, 30(1):13–21, 2022. doi:10.2478/forma-2022-0002.
- Tohru Ozawa. Ascoli-Arzelà theorem. 2012.
- Michael Read and Barry Simon. Functional Analysis (Methods of Modern Mathematical Physics). Academic Press, 1980.
- 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.
- Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991.
- Laurent Schwartz. Théorie des ensembles et topologie, tome 1. Analyse. Hermann, 1997.
- Laurent Schwartz. Calcul différentiel, tome 2. Analyse. Hermann, 1997.
- Hiroshi Yamazaki, Keiichi Miyajima, and Yasunari Shidama. Ascoli-Arzelà theorem. Formalized Mathematics, 29(2):87–94, 2021. doi:10.2478/forma-2021-0009.
- Kôsaku Yosida. Functional Analysis. Springer, 1980.