Quasi-uniform Space

In this article, using mostly Pervin [9], Kunzi [6], [8], [7], Williams [11] and Bourbaki [3] works, we formalize in Mizar [2] the notions of quasi-uniform space, semi-uniform space and locally uniform space. We define the topology induced by a quasi-uniform space. Finally we formalize from the sets of the form ((X backslash Omega) x X) boolean OR (X x Omega), the Csaszar-Pervin quasi-uniform space induced by a topological space.