Compactness of Neural Networks

In this article, Feed-forward Neural Network is formalized in the Mizar system [1], [2]. First, the multilayer perceptron [6], [7], [8] is formalized using functional sequences. Next, we show that a set of functions generated by these neural networks satisfies equicontinuousness and equiboundedness property [10], [5]. At last, we formalized the compactness of the function set of these neural networks by using the Ascoli-Arzela’s theorem according to [4] and [3].