Quasi-uniform Space

Roland Coghetto. "Quasi-uniform Space." Formalized Mathematics 24.3 (2016): 205-214. <http://eudml.org/doc/287993>.

@article{RolandCoghetto2016,
abstract = {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.},
author = {Roland Coghetto},
journal = {Formalized Mathematics},
keywords = {quasi-uniform space; quasi-uniformity; Pervin space; Csaszar-Pervin quasi-uniformity},
language = {eng},
number = {3},
pages = {205-214},
title = {Quasi-uniform Space},
url = {http://eudml.org/doc/287993},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Roland Coghetto
TI - Quasi-uniform Space
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 3
SP - 205
EP - 214
AB - 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.
LA - eng
KW - quasi-uniform space; quasi-uniformity; Pervin space; Csaszar-Pervin quasi-uniformity
UR - http://eudml.org/doc/287993
ER -