<abstract xmlns="http://www.w3.org/1999/xhtml"><p> 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.</p><p>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.</p></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.

Quasi-uniform Space

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

{"article-title":"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 quasiuniform...

Quasi-uniform Space

Pubblicato online: 21 feb 2017

Pagine: 205 - 214

Ricevuto: 30 giu 2016

DOI: https://doi.org/10.1515/forma-2016-0017

Parole chiave
quasi-uniform space, quasi-uniformity, Pervin space, Csaszar-Pervin quasi-uniformity

© by Roland Coghetto

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Quasi-uniform Space

Pubblicato online: 21 feb 2017

Pagine: 205 - 214

Ricevuto: 30 giu 2016

DOI: https://doi.org/10.1515/forma-2016-0017

Parole chiavequasi-uniform space, quasi-uniformity, Pervin space, Csaszar-Pervin quasi-uniformity

© by Roland Coghetto

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Parole chiave
quasi-uniform space, quasi-uniformity, Pervin space, Csaszar-Pervin quasi-uniformity