:: by Roland Coghetto

::

:: Received June 30, 2016

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

theorem :: UNIFORM3:1

for X being set

for A being Subset of X holds [:A,A:] \/ [:(X \ A),(X \ A):] c= [:(X \ A),X:] \/ [:X,A:]

for A being Subset of X holds [:A,A:] \/ [:(X \ A),(X \ A):] c= [:(X \ A),X:] \/ [:X,A:]

proof end;

theorem :: UNIFORM3:3

for X being set

for A being Subset of X st X = {1,2,3} & A = {1} holds

( [2,1] in [:(X \ A),X:] \/ [:X,A:] & not [2,1] in [:A,A:] \/ [:(X \ A),(X \ A):] )

for A being Subset of X st X = {1,2,3} & A = {1} holds

( [2,1] in [:(X \ A),X:] \/ [:X,A:] & not [2,1] in [:A,A:] \/ [:(X \ A),(X \ A):] )

proof end;

theorem Th33: :: UNIFORM3:4

for X being set

for A being Subset of X holds ([:A,A:] \/ [:(X \ A),(X \ A):]) ~ = [:A,A:] \/ [:(X \ A),(X \ A):]

for A being Subset of X holds ([:A,A:] \/ [:(X \ A),(X \ A):]) ~ = [:A,A:] \/ [:(X \ A),(X \ A):]

proof end;

Th1: for X being set

for D being a_partition of X

for P1, P2 being Subset of D st union P1 = union P2 holds

P1 c= P2

proof end;

theorem :: UNIFORM3:5

theorem Th2: :: UNIFORM3:6

for X being set

for D being a_partition of X

for P being Subset of D holds union (D \ P) = (union D) \ (union P)

for D being a_partition of X

for P being Subset of D holds union (D \ P) = (union D) \ (union P)

proof end;

theorem Th4: :: UNIFORM3:9

for TG being TopologicalGroup

for e being Element of TG

for V being a_neighborhood of 1_ TG holds {e} * V is a_neighborhood of e

for e being Element of TG

for V being a_neighborhood of 1_ TG holds {e} * V is a_neighborhood of e

proof end;

theorem Th5: :: UNIFORM3:10

for TG being TopologicalGroup

for e being Element of TG

for V being a_neighborhood of 1_ TG holds V * {e} is a_neighborhood of e

for e being Element of TG

for V being a_neighborhood of 1_ TG holds V * {e} is a_neighborhood of e

proof end;

theorem :: UNIFORM3:11

for TG being TopologicalGroup

for V being a_neighborhood of 1_ TG holds V " is a_neighborhood of 1_ TG

for V being a_neighborhood of 1_ TG holds V " is a_neighborhood of 1_ TG

proof end;

:: deftheorem defines axiom_UP2 UNIFORM3:def 1 :

for X being set

for cB being Subset-Family of [:X,X:] holds

( cB is axiom_UP2 iff for B1 being Element of cB ex B2 being Element of cB st B2 c= B1 ~ );

for X being set

for cB being Subset-Family of [:X,X:] holds

( cB is axiom_UP2 iff for B1 being Element of cB ex B2 being Element of cB st B2 c= B1 ~ );

theorem :: UNIFORM3:14

for X being empty set

for cB being empty Subset-Family of [:X,X:] holds

( cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 )

for cB being empty Subset-Family of [:X,X:] holds

( cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 )

proof end;

theorem Th6: :: UNIFORM3:15

for X being set

for SF being Subset-Family of [:X,X:] st X = {{}} & SF = {[:X,X:]} holds

UniformSpaceStr(# X,SF #) is UniformSpace

for SF being Subset-Family of [:X,X:] st X = {{}} & SF = {[:X,X:]} holds

UniformSpaceStr(# X,SF #) is UniformSpace

proof end;

theorem Th7: :: UNIFORM3:16

for X being set

for cB being Subset-Family of [:X,X:] st cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 holds

ex US being strict UniformSpace st

( the carrier of US = X & the entourages of US = <.cB.] )

for cB being Subset-Family of [:X,X:] st cB is quasi_basis & cB is axiom_UP1 & cB is axiom_UP2 & cB is axiom_UP3 holds

ex US being strict UniformSpace st

( the carrier of US = X & the entourages of US = <.cB.] )

proof end;

theorem :: UNIFORM3:17

for US being non empty UniformSpace holds

( the carrier of (TopSpace_induced_by US) = the carrier of US & the topology of (TopSpace_induced_by US) = Family_open_set (FMT_induced_by US) ) by FINTOPO7:def 16;

( the carrier of (TopSpace_induced_by US) = the carrier of US & the topology of (TopSpace_induced_by US) = Family_open_set (FMT_induced_by US) ) by FINTOPO7:def 16;

theorem Th8: :: UNIFORM3:18

for US being non empty UniformSpace

for S being Subset of (FMT_induced_by US) holds

( S is open iff for x being Element of US st x in S holds

S in Neighborhood x )

for S being Subset of (FMT_induced_by US) holds

