:: by Roland Coghetto

::

:: Received June 30, 2016

:: Copyright (c) 2016-2021 Association of Mizar Users

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 ) }

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
end;

registration

let X be set ;

let cB be Subset-Family of [:X,X:];

coherence

for b_{1} being Element of cB holds b_{1} is Relation-like

end;
let cB be Subset-Family of [:X,X:];

coherence

for b

proof end;

notation
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:]

end;
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;

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;
let cB be Subset-Family of [:X,X:];

let B1, B2 be Element of cB;

synonym B1 [*] B2 for X * cB;

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:]

end;
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;

definition

attr c_{1} is strict ;

struct UniformSpaceStr -> 1-sorted ;

aggr UniformSpaceStr(# carrier, entourages #) -> UniformSpaceStr ;

sel entourages c_{1} -> Subset-Family of [: the carrier of c_{1}, the carrier of c_{1}:];

end;
struct UniformSpaceStr -> 1-sorted ;

aggr UniformSpaceStr(# carrier, entourages #) -> UniformSpaceStr ;

sel entourages c

definition
end;

:: deftheorem defines void UNIFORM2:def 1 :

for U being UniformSpaceStr holds

( U is void iff the entourages of U is empty );

for U being UniformSpaceStr holds

( U is void iff the entourages of U is empty );

definition

let X be set ;

UniformSpaceStr(# X,({} (bool [:X,X:])) #) is strict UniformSpaceStr ;

end;
func Uniform_Space X -> strict UniformSpaceStr equals :: UNIFORM2:def 2

UniformSpaceStr(# X,({} (bool [:X,X:])) #);

coherence UniformSpaceStr(# X,({} (bool [:X,X:])) #);

UniformSpaceStr(# X,({} (bool [:X,X:])) #) is strict UniformSpaceStr ;

:: deftheorem defines Uniform_Space UNIFORM2:def 2 :

for X being set holds Uniform_Space X = UniformSpaceStr(# X,({} (bool [:X,X:])) #);

for X being set holds Uniform_Space X = UniformSpaceStr(# X,({} (bool [:X,X:])) #);

definition

UniformSpaceStr(# {},(cobool [:{},{}:]) #) is strict UniformSpaceStr ;

ex b_{1} being strict UniformSpaceStr ex SF being Subset-Family of [:{{}},{{}}:] st

( SF = {[:{{}},{{}}:]} & b_{1} = UniformSpaceStr(# {{}},SF #) )

for b_{1}, b_{2} being strict UniformSpaceStr st ex SF being Subset-Family of [:{{}},{{}}:] st

( SF = {[:{{}},{{}}:]} & b_{1} = UniformSpaceStr(# {{}},SF #) ) & ex SF being Subset-Family of [:{{}},{{}}:] st

( SF = {[:{{}},{{}}:]} & b_{2} = UniformSpaceStr(# {{}},SF #) ) holds

b_{1} = b_{2}
;

end;

func TrivialUniformSpace -> strict UniformSpaceStr equals :: UNIFORM2:def 3

UniformSpaceStr(# {},(cobool [:{},{}:]) #);

coherence UniformSpaceStr(# {},(cobool [:{},{}:]) #);

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 SF being Subset-Family of [:{{}},{{}}:] st

( SF = {[:{{}},{{}}:]} & it = UniformSpaceStr(# {{}},SF #) );

ex b

( SF = {[:{{}},{{}}:]} & b

proof end;

uniqueness for b

( SF = {[:{{}},{{}}:]} & b

( SF = {[:{{}},{{}}:]} & b

b

:: deftheorem defines TrivialUniformSpace UNIFORM2:def 3 :

TrivialUniformSpace = UniformSpaceStr(# {},(cobool [:{},{}:]) #);

TrivialUniformSpace = UniformSpaceStr(# {},(cobool [:{},{}:]) #);

:: deftheorem D1 defines NonEmptyTrivialUniformSpace UNIFORM2:def 4 :

for b_{1} being strict UniformSpaceStr holds

( b_{1} = NonEmptyTrivialUniformSpace iff ex SF being Subset-Family of [:{{}},{{}}:] st

( SF = {[:{{}},{{}}:]} & b_{1} = UniformSpaceStr(# {{}},SF #) ) );

for b

( b

( SF = {[:{{}},{{}}:]} & b

registration
end;

registration
end;

registration

coherence

( TrivialUniformSpace is empty & not TrivialUniformSpace is void ) ;

coherence

( not NonEmptyTrivialUniformSpace is empty & not NonEmptyTrivialUniformSpace is void )

end;
( TrivialUniformSpace is empty & not TrivialUniformSpace is void ) ;

coherence

( not NonEmptyTrivialUniformSpace is empty & not NonEmptyTrivialUniformSpace is void )

proof end;

registration

existence

ex b_{1} being UniformSpaceStr st

( b_{1} is empty & b_{1} is strict & b_{1} is void )

ex b_{1} being UniformSpaceStr st

( b_{1} is empty & b_{1} is strict & not b_{1} is void )

ex b_{1} being UniformSpaceStr st

( not b_{1} is empty & b_{1} is strict & b_{1} is void )

ex b_{1} being UniformSpaceStr st

( not b_{1} is empty & b_{1} is strict & not b_{1} is void )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

existence ex b

( not b

proof end;

existence ex b

( not b

proof end;

definition

let X be set ;

let SF be Subset-Family of [:X,X:];

{ (S [~]) where S is Element of SF : verum } is Subset-Family of [:X,X:]

end;
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 } ;

{ (S [~]) where S is Element of SF : verum } is Subset-Family of [:X,X:]

proof 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 } ;

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 ;

UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #) is UniformSpaceStr ;

end;
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 [~]) #);

UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #) is UniformSpaceStr ;

:: deftheorem defines [~] UNIFORM2:def 6 :

for US being UniformSpaceStr holds US [~] = UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #);

for US being UniformSpaceStr holds US [~] = UniformSpaceStr(# the carrier of US,( the entourages of US [~]) #);

definition

let US be UniformSpaceStr ;

end;
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;

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;

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;

for S being Element of the entourages of US ex W being Element of the entourages of US st W [*] W c= S;

:: deftheorem defines upper UNIFORM2:def 7 :

for US being UniformSpaceStr holds

( US is upper iff the entourages of US is upper );

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 );

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 );

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 );

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 );

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 ) )

( 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 )

( 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
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

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

( 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

( 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 )

( US is axiom_U1 & US is axiom_U2 )

proof end;

registration

let X be empty set ;

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 )

end;
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;

registration

coherence

( Uniform_Space {{}} is upper & Uniform_Space {{}} is cap-closed & not Uniform_Space {{}} is axiom_U2 )

( TrivialUniformSpace is upper & TrivialUniformSpace is cap-closed & TrivialUniformSpace is axiom_U1 & TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 )

( NonEmptyTrivialUniformSpace is upper & NonEmptyTrivialUniformSpace is cap-closed & NonEmptyTrivialUniformSpace is axiom_U1 & NonEmptyTrivialUniformSpace is axiom_U2 & NonEmptyTrivialUniformSpace is axiom_U3 )

end;
( Uniform_Space {{}} is upper & Uniform_Space {{}} is cap-closed & not Uniform_Space {{}} is axiom_U2 )

proof end;

coherence ( TrivialUniformSpace is upper & TrivialUniformSpace is cap-closed & TrivialUniformSpace is axiom_U1 & TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 )

proof end;

coherence ( NonEmptyTrivialUniformSpace is upper & NonEmptyTrivialUniformSpace is cap-closed & NonEmptyTrivialUniformSpace is axiom_U1 & NonEmptyTrivialUniformSpace is axiom_U2 & NonEmptyTrivialUniformSpace is axiom_U3 )

proof end;

registration

existence

ex b_{1} being UniformSpaceStr st

( b_{1} is strict & b_{1} is empty & not b_{1} is void & b_{1} is upper & b_{1} is cap-closed & b_{1} is axiom_U1 & b_{1} is axiom_U2 & b_{1} is axiom_U3 )

end;
ex b

( b

proof end;

registration

coherence

for b_{1} being strict UniformSpaceStr st b_{1} is empty holds

b_{1} is axiom_U1

end;
for b

b

proof end;

registration

existence

ex b_{1} being UniformSpaceStr st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void & b_{1} is upper & b_{1} is cap-closed & b_{1} is axiom_U1 & b_{1} is axiom_U2 & b_{1} is axiom_U3 )

end;
ex b

( b

proof 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;

{ y where y is Element of SUS : [x,y] in V } is non empty Subset of SUS

end;
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 } ;

{ y where y is Element of SUS : [x,y] in V } is non empty Subset of SUS

proof 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 } ;

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)

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

end;
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;

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)

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 ;

coherence

the entourages of USS is with_non-empty_elements

end;
coherence

the entourages of USS is with_non-empty_elements

proof end;

registration

let USS be non empty axiom_U1 UniformSpaceStr ;

coherence

not the entourages of USS is empty

end;
coherence

not the entourages of USS is empty

proof end;

definition

let USS be non empty axiom_U1 UniformSpaceStr ;

let x be Point of USS;

{ (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } is Subset-Family of USS

end;
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 } ;

{ (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } is Subset-Family of USS

proof 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 } ;

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;

coherence

not Neighborhood x is empty

end;
let x be Point of USS;

coherence

not Neighborhood x is empty

proof 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 (,) )

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 ;

ex b_{1} being Function of the carrier of USS,(bool (bool the carrier of USS)) st

for x being Element of USS holds b_{1} . x = Neighborhood x

for b_{1}, b_{2} being Function of the carrier of USS,(bool (bool the carrier of USS)) st ( for x being Element of USS holds b_{1} . x = Neighborhood x ) & ( for x being Element of USS holds b_{2} . x = Neighborhood x ) holds

b_{1} = b_{2}

end;
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 for x being Element of USS holds it . x = Neighborhood x;

ex b

for x being Element of USS holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines Neighborhood UNIFORM2:def 14 :

for USS being non empty axiom_U1 UniformSpaceStr

for b_{2} being Function of the carrier of USS,(bool (bool the carrier of USS)) holds

( b_{2} = Neighborhood USS iff for x being Element of USS holds b_{2} . x = Neighborhood x );

for USS being non empty axiom_U1 UniformSpaceStr

for b

( b

definition

let USS be non empty axiom_U1 UniformSpaceStr ;

end;
attr USS is topological means :: UNIFORM2:def 15

FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace;

FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace;

:: 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 );

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 );

theorem :: UNIFORM2:15

for QUS being Quasi-UniformSpace st the entourages of QUS is empty holds

the entourages of (QUS [~]) = {{}}

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

the carrier of QUS is empty

proof end;

registration

let QUS be non void Quasi-UniformSpace;

coherence

( QUS [~] is upper & QUS [~] is cap-closed & QUS [~] is axiom_U1 & QUS [~] is axiom_U3 )

end;
coherence

( QUS [~] is upper & QUS [~] is cap-closed & QUS [~] is axiom_U1 & QUS [~] is axiom_U3 )

proof 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 );

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 );

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 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

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;

registration

let SUS be empty Semi-UniformSpace;

coherence

not the entourages of SUS is with_non-empty_elements by Th12, SETFAM_1:def 8;

end;
coherence

not the entourages of SUS is with_non-empty_elements by Th12, SETFAM_1:def 8;

definition

let SUS be non empty Semi-UniformSpace;

end;
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);

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);

:: 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) );

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

for b_{1} being non empty Semi-UniformSpace st b_{1} is axiom_U3 holds

b_{1} is axiom_UL
end;

cluster non empty upper cap-closed axiom_U1 axiom_U2 axiom_U3 -> non empty axiom_UL for UniformSpaceStr ;

coherence for b

b

proof end;

registration
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

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)

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

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

for x being Element of US holds Neighborhood x is Filter of the carrier of US

proof end;

registration
end;

definition

let USS be non empty axiom_U1 topological UniformSpaceStr ;

FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace

end;
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) #);

FMT_Space_Str(# the carrier of USS,(Neighborhood USS) #) is FMT_TopSpace

proof 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) #);

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 ;

FMT2TopSpace (FMT_induced_by USS) is TopSpace ;

end;
func TopSpace_induced_by USS -> TopSpace equals :: UNIFORM2:def 20

FMT2TopSpace (FMT_induced_by USS);

coherence FMT2TopSpace (FMT_induced_by USS);

FMT2TopSpace (FMT_induced_by USS) is TopSpace ;

:: 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);

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;

[:(X \ A),X:] \/ [:X,A:] is Subset of [:X,X:]

end;
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:];

[:(X \ A),X:] \/ [:X,A:] is Subset of [:X,X:]

proof 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:];

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 )

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;

{ (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:]

end;
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 } ;

{ (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;

:: 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 } ;

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
end;

definition

let T be TopSpace;

FinMeetCl (subbasis_Pervin_quasi_uniformity T) is Subset-Family of [: the carrier of T, the carrier of T:] ;

end;
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);

FinMeetCl (subbasis_Pervin_quasi_uniformity T) is Subset-Family of [: the carrier of T, the carrier of T:] ;

:: 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);

for T being TopSpace holds basis_Pervin_quasi_uniformity T = FinMeetCl (subbasis_Pervin_quasi_uniformity T);

registration

let X be set ;

coherence

for b_{1} being non empty Subset-Family of [:X,X:] st b_{1} is cap-closed holds

b_{1} is quasi_basis

end;
coherence

for b

b

proof end;

registration
end;

registration
end;

registration
end;

definition

let T be TopSpace;

UniformSpaceStr(# the carrier of T,<.(basis_Pervin_quasi_uniformity T).] #) is strict Quasi-UniformSpace by Th11bis;

end;
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).] #);

UniformSpaceStr(# the carrier of T,<.(basis_Pervin_quasi_uniformity T).] #) is strict Quasi-UniformSpace by Th11bis;

:: 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).] #);

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

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)

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

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
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

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

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 )

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;