In this article, we formalize in Mizar [1] the notion of uniform space introduced by André Weil using the concepts of entourages [2]. We present some results between uniform space and pseudo metric space. We introduce the concepts of left-uniformity and right-uniformity of a topological group. Next, we define the concept of the partition topology. Following the Vlach’s works [11, 10], we define the semi-uniform space induced by a tolerance and the uniform space induced by an equivalence relation. Finally, using mostly Gehrke, Grigorieff and Pin [4] works, a Pervin uniform space defined from the sets of the form ((X) × (X)) ∪ (A×A) is presented.
@article{bwmeta1.element.doi-10_1515_forma-2016-0018,
author = {Roland Coghetto},
title = {Uniform Space},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {215-226},
zbl = {1357.54025},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0018}
}
Roland Coghetto. Uniform Space. Formalized Mathematics, Tome 24 (2016) pp. 215-226. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0018/