( S is open iff for x being Element of US st x in S holds

S in Neighborhood x )

proof end;

theorem :: UNIFORM3:19

for US being non empty UniformSpace holds Family_open_set (FMT_induced_by US) = { O where O is open Subset of (FMT_induced_by US) : verum } ;

theorem Th9: :: UNIFORM3:20

for US being non empty UniformSpace

for S being Subset of (FMT_induced_by US) holds

( S is open iff S in Family_open_set (FMT_induced_by US) )

for S being Subset of (FMT_induced_by US) holds

( S is open iff S in Family_open_set (FMT_induced_by US) )

proof end;

theorem :: UNIFORM3:21

for US being non empty UniformSpace

for S being Subset of (FMT_induced_by US) holds

( S in Family_open_set (FMT_induced_by US) iff for x being Element of US st x in S holds

S in Neighborhood x ) by Th8, Th9;

for S being Subset of (FMT_induced_by US) holds

( S in Family_open_set (FMT_induced_by US) iff for x being Element of US st x in S holds

S in Neighborhood x ) by Th8, Th9;

definition

let MS be non empty MetrStruct ;

let r be positive Real;

{ [x,y] where x, y is Element of MS : dist (x,y) <= r } is Subset of [: the carrier of MS, the carrier of MS:]

end;
let r be positive Real;

func fundamental_element_of_entourages (MS,r) -> Subset of [: the carrier of MS, the carrier of MS:] equals :: UNIFORM3:def 2

{ [x,y] where x, y is Element of MS : dist (x,y) <= r } ;

coherence { [x,y] where x, y is Element of MS : dist (x,y) <= r } ;

{ [x,y] where x, y is Element of MS : dist (x,y) <= r } is Subset of [: the carrier of MS, the carrier of MS:]

proof end;

:: deftheorem defines fundamental_element_of_entourages UNIFORM3:def 2 :

for MS being non empty MetrStruct

for r being positive Real holds fundamental_element_of_entourages (MS,r) = { [x,y] where x, y is Element of MS : dist (x,y) <= r } ;

for MS being non empty MetrStruct

for r being positive Real holds fundamental_element_of_entourages (MS,r) = { [x,y] where x, y is Element of MS : dist (x,y) <= r } ;

registration

let MS be non empty Reflexive MetrStruct ;

let r be positive Real;

coherence

not fundamental_element_of_entourages (MS,r) is empty

end;
let r be positive Real;

coherence

not fundamental_element_of_entourages (MS,r) is empty

proof end;

definition

let MS be non empty MetrStruct ;

