Cite

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
Idioma:
Inglés
Calendario de la edición:
Volume Open
Temas de la revista:
Computer Sciences, other, Mathematics, General Mathematics