<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

Data publikacji: 30 gru 2021

Zakres stron: 87 - 94

Przyjęty: 30 cze 2021

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

Słowa kluczowe
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

Data publikacji: 30 gru 2021

Zakres stron: 87 - 94

Przyjęty: 30 cze 2021

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

Słowa kluczoweAscoli-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

Słowa kluczowe
Ascoli-Arzela’s theorem, equicontinuousness of continuous functions, equiboundedness of continuous functions