Zitieren

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.

eISSN:
1898-9934
Sprache:
Englisch
Zeitrahmen der Veröffentlichung:
Volume Open
Fachgebiete der Zeitschrift:
Informatik, andere, Mathematik, Allgemeines