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 quasiuniform 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 Ω) × X) ∪ (X × Ω), the Csaszar-Pervin quasi-uniform space induced by a topological space.
@article{bwmeta1.element.doi-10_1515_forma-2016-0017,
author = {Roland Coghetto},
title = {Quasi-uniform Space},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {205-214},
zbl = {1357.54024},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0017}
}
Roland Coghetto. Quasi-uniform Space. Formalized Mathematics, Tome 24 (2016) pp. 205-214. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0017/