{ (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } is non empty Subset-Family of [: the carrier of MS, the carrier of MS:]

end;
func fundamental_system_of_entourages MS -> non empty Subset-Family of [: the carrier of MS, the carrier of MS:] equals :: UNIFORM3:def 3

{ (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;

coherence { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;

{ (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } is non empty Subset-Family of [: the carrier of MS, the carrier of MS:]

proof end;

:: deftheorem defines fundamental_system_of_entourages UNIFORM3:def 3 :

for MS being non empty MetrStruct holds fundamental_system_of_entourages MS = { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;

for MS being non empty MetrStruct holds fundamental_system_of_entourages MS = { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;

definition

let MS be non empty MetrStruct ;

UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #) is UniformSpaceStr ;

end;
func uniformity_induced_by MS -> UniformSpaceStr equals :: UNIFORM3:def 4

UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

coherence UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #) is UniformSpaceStr ;

:: deftheorem defines uniformity_induced_by UNIFORM3:def 4 :

for MS being non empty MetrStruct holds uniformity_induced_by MS = UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

for MS being non empty MetrStruct holds uniformity_induced_by MS = UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

Th10: for MS being PseudoMetricSpace ex US being strict UniformSpace st US = uniformity_induced_by MS

proof end;

definition

let MS be PseudoMetricSpace;

UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #) is non empty strict UniformSpace

end;
func uniformity_induced_by MS -> non empty strict UniformSpace equals :: UNIFORM3:def 5

UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

coherence UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #) is non empty strict UniformSpace

proof end;

:: deftheorem defines uniformity_induced_by UNIFORM3:def 5 :

for MS being PseudoMetricSpace holds uniformity_induced_by MS = UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

for MS being PseudoMetricSpace holds uniformity_induced_by MS = UniformSpaceStr(# the carrier of MS,<.(fundamental_system_of_entourages MS).] #);

theorem Th11: :: UNIFORM3:22

for MS being PseudoMetricSpace holds Family_open_set (FMT_induced_by (uniformity_induced_by MS)) = Family_open_set MS

proof end;

theorem :: UNIFORM3:23

for MS being PseudoMetricSpace holds TopSpace_induced_by (uniformity_induced_by MS) = TopSpaceMetr MS

proof end;

definition

let G be TopologicalGroup;

let U be a_neighborhood of 1_ G;

{ [x,y] where x, y is Element of G : (x ") * y in U } is Subset of [: the carrier of G, the carrier of G:]

end;
let U be a_neighborhood of 1_ G;

func element_left_uniformity U -> Subset of [: the carrier of G, the carrier of G:] equals :: UNIFORM3:def 6

{ [x,y] where x, y is Element of G : (x ") * y in U } ;

coherence { [x,y] where x, y is Element of G : (x ") * y in U } ;

{ [x,y] where x, y is Element of G : (x ") * y in U } is Subset of [: the carrier of G, the carrier of G:]

proof end;

:: deftheorem defines element_left_uniformity UNIFORM3:def 6 :

for G being TopologicalGroup

for U being a_neighborhood of 1_ G holds element_left_uniformity U = { [x,y] where x, y is Element of G : (x ") * y in U } ;

for G being TopologicalGroup

for U being a_neighborhood of 1_ G holds element_left_uniformity U = { [x,y] where x, y is Element of G : (x ") * y in U } ;

definition

let TG be TopologicalGroup;

{ (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

end;
func system_left_uniformity TG -> non empty Subset-Family of [: the carrier of TG, the carrier of TG:] equals :: UNIFORM3:def 7

{ (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

coherence { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

{ (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

proof end;

:: deftheorem defines system_left_uniformity UNIFORM3:def 7 :

for TG being TopologicalGroup holds system_left_uniformity TG = { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

for TG being TopologicalGroup holds system_left_uniformity TG = { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

definition

let TG be TopologicalGroup;

UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #) is non empty UniformSpace

end;
func left_uniformity TG -> non empty UniformSpace equals :: UNIFORM3:def 8

UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

coherence UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #) is non empty UniformSpace

proof end;

:: deftheorem defines left_uniformity UNIFORM3:def 8 :

for TG being TopologicalGroup holds left_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

for TG being TopologicalGroup holds left_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

definition

let G be TopologicalGroup;

let U be a_neighborhood of 1_ G;

{ [x,y] where x, y is Element of G : y * (x ") in U } is Subset of [: the carrier of G, the carrier of G:]

end;
let U be a_neighborhood of 1_ G;

func element_right_uniformity U -> Subset of [: the carrier of G, the carrier of G:] equals :: UNIFORM3:def 9

{ [x,y] where x, y is Element of G : y * (x ") in U } ;

coherence { [x,y] where x, y is Element of G : y * (x ") in U } ;

{ [x,y] where x, y is Element of G : y * (x ") in U } is Subset of [: the carrier of G, the carrier of G:]

proof end;

:: deftheorem defines element_right_uniformity UNIFORM3:def 9 :

for G being TopologicalGroup

for U being a_neighborhood of 1_ G holds element_right_uniformity U = { [x,y] where x, y is Element of G : y * (x ") in U } ;

for G being TopologicalGroup

for U being a_neighborhood of 1_ G holds element_right_uniformity U = { [x,y] where x, y is Element of G : y * (x ") in U } ;

definition

let TG be TopologicalGroup;

{ (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

end;
func system_right_uniformity TG -> non empty Subset-Family of [: the carrier of TG, the carrier of TG:] equals :: UNIFORM3:def 10

{ (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

coherence { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

{ (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

proof end;

:: deftheorem defines system_right_uniformity UNIFORM3:def 10 :

for TG being TopologicalGroup holds system_right_uniformity TG = { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

for TG being TopologicalGroup holds system_right_uniformity TG = { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;

definition

let TG be TopologicalGroup;

UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #) is non empty UniformSpace

end;
func right_uniformity TG -> non empty UniformSpace equals :: UNIFORM3:def 11

UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

coherence UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #) is non empty UniformSpace

proof end;

:: deftheorem defines right_uniformity UNIFORM3:def 11 :

for TG being TopologicalGroup holds right_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

for TG being TopologicalGroup holds right_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

theorem Th12: :: UNIFORM3:24

for TG being commutative TopologicalGroup

for U being a_neighborhood of 1_ TG holds element_left_uniformity U = element_right_uniformity U

for U being a_neighborhood of 1_ TG holds element_left_uniformity U = element_right_uniformity U

proof end;

definition

let G be TopaddGroup;

let U be a_neighborhood of 0_ G;

{ [x,y] where x, y is Element of G : (- x) + y in U } is Subset of [: the carrier of G, the carrier of G:]

end;
let U be a_neighborhood of 0_ G;

func element_left_uniformity U -> Subset of [: the carrier of G, the carrier of G:] equals :: UNIFORM3:def 12

{ [x,y] where x, y is Element of G : (- x) + y in U } ;

coherence { [x,y] where x, y is Element of G : (- x) + y in U } ;

{ [x,y] where x, y is Element of G : (- x) + y in U } is Subset of [: the carrier of G, the carrier of G:]

proof end;

:: deftheorem defines element_left_uniformity UNIFORM3:def 12 :

for G being TopaddGroup

for U being a_neighborhood of 0_ G holds element_left_uniformity U = { [x,y] where x, y is Element of G : (- x) + y in U } ;

for G being TopaddGroup

for U being a_neighborhood of 0_ G holds element_left_uniformity U = { [x,y] where x, y is Element of G : (- x) + y in U } ;

definition

let TG be TopaddGroup;

{ (element_left_uniformity U) where U is a_neighborhood of 0_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

end;
func system_left_uniformity TG -> non empty Subset-Family of [: the carrier of TG, the carrier of TG:] equals :: UNIFORM3:def 13

{ (element_left_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

coherence { (element_left_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

{ (element_left_uniformity U) where U is a_neighborhood of 0_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

proof end;

:: deftheorem defines system_left_uniformity UNIFORM3:def 13 :

for TG being TopaddGroup holds system_left_uniformity TG = { (element_left_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

for TG being TopaddGroup holds system_left_uniformity TG = { (element_left_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

definition

let TG be TopologicaladdGroup;

UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #) is non empty UniformSpace

end;
func left_uniformity TG -> non empty UniformSpace equals :: UNIFORM3:def 14

UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

coherence UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #) is non empty UniformSpace

proof end;

:: deftheorem defines left_uniformity UNIFORM3:def 14 :

for TG being TopologicaladdGroup holds left_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

for TG being TopologicaladdGroup holds left_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_left_uniformity TG).] #);

definition

let G be TopaddGroup;

let U be a_neighborhood of 0_ G;

{ [x,y] where x, y is Element of G : y + (- x) in U } is Subset of [: the carrier of G, the carrier of G:]

end;
let U be a_neighborhood of 0_ G;

func element_right_uniformity U -> Subset of [: the carrier of G, the carrier of G:] equals :: UNIFORM3:def 15

{ [x,y] where x, y is Element of G : y + (- x) in U } ;

coherence { [x,y] where x, y is Element of G : y + (- x) in U } ;

{ [x,y] where x, y is Element of G : y + (- x) in U } is Subset of [: the carrier of G, the carrier of G:]

proof end;

:: deftheorem defines element_right_uniformity UNIFORM3:def 15 :

for G being TopaddGroup

for U being a_neighborhood of 0_ G holds element_right_uniformity U = { [x,y] where x, y is Element of G : y + (- x) in U } ;

for G being TopaddGroup

for U being a_neighborhood of 0_ G holds element_right_uniformity U = { [x,y] where x, y is Element of G : y + (- x) in U } ;

definition

let TG be TopaddGroup;

{ (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

end;
func system_right_uniformity TG -> non empty Subset-Family of [: the carrier of TG, the carrier of TG:] equals :: UNIFORM3:def 16

{ (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

coherence { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

{ (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]

proof end;

:: deftheorem defines system_right_uniformity UNIFORM3:def 16 :

for TG being TopaddGroup holds system_right_uniformity TG = { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

for TG being TopaddGroup holds system_right_uniformity TG = { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;

definition

let TG be TopologicaladdGroup;

UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #) is non empty UniformSpace

end;
func right_uniformity TG -> non empty UniformSpace equals :: UNIFORM3:def 17

UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

coherence UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #) is non empty UniformSpace

proof end;

:: deftheorem defines right_uniformity UNIFORM3:def 17 :

for TG being TopologicaladdGroup holds right_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

for TG being TopologicaladdGroup holds right_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);

theorem Th13: :: UNIFORM3:26

for TG being Abelian TopaddGroup

for U being a_neighborhood of 0_ TG holds element_left_uniformity U = element_right_uniformity U

for U being a_neighborhood of 0_ TG holds element_left_uniformity U = element_right_uniformity U

proof end;

theorem :: UNIFORM3:28

for TG being TopologicalGroup holds the topology of (TopSpace_induced_by (left_uniformity TG)) = the topology of TG

proof end;

theorem :: UNIFORM3:29

for TG being TopologicalGroup holds the topology of (TopSpace_induced_by (right_uniformity TG)) = the topology of TG

proof end;

definition

let US1, US2 be UniformSpaceStr ;

let f be Function of US1,US2;

end;
let f be Function of US1,US2;

attr f is uniformly_continuous means :: UNIFORM3:def 18

for V being Element of the entourages of US2 ex U being Element of the entourages of US1 st

for x, y being object st [x,y] in U holds

[(f . x),(f . y)] in V;

for V being Element of the entourages of US2 ex U being Element of the entourages of US1 st

for x, y being object st [x,y] in U holds

[(f . x),(f . y)] in V;

:: deftheorem defines uniformly_continuous UNIFORM3:def 18 :

for US1, US2 being UniformSpaceStr

for f being Function of US1,US2 holds

( f is uniformly_continuous iff for V being Element of the entourages of US2 ex U being Element of the entourages of US1 st

for x, y being object st [x,y] in U holds

[(f . x),(f . y)] in V );

for US1, US2 being UniformSpaceStr

for f being Function of US1,US2 holds

( f is uniformly_continuous iff for V being Element of the entourages of US2 ex U being Element of the entourages of US1 st

for x, y being object st [x,y] in U holds

[(f . x),(f . y)] in V );

registration

let US1, US2 be non empty axiom_U1 UniformSpaceStr ;

ex b_{1} being Function of US1,US2 st b_{1} is uniformly_continuous

end;
cluster Relation-like the carrier of US1 -defined the carrier of US2 -valued Function-like V31( the carrier of US1, the carrier of US2) uniformly_continuous for Element of bool [: the carrier of US1, the carrier of US2:];

existence ex b

proof end;

theorem Th14: :: UNIFORM3:30

for X being set

for D being a_partition of X holds { (union P) where P is Subset of D : verum } = UniCl D

for D being a_partition of X holds { (union P) where P is Subset of D : verum } = UniCl D

proof end;

theorem Th16: :: UNIFORM3:32

for X being set

for D being a_partition of X st D = {} holds

( X is empty & UniCl D = {{}} ) by ZFMISC_1:2, EQREL_1:def 4, YELLOW_9:16;

for D being a_partition of X st D = {} holds

( X is empty & UniCl D = {{}} ) by ZFMISC_1:2, EQREL_1:def 4, YELLOW_9:16;

registration
end;

registration
end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} is union-closed holds

b_{1} is cup-closed

end;
coherence

for b

b

proof end;

registration
end;

registration

let X be set ;

let D be a_partition of X;

coherence

( UniCl D is cup-closed & UniCl D is diff-closed ) ;

end;
let D be a_partition of X;

coherence

( UniCl D is cup-closed & UniCl D is diff-closed ) ;

registration
end;

theorem :: UNIFORM3:34

registration
end;

registration
end;

theorem :: UNIFORM3:35

registration

let X be set ;

let D be a_partition of X;

coherence

( UniCl D is closed_for_countable_unions & UniCl D is closed_for_countable_meets ) by TOPGEN_4:17;

end;
let D be a_partition of X;

coherence

( UniCl D is closed_for_countable_unions & UniCl D is closed_for_countable_meets ) by TOPGEN_4:17;

theorem :: UNIFORM3:36

for Omega being non empty set

for D being a_partition of Omega holds UniCl D is Dynkin_System of Omega

for D being a_partition of Omega holds UniCl D is Dynkin_System of Omega

proof end;

definition

let X be set ;

let D be a_partition of X;

coherence

TopStruct(# X,(UniCl D) #) is TopSpace

end;
let D be a_partition of X;

coherence

TopStruct(# X,(UniCl D) #) is TopSpace

proof end;

:: deftheorem defines partition_topology UNIFORM3:def 19 :

for X being set

for D being a_partition of X holds partition_topology D = TopStruct(# X,(UniCl D) #);

for X being set

for D being a_partition of X holds partition_topology D = TopStruct(# X,(UniCl D) #);

theorem Th18: :: UNIFORM3:37

for X being set

for D being a_partition of X

for O being open Subset of (partition_topology D) holds O is closed

for D being a_partition of X

for O being open Subset of (partition_topology D) holds O is closed

proof end;

theorem Th19: :: UNIFORM3:38

for X being set

for D being a_partition of X

for O being closed Subset of (partition_topology D) holds O is open

for D being a_partition of X

for O being closed Subset of (partition_topology D) holds O is open

proof end;

theorem :: UNIFORM3:39

for X being set

for D being a_partition of X

for S being Subset of (partition_topology D) holds

( S is open iff S is closed ) by Th18, Th19;

for D being a_partition of X

for S being Subset of (partition_topology D) holds

( S is open iff S is closed ) by Th18, Th19;

registration
end;

theorem :: UNIFORM3:40

for X being non empty set

for D being a_partition of X holds capOpCl (partition_topology D) = UniCl D

for D being a_partition of X holds capOpCl (partition_topology D) = UniCl D

proof end;

theorem :: UNIFORM3:41

for X being non empty set

for D being a_partition of X holds OpenClosedSet (partition_topology D) = the topology of (partition_topology D)

for D being a_partition of X holds OpenClosedSet (partition_topology D) = the topology of (partition_topology D)

proof end;

definition

let X be set ;

let R be Relation of X;

{ S where S is Subset of [:X,X:] : R c= S } is non empty Subset-Family of [:X,X:]

end;
let R be Relation of X;

func rho R -> non empty Subset-Family of [:X,X:] equals :: UNIFORM3:def 20

{ S where S is Subset of [:X,X:] : R c= S } ;

coherence { S where S is Subset of [:X,X:] : R c= S } ;

{ S where S is Subset of [:X,X:] : R c= S } is non empty Subset-Family of [:X,X:]

proof end;

:: deftheorem defines rho UNIFORM3:def 20 :

for X being set

for R being Relation of X holds rho R = { S where S is Subset of [:X,X:] : R c= S } ;

for X being set

for R being Relation of X holds rho R = { S where S is Subset of [:X,X:] : R c= S } ;

definition

let X be set ;

let R be Relation of X;

UniformSpaceStr(# X,(rho R) #) is strict upper cap-closed UniformSpaceStr

end;
let R be Relation of X;

func uniformity_induced_by R -> strict upper cap-closed UniformSpaceStr equals :: UNIFORM3:def 21

UniformSpaceStr(# X,(rho R) #);

coherence UniformSpaceStr(# X,(rho R) #);

UniformSpaceStr(# X,(rho R) #) is strict upper cap-closed UniformSpaceStr

proof end;

:: deftheorem defines uniformity_induced_by UNIFORM3:def 21 :

for X being set

for R being Relation of X holds uniformity_induced_by R = UniformSpaceStr(# X,(rho R) #);

for X being set

for R being Relation of X holds uniformity_induced_by R = UniformSpaceStr(# X,(rho R) #);

theorem Th27: :: UNIFORM3:50

for X being set

for R being total transitive Relation of X holds uniformity_induced_by R is axiom_U3

for R being total transitive Relation of X holds uniformity_induced_by R is axiom_U3

proof end;

definition

let X be set ;

let R be Tolerance of X;

:: original: uniformity_induced_by

redefine func uniformity_induced_by R -> strict Semi-UniformSpace;

coherence

uniformity_induced_by R is strict Semi-UniformSpace by Th25, Th26;

end;
let R be Tolerance of X;

:: original: uniformity_induced_by

redefine func uniformity_induced_by R -> strict Semi-UniformSpace;

coherence

uniformity_induced_by R is strict Semi-UniformSpace by Th25, Th26;

theorem :: UNIFORM3:51

for X being set

for R being Equivalence_Relation of X holds uniformity_induced_by R is UniformSpace by Th27;

for R being Equivalence_Relation of X holds uniformity_induced_by R is UniformSpace by Th27;

definition

let X be set ;

let R be Equivalence_Relation of X;

:: original: uniformity_induced_by

redefine func uniformity_induced_by R -> strict UniformSpace;

coherence

uniformity_induced_by R is strict UniformSpace by Th25, Th26, Th27;

end;
let R be Equivalence_Relation of X;

:: original: uniformity_induced_by

redefine func uniformity_induced_by R -> strict UniformSpace;

coherence

uniformity_induced_by R is strict UniformSpace by Th25, Th26, Th27;

registration
end;

registration

for b_{1} being non empty UniformSpace holds b_{1} is topological
;

end;

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

coherence for b

definition
end;

theorem :: UNIFORM3:52

for X being non empty set

for R being Equivalence_Relation of X holds TopSpace_induced_by (@ (uniformity_induced_by R)) = partition_topology (Class R)

for R being Equivalence_Relation of X holds TopSpace_induced_by (@ (uniformity_induced_by R)) = partition_topology (Class R)

proof end;

theorem :: UNIFORM3:53

for USS being upper UniformSpaceStr st meet the entourages of USS in the entourages of USS holds

ex R being Relation of the carrier of USS st

( meet the entourages of USS = R & the entourages of USS = rho R )

ex R being Relation of the carrier of USS st

( meet the entourages of USS = R & the entourages of USS = rho R )

proof end;

definition

let USS be UniformSpaceStr ;

meet the entourages of USS is Relation of the carrier of USS ;

end;
func Uniformity2InternalRel USS -> Relation of the carrier of USS equals :: UNIFORM3:def 23

meet the entourages of USS;

coherence meet the entourages of USS;

meet the entourages of USS is Relation of the carrier of USS ;

:: deftheorem defines Uniformity2InternalRel UNIFORM3:def 23 :

for USS being UniformSpaceStr holds Uniformity2InternalRel USS = meet the entourages of USS;

for USS being UniformSpaceStr holds Uniformity2InternalRel USS = meet the entourages of USS;

definition

let USS be UniformSpaceStr ;

RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #) is RelStr ;

end;
func UniformSpaceStr2RelStr USS -> RelStr equals :: UNIFORM3:def 24

RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #);

coherence RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #);

RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #) is RelStr ;

:: deftheorem defines UniformSpaceStr2RelStr UNIFORM3:def 24 :

for USS being UniformSpaceStr holds UniformSpaceStr2RelStr USS = RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #);

for USS being UniformSpaceStr holds UniformSpaceStr2RelStr USS = RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #);

definition

let RS be RelStr ;

{ R where R is Relation of the carrier of RS : the InternalRel of RS c= R } is Subset-Family of [: the carrier of RS, the carrier of RS:]

end;
func InternalRel2Uniformity RS -> Subset-Family of [: the carrier of RS, the carrier of RS:] equals :: UNIFORM3:def 25

{ R where R is Relation of the carrier of RS : the InternalRel of RS c= R } ;

coherence { R where R is Relation of the carrier of RS : the InternalRel of RS c= R } ;

{ R where R is Relation of the carrier of RS : the InternalRel of RS c= R } is Subset-Family of [: the carrier of RS, the carrier of RS:]

proof end;

:: deftheorem defines InternalRel2Uniformity UNIFORM3:def 25 :

for RS being RelStr holds InternalRel2Uniformity RS = { R where R is Relation of the carrier of RS : the InternalRel of RS c= R } ;

for RS being RelStr holds InternalRel2Uniformity RS = { R where R is Relation of the carrier of RS : the InternalRel of RS c= R } ;

definition

let RS be RelStr ;

UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #) is strict UniformSpaceStr ;

end;
func RelStr2UniformSpaceStr RS -> strict UniformSpaceStr equals :: UNIFORM3:def 26

UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #);

coherence UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #);

UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #) is strict UniformSpaceStr ;

:: deftheorem defines RelStr2UniformSpaceStr UNIFORM3:def 26 :

for RS being RelStr holds RelStr2UniformSpaceStr RS = UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #);

for RS being RelStr holds RelStr2UniformSpaceStr RS = UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #);

definition

let RS be RelStr ;

the InternalRel of RS is Element of the entourages of (RelStr2UniformSpaceStr RS)

end;
func InternalRel2Element RS -> Element of the entourages of (RelStr2UniformSpaceStr RS) equals :: UNIFORM3:def 27

the InternalRel of RS;

coherence the InternalRel of RS;

the InternalRel of RS is Element of the entourages of (RelStr2UniformSpaceStr RS)

proof end;

:: deftheorem defines InternalRel2Element UNIFORM3:def 27 :

for RS being RelStr holds InternalRel2Element RS = the InternalRel of RS;

for RS being RelStr holds InternalRel2Element RS = the InternalRel of RS;

theorem :: UNIFORM3:56

for US being UniformSpaceStr holds

( the carrier of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr US)) = the carrier of US & the entourages of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr US)) = rho (meet the entourages of US) ) ;

( the carrier of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr US)) = the carrier of US & the entourages of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr US)) = rho (meet the entourages of US) ) ;

theorem Th29: :: UNIFORM3:57

for X being set

for SF being Subset-Family of [:X,X:]

for R being Relation of X st SF = rho R holds

SF c= rho (meet SF)

for SF being Subset-Family of [:X,X:]

for R being Relation of X st SF = rho R holds

SF c= rho (meet SF)

proof end;

theorem Th30: :: UNIFORM3:58

for X being set

for SF being upper Subset-Family of [:X,X:] st meet SF in SF holds

rho (meet SF) c= SF

for SF being upper Subset-Family of [:X,X:] st meet SF in SF holds

rho (meet SF) c= SF

proof end;

theorem :: UNIFORM3:59

theorem Th31: :: UNIFORM3:60

for US being upper UniformSpaceStr st ex R being Relation of the carrier of US st

( the entourages of US = rho R & meet the entourages of US in the entourages of US ) holds

the entourages of US = rho (meet the entourages of US)

( the entourages of US = rho R & meet the entourages of US in the entourages of US ) holds

the entourages of US = rho (meet the entourages of US)

proof end;

theorem :: UNIFORM3:61

for US being upper UniformSpaceStr

for R being Relation of the carrier of US st the entourages of US = rho R & meet the entourages of US in the entourages of US holds

the entourages of US = rho (meet the entourages of US) by Th31;

for R being Relation of the carrier of US st the entourages of US = rho R & meet the entourages of US in the entourages of US holds

the entourages of US = rho (meet the entourages of US) by Th31;

theorem :: UNIFORM3:62

for X being set

for R being Tolerance of X holds

( uniformity_induced_by R is Semi-UniformSpace & the entourages of (uniformity_induced_by R) = rho R & meet the entourages of (uniformity_induced_by R) = R ) by Th28;

for R being Tolerance of X holds

( uniformity_induced_by R is Semi-UniformSpace & the entourages of (uniformity_induced_by R) = rho R & meet the entourages of (uniformity_induced_by R) = R ) by Th28;

theorem :: UNIFORM3:63

for X being set

for R being Tolerance of X holds RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R

for R being Tolerance of X holds RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R

proof end;

theorem :: UNIFORM3:64

for X being set

for R being Equivalence_Relation of X holds RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R

for R being Equivalence_Relation of X holds RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R

proof end;

definition

let X be set ;

let SF be Subset-Family of X;

let A be Element of SF;

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

end;
let SF be Subset-Family of X;

let A be Element of SF;

func block_Pervin_uniformity A -> Subset of [:X,X:] equals :: UNIFORM3:def 28

[:(X \ A),(X \ A):] \/ [:A,A:];

coherence [:(X \ A),(X \ A):] \/ [:A,A:];

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

proof end;

:: deftheorem defines block_Pervin_uniformity UNIFORM3:def 28 :

for X being set

for SF being Subset-Family of X

for A being Element of SF holds block_Pervin_uniformity A = [:(X \ A),(X \ A):] \/ [:A,A:];

for X being set

for SF being Subset-Family of X

for A being Element of SF holds block_Pervin_uniformity A = [:(X \ A),(X \ A):] \/ [:A,A:];

theorem Th34: :: UNIFORM3:65

for X being set

for SF being Subset-Family of X

for A being Element of SF st A = {} holds

block_Pervin_uniformity A = [:X,X:]

for SF being Subset-Family of X

for A being Element of SF st A = {} holds

block_Pervin_uniformity A = [:X,X:]

proof end;

theorem :: UNIFORM3:66

for X being set

for SF being Subset-Family of X

for A being Element of SF st not X is empty holds

block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) }

for SF being Subset-Family of X

for A being Element of SF st not X is empty holds

block_Pervin_uniformity A = { [x,y] where x, y is Element of X : ( x in A iff y in A ) }

proof end;

theorem Th35: :: UNIFORM3:67

for X being set

for SF being Subset-Family of X

for A being Element of SF holds

( id X c= block_Pervin_uniformity A & (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A )

for SF being Subset-Family of X

for A being Element of SF holds

( id X c= block_Pervin_uniformity A & (block_Pervin_uniformity A) * (block_Pervin_uniformity A) c= block_Pervin_uniformity A )

proof end;

definition

let X be set ;

let SF be Subset-Family of X;

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

end;
let SF be Subset-Family of X;

func subbasis_Pervin_uniformity SF -> Subset-Family of [:X,X:] equals :: UNIFORM3:def 29

{ (block_Pervin_uniformity A) where A is Element of SF : verum } ;

coherence { (block_Pervin_uniformity A) where A is Element of SF : verum } ;

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

proof end;

:: deftheorem defines subbasis_Pervin_uniformity UNIFORM3:def 29 :

for X being set

for SF being Subset-Family of X holds subbasis_Pervin_uniformity SF = { (block_Pervin_uniformity A) where A is Element of SF : verum } ;

for X being set

for SF being Subset-Family of X holds subbasis_Pervin_uniformity SF = { (block_Pervin_uniformity A) where A is Element of SF : verum } ;

registration

let X be set ;

let SF be Subset-Family of X;

coherence

not subbasis_Pervin_uniformity SF is empty

end;
let SF be Subset-Family of X;

coherence

not subbasis_Pervin_uniformity SF is empty

proof end;

definition

let X be set ;

let SF be Subset-Family of X;

FinMeetCl (subbasis_Pervin_uniformity SF) is Subset-Family of [:X,X:] ;

end;
let SF be Subset-Family of X;

func basis_Pervin_uniformity SF -> Subset-Family of [:X,X:] equals :: UNIFORM3:def 30

FinMeetCl (subbasis_Pervin_uniformity SF);

coherence FinMeetCl (subbasis_Pervin_uniformity SF);

FinMeetCl (subbasis_Pervin_uniformity SF) is Subset-Family of [:X,X:] ;

:: deftheorem defines basis_Pervin_uniformity UNIFORM3:def 30 :

for X being set

for SF being Subset-Family of X holds basis_Pervin_uniformity SF = FinMeetCl (subbasis_Pervin_uniformity SF);

for X being set

for SF being Subset-Family of X holds basis_Pervin_uniformity SF = FinMeetCl (subbasis_Pervin_uniformity SF);

theorem Th39: :: UNIFORM3:71

for X being set

for SF being Subset-Family of X

for A being Element of SF

for R being Relation of X st R = block_Pervin_uniformity A holds

R ~ = block_Pervin_uniformity A

for SF being Subset-Family of X

for A being Element of SF

for R being Relation of X st R = block_Pervin_uniformity A holds

R ~ = block_Pervin_uniformity A

proof end;

theorem :: UNIFORM3:72

for X being set

for SF being Subset-Family of X

for R being Relation of X st R is Element of subbasis_Pervin_uniformity SF holds

R ~ is Element of subbasis_Pervin_uniformity SF

for SF being Subset-Family of X

for R being Relation of X st R is Element of subbasis_Pervin_uniformity SF holds

R ~ is Element of subbasis_Pervin_uniformity SF

proof end;

theorem Th40: :: UNIFORM3:73

for X being set

for SF being Subset-Family of X

for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds

Y [~] = Y

for SF being Subset-Family of X

for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds

Y [~] = Y

proof end;

theorem Th41: :: UNIFORM3:74

for X being set

for SF being Subset-Family of X

for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds

(meet Y) ~ = meet (Y [~])

for SF being Subset-Family of X

for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds

(meet Y) ~ = meet (Y [~])

proof end;

theorem Th42: :: UNIFORM3:75

for X being set

for SF being Subset-Family of X

for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds

meet Y = (meet Y) ~

for SF being Subset-Family of X

for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity SF holds

meet Y = (meet Y) ~

proof end;

Th45: for X being set

for SF being Subset-Family of X ex US being strict UniformSpace st

( the carrier of US = X & the entourages of US = <.(basis_Pervin_uniformity SF).] )

proof end;

definition

let X be set ;

let SF be Subset-Family of X;

UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #) is strict UniformSpace

end;
let SF be Subset-Family of X;

func Pervin_uniform_space SF -> strict UniformSpace equals :: UNIFORM3:def 31

UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #);

coherence UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #);

UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #) is strict UniformSpace

proof end;

:: deftheorem defines Pervin_uniform_space UNIFORM3:def 31 :

for X being set

for SF being Subset-Family of X holds Pervin_uniform_space SF = UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #);

for X being set

for SF being Subset-Family of X holds Pervin_uniform_space SF = UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #);