:: Quasi-uniform Space
:: by Roland Coghetto
::
:: Received June 30, 2016
:: Copyright (c) 2016-2021 Association of Mizar Users


theorem Th2: :: UNIFORM2:1
for X being set
for A being Subset of X holds [:(X \ A),X:] \/ [:X,A:] c= [:X,X:]
proof end;

theorem :: UNIFORM2:2
for X being set
for A being Subset of X holds [:(X \ A),X:] \/ [:X,A:] = [:A,A:] \/ [:(X \ A),X:]
proof end;

theorem Th3: :: UNIFORM2:3
for X being set
for R, S being Relation of X holds R * S = { [x,y] where x, y is Element of X : ex z being Element of X st
( [x,z] in R & [z,y] in S ) }
proof end;

registration
let X be set ;
let cB be Subset-Family of X;
cluster <.cB.] -> non empty ;
coherence
not <.cB.] is empty
proof end;
end;

registration
let X be set ;
let cB be Subset-Family of [:X,X:];
cluster -> Relation-like for Element of cB;
coherence
for b1 being Element of cB holds b1 is Relation-like
proof end;
end;

notation
let X be set ;
let cB be Subset-Family of [:X,X:];
let B be Element of cB;
synonym B [~] for X ~ ;
end;

definition
let X be set ;
let cB be Subset-Family of [:X,X:];
let B be Element of cB;
:: original: [~]
redefine func B [~] -> Subset of [:X,X:];
coherence
[~] is Subset of [:X,X:]
proof end;
end;

notation
let X be set ;
let cB be Subset-Family of [:X,X:];
let B1, B2 be Element of cB;
synonym B1 [*] B2 for X * cB;
end;

definition
let X be set ;
let cB be Subset-Family of [:X,X:];
let B1, B2 be Element of cB;
:: original: [*]
redefine func B1 [*] B2 -> Subset of [:X,X:];
coherence
[*] is Subset of [:X,X:]
proof end;
end;

theorem :: UNIFORM2:4
for X being set
for G being Subset-Family of X st G is upper holds
FinMeetCl G is upper
proof end;

theorem Th4: :: UNIFORM2:5
for X being set
for R being Relation of X st R is_symmetric_in X holds
R ~ is_symmetric_in X
proof end;

definition
attr c1 is strict ;
struct UniformSpaceStr -> 1-sorted ;
aggr UniformSpaceStr(# carrier, entourages #) -> UniformSpaceStr ;
sel entourages c1 -> Subset-Family of [: the carrier of c1, the carrier of c1:];
end;

definition
let U be UniformSpaceStr ;
attr U is void means :: UNIFORM2:def 1
 the entourages of U is empty ;
end;

:: deftheorem defines void UNIFORM2:def 1 :
for U being UniformSpaceStr holds
( U is void iff the entourages of U is empty );

definition
let X be set ;
func Uniform_Space X -> strict UniformSpaceStr equals :: UNIFORM2:def 2
 UniformSpaceStr(# X,({} (bool [:X,X:])) #);
coherence
UniformSpaceStr(# X,({} (bool [:X,X:])) #) is strict UniformSpaceStr ;
end;

:: deftheorem defines Uniform_Space UNIFORM2:def 2 :
for X being set holds Uniform_Space X = UniformSpaceStr(# X,({} (bool [:X,X:])) #);

definition
func TrivialUniformSpace -> strict UniformSpaceStr equals :: UNIFORM2:def 3
 UniformSpaceStr(# {},(cobool [:{},{}:]) #);
coherence
UniformSpaceStr(# {},(cobool [:{},{}:]) #) is strict UniformSpaceStr ;
func NonEmptyTrivialUniformSpace -> strict UniformSpaceStr means :D1: :: UNIFORM2:def 4
 ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & it = UniformSpaceStr(# {{}},SF #) );
existence
ex b1 being strict UniformSpaceStr ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & b1 = UniformSpaceStr(# {{}},SF #) )
proof end;
uniqueness
for b1, b2 being strict UniformSpaceStr st ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & b1 = UniformSpaceStr(# {{}},SF #) ) & ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & b2 = UniformSpaceStr(# {{}},SF #) ) holds
b1 = b2 ;
end;

:: deftheorem defines TrivialUniformSpace UNIFORM2:def 3 :
TrivialUniformSpace = UniformSpaceStr(# {},(cobool [:{},{}:]) #);

:: deftheorem D1 defines NonEmptyTrivialUniformSpace UNIFORM2:def 4 :
for b1 being strict UniformSpaceStr holds
( b1 = NonEmptyTrivialUniformSpace iff ex SF being Subset-Family of [:{{}},{{}}:] st
( SF = {[:{{}},{{}}:]} & b1 = UniformSpaceStr(# {{}},SF #) ) );

registration
let X be empty set ;
cluster Uniform_Space X -> empty strict ;
coherence
Uniform_Space X is empty ;
end;

registration
let X be non empty set ;
cluster Uniform_Space X -> non empty strict ;
coherence
not Uniform_Space X is empty ;
end;

registration
let X be set ;
cluster Uniform_Space X -> strict void ;
coherence
Uniform_Space X is void ;
end;

registration
cluster TrivialUniformSpace -> empty strict non void ;
coherence
( TrivialUniformSpace is empty & not TrivialUniformSpace is void ) ;
cluster NonEmptyTrivialUniformSpace -> non empty strict non void ;
coherence
( not NonEmptyTrivialUniformSpace is empty & not NonEmptyTrivialUniformSpace is void )
proof end;
end;

registration
cluster empty strict void for UniformSpaceStr ;
existence
ex b1 being UniformSpaceStr st
( b1 is empty & b1 is strict & b1 is void )
proof end;
cluster empty strict non void for UniformSpaceStr ;
existence
ex b1 being UniformSpaceStr st
( b1 is empty & b1 is strict & not b1 is void )
proof end;
cluster non empty strict void for UniformSpaceStr ;
existence
ex b1 being UniformSpaceStr st
( not b1 is empty & b1 is strict & b1 is void )
proof end;
cluster non empty strict non void for UniformSpaceStr ;
existence
ex b1 being UniformSpaceStr st
( not b1 is empty & b1 is strict & not b1 is void )
proof end;
end;

definition
let X be set ;
let SF be Subset-Family of [:X,X:];
func SF [~] -> Subset-Family of [:X,X:] equals :: UNIFORM2:def 5
 { (S [~]) where S is Element of SF : verum } ;
coherence
{ (S [~]) where S is Element of SF : verum } is Subset-Family of [:X,X:]
proof end;
end;

:: deftheorem defines [~] UNIFORM2:def 5 :
for X being set
for SF being Subset-Family of [:X,X:] holds SF [~] = { (S [~]) where S is Element of SF : verum } ;

definition
let US be UniformSpaceStr ;
func US [~] -> UniformSpaceStr equals :: UNIFORM2:def 6
 UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #);
coherence
UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #) is UniformSpaceStr ;
end;

:: deftheorem defines [~] UNIFORM2:def 6 :
for US being UniformSpaceStr holds US [~] = UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #);

registration
let USS be non empty UniformSpaceStr ;
cluster USS [~] -> non empty ;
coherence
not USS [~] is empty ;
end;

definition
let US be UniformSpaceStr ;
attr US is upper means :: UNIFORM2:def 7
 the entourages of US is upper ;
attr US is cap-closed means :: UNIFORM2:def 8
 the entourages of US is cap-closed ;
attr US is axiom_U1 means :: UNIFORM2:def 9
 for S being Element of the entourages of US holds id the carrier of US c= S;
attr US is axiom_U2 means :: UNIFORM2:def 10
 for S being Element of the entourages of US holds S [~] in the entourages of US;
attr US is axiom_U3 means :: UNIFORM2:def 11
 for S being Element of the entourages of US ex W being Element of the entourages of US st W [*] W c= S;
end;

:: deftheorem defines upper UNIFORM2:def 7 :
for US being UniformSpaceStr holds
( US is upper iff the entourages of US is upper );

:: deftheorem defines cap-closed UNIFORM2:def 8 :
for US being UniformSpaceStr holds
( US is cap-closed iff the entourages of US is cap-closed );

:: deftheorem defines axiom_U1 UNIFORM2:def 9 :
for US being UniformSpaceStr holds
( US is axiom_U1 iff for S being Element of the entourages of US holds id the carrier of US c= S );

:: deftheorem defines axiom_U2 UNIFORM2:def 10 :
for US being UniformSpaceStr holds
( US is axiom_U2 iff for S being Element of the entourages of US holds S [~] in the entourages of US );

:: deftheorem defines axiom_U3 UNIFORM2:def 11 :
for US being UniformSpaceStr holds
( US is axiom_U3 iff for S being Element of the entourages of US ex W being Element of the entourages of US st W [*] W c= S );

theorem Th7: :: UNIFORM2:6
for US being non void UniformSpaceStr holds
( US is axiom_U1 iff for S being Element of the entourages of US ex R being Relation of the carrier of US st
( R = S & R is_reflexive_in the carrier of US ) )
proof end;

theorem Th8: :: UNIFORM2:7
for US being non void UniformSpaceStr holds
( US is axiom_U1 iff for S being Element of the entourages of US ex R being total reflexive Relation of the carrier of US st R = S )
proof end;

registration
cluster void -> non axiom_U2 for UniformSpaceStr ;
coherence
for b1 being UniformSpaceStr st b1 is void holds
not b1 is axiom_U2 ;
end;

theorem :: UNIFORM2:8
for US being UniformSpaceStr st US is axiom_U2 holds
for S being Element of the entourages of US
for x, y being Element of US st [x,y] in S holds
[y,x] in union the entourages of US
proof end;

theorem Th9: :: UNIFORM2:9
for US being non void UniformSpaceStr st ( for S being Element of the entourages of US ex R being Relation of the carrier of US st
( S = R & R is_symmetric_in the carrier of US ) ) holds
US is axiom_U2
proof end;

theorem Th10: :: UNIFORM2:10
for US being non void UniformSpaceStr st ( for S being Element of the entourages of US ex R being Relation of the carrier of US st
( S = R & R is symmetric ) ) holds
US is axiom_U2
proof end;

theorem :: UNIFORM2:11
for US being non void UniformSpaceStr st ( for S being Element of the entourages of US ex R being Tolerance of the carrier of US st S = R ) holds
( US is axiom_U1 & US is axiom_U2 )
proof end;

registration
let X be empty set ;
cluster Uniform_Space X -> strict upper cap-closed axiom_U1 non axiom_U2 axiom_U3 ;
coherence
( Uniform_Space X is upper & Uniform_Space X is cap-closed & Uniform_Space X is axiom_U1 & not Uniform_Space X is axiom_U2 & Uniform_Space X is axiom_U3 )
proof end;
end;

registration
cluster Uniform_Space {{}} -> strict upper cap-closed non axiom_U2 ;
coherence
( Uniform_Space {{}} is upper & Uniform_Space {{}} is cap-closed & not Uniform_Space {{}} is axiom_U2 )
proof end;
cluster TrivialUniformSpace -> strict upper cap-closed axiom_U1 axiom_U2 axiom_U3 ;
coherence
( TrivialUniformSpace is upper & TrivialUniformSpace is cap-closed & TrivialUniformSpace is axiom_U1 & TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 )
proof end;
cluster NonEmptyTrivialUniformSpace -> strict upper cap-closed axiom_U1 axiom_U2 axiom_U3 ;
coherence
( NonEmptyTrivialUniformSpace is upper & NonEmptyTrivialUniformSpace is cap-closed & NonEmptyTrivialUniformSpace is axiom_U1 & NonEmptyTrivialUniformSpace is axiom_U2 & NonEmptyTrivialUniformSpace is axiom_U3 )
proof end;
end;

registration
cluster empty strict non void upper cap-closed axiom_U1 axiom_U2 axiom_U3 for UniformSpaceStr ;
existence
ex b1 being UniformSpaceStr st
( b1 is strict & b1 is empty & not b1 is void & b1 is upper & b1 is cap-closed & b1 is axiom_U1 & b1 is axiom_U2 & b1 is axiom_U3 )
proof end;
end;

registration
cluster empty strict -> strict axiom_U1 for UniformSpaceStr ;
coherence
for b1 being strict UniformSpaceStr st b1 is empty holds
b1 is axiom_U1
proof end;
end;

registration
cluster non empty strict non void upper cap-closed axiom_U1 axiom_U2 axiom_U3 for UniformSpaceStr ;
existence
ex b1 being UniformSpaceStr st
( b1 is strict & not b1 is empty & not b1 is void & b1 is upper & b1 is cap-closed & b1 is axiom_U1 & b1 is axiom_U2 & b1 is axiom_U3 )
proof end;
end;

definition
let SUS be non empty axiom_U1 UniformSpaceStr ;
let x be Element of SUS;
let V be Element of the entourages of SUS;
func Neighborhood (V,x) -> non empty Subset of SUS equals :: UNIFORM2:def 12
 { y where y is Element of SUS : [x,y] in V } ;
coherence
{ y where y is Element of SUS : [x,y] in V } is non empty Subset of SUS
proof end;
end;

:: deftheorem defines Neighborhood UNIFORM2:def 12 :
for SUS being non empty axiom_U1 UniformSpaceStr
for x being Element of SUS
for V being Element of the entourages of SUS holds Neighborhood (V,x) = { y where y is Element of SUS : [x,y] in V } ;

theorem :: UNIFORM2:12
for USS being non empty axiom_U1 UniformSpaceStr
for x being Element of the carrier of USS
for V being Element of the entourages of USS holds x in Neighborhood (V,x)
proof end;

definition
let USS be cap-closed UniformSpaceStr ;
let V1, V2 be Element of the entourages of USS;
:: original: /\
redefine func V1 /\ V2 -> Element of the entourages of USS;
coherence
V1 /\ V2 is Element of the entourages of USS
proof end;
end;

theorem Th11: :: UNIFORM2:13
for USS being non empty cap-closed axiom_U1 UniformSpaceStr
for x being Element of USS
for V, W being Element of the entourages of USS holds (Neighborhood (V,x)) /\ (Neighborhood (W,x)) = Neighborhood ((V /\ W),x)
proof end;

registration
let USS be non empty axiom_U1 UniformSpaceStr ;
cluster the entourages of USS -> with_non-empty_elements ;
coherence
the entourages of USS is with_non-empty_elements
proof end;
end;

registration
let USS be non empty axiom_U1 UniformSpaceStr ;
cluster the entourages of USS -> non empty ;
coherence
not the entourages of USS is empty
proof end;
end;

definition
let USS be non empty axiom_U1 UniformSpaceStr ;
let x be Point of USS;
func Neighborhood x -> Subset-Family of USS equals :: UNIFORM2:def 13
 { (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } ;
coherence
{ (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } is Subset-Family of USS
proof end;
end;

:: deftheorem defines Neighborhood UNIFORM2:def 13 :
for USS being non empty axiom_U1 UniformSpaceStr
for x being Point of USS holds Neighborhood x = { (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } ;

registration
let USS be non empty axiom_U1 UniformSpaceStr ;
let x be Point of USS;
cluster Neighborhood x -> non empty ;
coherence
not Neighborhood x is empty
proof end;
end;

theorem :: UNIFORM2:14
for SUS being non empty axiom_U1 UniformSpaceStr
for x being Element of the carrier of SUS
for V being Element of the entourages of SUS holds
( Neighborhood (V,x) = V .: {x} & Neighborhood (V,x) = rng (V | {x}) & Neighborhood (V,x) = Im (V,x) & Neighborhood (V,x) = Class (V,x) & Neighborhood (V,x) = neighbourhood (,) )
proof end;

definition
let USS be non empty axiom_U1 UniformSpaceStr ;
func Neighborhood USS -> Function of the carrier of USS,(bool (bool the carrier of USS)) means :Def5: :: UNIFORM2:def 14
 for x being Element of USS holds it . x = Neighborhood x;
existence
ex b1 being Function of the carrier of USS,(bool (bool the carrier of USS)) st
for x being Element of USS holds b1 . x = Neighborhood x
proof end;
uniqueness
for b1, b2 being Function of the carrier of USS,(bool (bool the carrier of USS)) st ( for x being Element of USS holds b1 . x = Neighborhood x ) & ( for x being Element of USS holds b2 . x = Neighborhood x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Neighborhood UNIFORM2:def 14 :
for USS being non empty axiom_U1 UniformSpaceStr
for b2 being Function of the carrier of USS,(bool (bool the carrier of USS)) holds
( b2 = Neighborhood USS iff for x being Element of USS holds b2 . x = Neighborhood x );

definition
let USS be non empty axiom_U1 UniformSpaceStr ;
attr USS is topological means :: UNIFORM2:def 15
 FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace;
end;

:: deftheorem defines topological UNIFORM2:def 15 :
for USS being non empty axiom_U1 UniformSpaceStr holds
( USS is topological iff FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace );

definition
mode Quasi-UniformSpace is upper cap-closed axiom_U1 axiom_U3 UniformSpaceStr ;
end;

theorem :: UNIFORM2:15
for QUS being Quasi-UniformSpace st the entourages of QUS is empty holds
the entourages of (QUS [~]) = {{}}
proof end;

theorem :: UNIFORM2:16
for QUS being Quasi-UniformSpace st the entourages of (QUS [~]) = {{}} & the entourages of (QUS [~]) is upper holds
the carrier of QUS is empty
proof end;

registration
let QUS be non void Quasi-UniformSpace;
cluster QUS [~] -> upper cap-closed axiom_U1 axiom_U3 ;
coherence
( QUS [~] is upper & QUS [~] is cap-closed & QUS [~] is axiom_U1 & QUS [~] is axiom_U3 )
proof end;
end;

definition
let X be set ;
let cB be Subset-Family of [:X,X:];
attr cB is axiom_UP1 means :: UNIFORM2:def 16
 for B being Element of cB holds id X c= B;
attr cB is axiom_UP3 means :: UNIFORM2:def 17
 for B1 being Element of cB ex B2 being Element of cB st B2 [*] B2 c= B1;
end;

:: deftheorem defines axiom_UP1 UNIFORM2:def 16 :
for X being set
for cB being Subset-Family of [:X,X:] holds
( cB is axiom_UP1 iff for B being Element of cB holds id X c= B );

:: deftheorem defines axiom_UP3 UNIFORM2:def 17 :
for X being set
for cB being Subset-Family of [:X,X:] holds
( cB is axiom_UP3 iff for B1 being Element of cB ex B2 being Element of cB st B2 [*] B2 c= B1 );

theorem :: UNIFORM2:17
for X being non empty set
for cB being empty Subset-Family of [:X,X:] holds not cB is axiom_UP1
proof end;

theorem Th11bis: :: UNIFORM2:18
for X being set
for cB being Subset-Family of [:X,X:] st cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP3 holds
UniformSpaceStr(# X,<.cB.] #) is Quasi-UniformSpace
proof end;

definition
mode Semi-UniformSpace is upper cap-closed axiom_U1 axiom_U2 UniformSpaceStr ;
end;

registration
cluster upper cap-closed axiom_U1 axiom_U2 -> non void for UniformSpaceStr ;
coherence
for b1 being Semi-UniformSpace holds not b1 is void ;
end;

theorem Th12: :: UNIFORM2:19
for SUS being Semi-UniformSpace st SUS is empty holds
{} in the entourages of SUS
proof end;

registration
let SUS be empty Semi-UniformSpace;
cluster the entourages of SUS -> with_empty_element ;
coherence
not the entourages of SUS is with_non-empty_elements by Th12, SETFAM_1:def 8;
end;

definition
let SUS be non empty Semi-UniformSpace;
attr SUS is axiom_UL means :: UNIFORM2:def 18
 for S being Element of the entourages of SUS
for x being Element of SUS ex W being Element of the entourages of SUS st { y where y is Element of SUS : [x,y] in W [*] W } c= Neighborhood (S,x);
end;

:: deftheorem defines axiom_UL UNIFORM2:def 18 :
for SUS being non empty Semi-UniformSpace holds
( SUS is axiom_UL iff for S being Element of the entourages of SUS
for x being Element of SUS ex W being Element of the entourages of SUS st { y where y is Element of SUS : [x,y] in W [*] W } c= Neighborhood (S,x) );

registration
cluster non empty upper cap-closed axiom_U1 axiom_U2 axiom_U3 -> non empty axiom_UL for UniformSpaceStr ;
coherence
for b1 being non empty Semi-UniformSpace st b1 is axiom_U3 holds
b1 is axiom_UL
proof end;
end;

registration
cluster non empty non void upper cap-closed axiom_U1 axiom_U2 axiom_UL for UniformSpaceStr ;
existence
ex b1 being non empty Semi-UniformSpace st b1 is axiom_UL
proof end;
end;

definition
mode Locally-UniformSpace is non empty axiom_UL Semi-UniformSpace;
end;

theorem Th15: :: UNIFORM2:20
for USS being non empty upper axiom_U1 UniformSpaceStr
for x being Element of the carrier of USS holds Neighborhood x is upper
proof end;

theorem Th16: :: UNIFORM2:21
for US being non empty axiom_U1 UniformSpaceStr
for x being Element of US
for V being Element of the entourages of US holds x in Neighborhood (V,x)
proof end;

theorem Th17: :: UNIFORM2:22
for US being non empty cap-closed axiom_U1 UniformSpaceStr
for x being Element of US holds Neighborhood x is cap-closed
proof end;

theorem Th18: :: UNIFORM2:23
for US being non empty upper cap-closed axiom_U1 UniformSpaceStr
for x being Element of US holds Neighborhood x is Filter of the carrier of US
proof end;

registration
cluster non empty upper cap-closed axiom_U1 axiom_U2 axiom_UL -> topological for UniformSpaceStr ;
coherence
for b1 being Locally-UniformSpace holds b1 is topological
proof end;
end;

definition
let USS be non empty axiom_U1 topological UniformSpaceStr ;
func FMT_induced_by USS -> FMT_TopSpace equals :: UNIFORM2:def 19
 FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #);
coherence
FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace
proof end;
end;

:: deftheorem defines FMT_induced_by UNIFORM2:def 19 :
for USS being non empty axiom_U1 topological UniformSpaceStr holds FMT_induced_by USS = FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #);

definition
let USS be non empty axiom_U1 topological UniformSpaceStr ;
func TopSpace_induced_by USS -> TopSpace equals :: UNIFORM2:def 20
 FMT2TopSpace (FMT_induced_by USS);
coherence
FMT2TopSpace (FMT_induced_by USS) is TopSpace ;
end;

:: deftheorem defines TopSpace_induced_by UNIFORM2:def 20 :
for USS being non empty axiom_U1 topological UniformSpaceStr holds TopSpace_induced_by USS = FMT2TopSpace (FMT_induced_by USS);

definition
let X be set ;
let A be Subset of X;
func block_Pervin_quasi_uniformity A -> Subset of [:X,X:] equals :: UNIFORM2:def 21
[:(X \ A),X:] \/ [:X,A:];
coherence
[:(X \ A),X:] \/ [:X,A:] is Subset of [:X,X:]
proof end;
end;

:: deftheorem defines block_Pervin_quasi_uniformity UNIFORM2:def 21 :
for X being set
for A being Subset of X holds block_Pervin_quasi_uniformity A = [:(X \ A),X:] \/ [:X,A:];

theorem Th20: :: UNIFORM2:24
for X being set
for A being Subset of X holds
( id X c= block_Pervin_quasi_uniformity A & (block_Pervin_quasi_uniformity A) * (block_Pervin_quasi_uniformity A) c= block_Pervin_quasi_uniformity A )
proof end;

definition
let T be TopSpace;
func subbasis_Pervin_quasi_uniformity T -> Subset-Family of [: the carrier of T, the carrier of T:] equals :: UNIFORM2:def 22
 { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } ;
coherence
{ (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } is Subset-Family of [: the carrier of T, the carrier of T:]
proof end;
end;

:: deftheorem defines subbasis_Pervin_quasi_uniformity UNIFORM2:def 22 :
for T being TopSpace holds subbasis_Pervin_quasi_uniformity T = { (block_Pervin_quasi_uniformity O) where O is Element of the topology of T : verum } ;

registration
let T be non empty TopSpace;
cluster subbasis_Pervin_quasi_uniformity T -> non empty ;
coherence
not subbasis_Pervin_quasi_uniformity T is empty
proof end;
end;

definition
let T be TopSpace;
func basis_Pervin_quasi_uniformity T -> Subset-Family of [: the carrier of T, the carrier of T:] equals :: UNIFORM2:def 23
 FinMeetCl (subbasis_Pervin_quasi_uniformity T);
coherence
FinMeetCl (subbasis_Pervin_quasi_uniformity T) is Subset-Family of [: the carrier of T, the carrier of T:] ;
end;

:: deftheorem defines basis_Pervin_quasi_uniformity UNIFORM2:def 23 :
for T being TopSpace holds basis_Pervin_quasi_uniformity T = FinMeetCl (subbasis_Pervin_quasi_uniformity T);

registration
let X be set ;
cluster non empty cap-closed -> non empty quasi_basis for Element of bool (bool [:X,X:]);
coherence
for b1 being non empty Subset-Family of [:X,X:] st b1 is cap-closed holds
b1 is quasi_basis
proof end;
end;

registration
let T be TopSpace;
cluster basis_Pervin_quasi_uniformity T -> cap-closed ;
coherence
basis_Pervin_quasi_uniformity T is cap-closed
proof end;
end;

registration
let T be TopSpace;
cluster basis_Pervin_quasi_uniformity T -> quasi_basis ;
coherence
basis_Pervin_quasi_uniformity T is quasi_basis ;
end;

registration
let T be TopSpace;
cluster basis_Pervin_quasi_uniformity T -> axiom_UP1 ;
coherence
basis_Pervin_quasi_uniformity T is axiom_UP1
proof end;
end;

registration
let T be TopSpace;
cluster basis_Pervin_quasi_uniformity T -> axiom_UP3 ;
coherence
basis_Pervin_quasi_uniformity T is axiom_UP3
proof end;
end;

definition
let T be TopSpace;
func Pervin_quasi_uniformity T -> strict Quasi-UniformSpace equals :: UNIFORM2:def 24
 UniformSpaceStr(# the carrier of T,<.(basis_Pervin_quasi_uniformity T).] #);
coherence
UniformSpaceStr(# the carrier of T,<.(basis_Pervin_quasi_uniformity T).] #) is strict Quasi-UniformSpace by Th11bis;
end;

:: deftheorem defines Pervin_quasi_uniformity UNIFORM2:def 24 :
for T being TopSpace holds Pervin_quasi_uniformity T = UniformSpaceStr(# the carrier of T,<.(basis_Pervin_quasi_uniformity T).] #);

theorem :: UNIFORM2:25
for T being non empty TopSpace
for V being Element of the entourages of (Pervin_quasi_uniformity T) ex b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) st b c= V
proof end;

theorem :: UNIFORM2:26
for T being non empty TopSpace
for V being Subset of [: the carrier of T, the carrier of T:] st ex b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) st b c= V holds
V is Element of the entourages of (Pervin_quasi_uniformity T)
proof end;

theorem :: UNIFORM2:27
for T being TopSpace holds subbasis_Pervin_quasi_uniformity T c= the entourages of (Pervin_quasi_uniformity T)
proof end;

theorem Th27: :: UNIFORM2:28
for QU being non void Quasi-UniformSpace holds [: the carrier of QU, the carrier of QU:] in the entourages of QU
proof end;

theorem :: UNIFORM2:29
for T being TopSpace
for QU being non void Quasi-UniformSpace st the carrier of T = the carrier of QU & subbasis_Pervin_quasi_uniformity T c= the entourages of QU holds
the entourages of (Pervin_quasi_uniformity T) c= the entourages of QU
proof end;

registration
let T be non empty TopSpace;
cluster Pervin_quasi_uniformity T -> non empty strict ;
coherence
not Pervin_quasi_uniformity T is empty ;
end;

registration
let T be non empty TopSpace;
cluster Pervin_quasi_uniformity T -> strict topological ;
coherence
Pervin_quasi_uniformity T is topological
proof end;
end;

theorem Th29: :: UNIFORM2:30
for T being non empty TopSpace
for x being Element of subbasis_Pervin_quasi_uniformity T
for y being Element of (Pervin_quasi_uniformity T) holds { z where z is Element of (Pervin_quasi_uniformity T) : [y,z] in x } in the topology of T
proof end;

theorem Th30: :: UNIFORM2:31
for T being non empty TopSpace
for x being Element of the carrier of (Pervin_quasi_uniformity T)
for b being Element of FinMeetCl (subbasis_Pervin_quasi_uniformity T) holds { y where y is Element of T : [x,y] in b } in the topology of T
proof end;

theorem Th31: :: UNIFORM2:32
for UT being non empty strict Quasi-UniformSpace
for FMT being non empty strict FMT_Space_Str
for x being Element of FMT st FMT = FMT_Space_Str(# the carrier of UT,(Neighborhood UT) #) holds
ex y being Element of UT st
( x = y & U_FMT x = Neighborhood y )
proof end;

theorem Th32: :: UNIFORM2:33
for T being non empty TopSpace holds Family_open_set (FMT_induced_by (Pervin_quasi_uniformity T)) = the topology of T
proof end;

theorem :: UNIFORM2:34
for T being non empty strict TopSpace holds TopSpace_induced_by (Pervin_quasi_uniformity T) = T
proof end;