Ascoli-Arzelà Theorem
| Autor: | Hiroshi Yamazaki, Keiichi Miyajima, Yasunari Shidama |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | Formalized Mathematics, Vol 29, Iss 2, Pp 87-94 (2021) |
| ISSN: | 1898-9934 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|