Ascoli-Arzelà Theorem (Metric Space Version)

We formulate and prove in Mizar the Ascoli-Arzelà’s theorem, which gives necessary and sufficient conditions for a collection of continuous functions to be compact. We use the metric space setting, and the notions of equicontinuousness and equiboundedness of a set of continuous functions are utilized.