Quasi-uniform Space

• Autorzy: Roland Coghetto
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

quasi-uniform space; quasi-uniformity; Pervin space; Csaszar-Pervin quasi-uniformity

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 3
• Strony: 205-214

Daty

wydano

2016-09-01

otrzymano

2016-06-30

online

2017-02-08

Twórcy

autor

Roland Coghetto

• Rue de la Brasserie 5 7100 La Louvière,

Identyfikatory

DOI

10.1515/forma-2016-0017