<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

Published Online: Dec 30, 2021

Page range: 87 - 94

Accepted: Jun 30, 2021

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

Keywords
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

Published Online: Dec 30, 2021

Page range: 87 - 94

Accepted: Jun 30, 2021

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

KeywordsAscoli-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

Keywords
Ascoli-Arzela’s theorem, equicontinuousness of continuous functions, equiboundedness of continuous functions