<abstract xmlns="http://www.w3.org/1999/xhtml">
<p><bold>Summary</bold>. 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.</p>
</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.

Ascoli-Arzelà Theorem

Nagano Prefectural Institute of Technology Nagano

Ibaraki University Faculty of Engineering Hitachi

Formalized Mathematics

{"article-title":"Ascoli-Arzelà Theorem"}

Summary. In this article we formalize the Ascoli-Arzelà theorem [5], [6], [8] in Mizar [1], [2]. First, we gave definitions of equicontinuousness and...

Ascoli-Arzelà Theorem

Article Category: Artikel

Online veröffentlicht: 30. Dez. 2021

Seitenbereich: 87 - 94

Akzeptiert: 30. Juni 2021

DOI: https://doi.org/10.2478/forma-2021-0009

Schlüsselwörter
Ascoli-Arzela’s theorem, equicontinuousness of continuous functions, equiboundedness of continuous functions

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Ascoli-Arzelà Theorem

Article Category: Artikel

Online veröffentlicht: 30. Dez. 2021

Seitenbereich: 87 - 94

Akzeptiert: 30. Juni 2021

DOI: https://doi.org/10.2478/forma-2021-0009

SchlüsselwörterAscoli-Arzela’s theorem, equicontinuousness of continuous functions, equiboundedness of continuous functions

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Schlüsselwörter
Ascoli-Arzela’s theorem, equicontinuousness of continuous functions, equiboundedness of continuous functions