Uniform Space

Roland Coghetto. "Uniform Space." Formalized Mathematics 24.3 (2016): 215-226. <http://eudml.org/doc/288011>.

@article{RolandCoghetto2016,
abstract = {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.},
author = {Roland Coghetto},
journal = {Formalized Mathematics},
keywords = {uniform space; uniformity; pseudo-metric space; topological group; partition topology; Pervin uniform space; pervin uniform space},
language = {eng},
number = {3},
pages = {215-226},
title = {Uniform Space},
url = {http://eudml.org/doc/288011},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Roland Coghetto
TI - Uniform Space
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 3
SP - 215
EP - 226
AB - 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.
LA - eng
KW - uniform space; uniformity; pseudo-metric space; topological group; partition topology; Pervin uniform space; pervin uniform space
UR - http://eudml.org/doc/288011
ER -