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

theorem Th32: :: UNIFORM3:2
{1,2,3} \ {1} = {2,3}
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):] )
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):]
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
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 = P2 by Th1;

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

theorem :: UNIFORM3:7
for X being set
for SF being upper Subset-Family of X
for S being Element of SF holds meet SF c= S
proof end;

theorem Th3: :: UNIFORM3:8
for G being addGroup
for A, B, C, D being Subset of G st A c= B & C c= D holds
A + C c= B + D
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
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
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
proof end;

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

theorem :: UNIFORM3:12
for US being UniformSpace holds US is axiom_U2 Quasi-UniformSpace ;

theorem :: UNIFORM3:13
for US being UniformSpace holds US is axiom_U3 Semi-UniformSpace ;

definition
let X be set ;
let cB be Subset-Family of [:X,X:];
attr cB is axiom_UP2 means :: UNIFORM3:def 1
 for B1 being Element of cB ex B2 being Element of cB st B2 c= B1 ~ ;
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 ~ );

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

registration
cluster strict non void upper cap-closed axiom_U1 axiom_U2 axiom_U3 for UniformSpaceStr ;
existence
ex b1 being UniformSpace st b1 is strict
proof end;
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
proof end;

registration
cluster non empty strict non void upper cap-closed axiom_U1 axiom_U2 axiom_U3 for UniformSpaceStr ;
existence
not for b1 being strict UniformSpace holds b1 is empty
proof end;
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.] )
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;

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

definition
let MS be non empty MetrStruct ;
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 } is Subset of [: the carrier of MS, the carrier of MS:]
proof end;
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 } ;

registration
let MS be non empty Reflexive MetrStruct ;
let r be positive Real;
cluster fundamental_element_of_entourages (MS,r) -> non empty ;
coherence
not fundamental_element_of_entourages (MS,r) is empty
proof end;
end;

definition
let MS be non empty MetrStruct ;
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 } is non empty Subset-Family of [: the carrier of MS, the carrier of MS:]
proof end;
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 } ;

definition
let MS be non empty MetrStruct ;
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).] #) is UniformSpaceStr ;
end;

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

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

definition
let MS be PseudoMetricSpace;
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).] #) is non empty strict UniformSpace
proof end;
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).] #);

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;
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 } is Subset of [: the carrier of G, the carrier of G:]
proof end;
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 } ;

definition
let TG be TopologicalGroup;
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 } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]
proof end;
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 } ;

definition
let TG be TopologicalGroup;
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).] #) is non empty UniformSpace
proof end;
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).] #);

definition
let G be TopologicalGroup;
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 } is Subset of [: the carrier of G, the carrier of G:]
proof end;
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 } ;

definition
let TG be TopologicalGroup;
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 } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]
proof end;
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 } ;

definition
let TG be TopologicalGroup;
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).] #) is non empty UniformSpace
proof end;
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).] #);

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

theorem :: UNIFORM3:25
for TG being commutative TopologicalGroup holds left_uniformity TG = right_uniformity TG
proof end;

definition
let G be TopaddGroup;
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 } is Subset of [: the carrier of G, the carrier of G:]
proof end;
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 } ;

definition
let TG be TopaddGroup;
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 } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]
proof end;
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 } ;

definition
let TG be TopologicaladdGroup;
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).] #) is non empty UniformSpace
proof end;
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).] #);

definition
let G be TopaddGroup;
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 } is Subset of [: the carrier of G, the carrier of G:]
proof end;
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 } ;

definition
let TG be TopaddGroup;
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 } is non empty Subset-Family of [: the carrier of TG, the carrier of TG:]
proof end;
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 } ;

definition
let TG be TopologicaladdGroup;
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).] #) is non empty UniformSpace
proof end;
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).] #);

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

theorem :: UNIFORM3:27
for TG being TopologicaladdGroup st TG is Abelian holds
left_uniformity TG = right_uniformity TG
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;
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;
end;

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

registration
let US1, US2 be non empty axiom_U1 UniformSpaceStr ;
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 b1 being Function of US1,US2 st b1 is uniformly_continuous
proof end;
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
proof end;

theorem Th15: :: UNIFORM3:31
for X being set
for D being a_partition of X holds X in 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;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> V288() ;
coherence
UniCl D is intersection_stable
proof end;
end;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> union-closed ;
coherence
UniCl D is union-closed
proof end;
end;

registration
let X be set ;
cluster union-closed -> cup-closed for Element of bool (bool X);
coherence
for b1 being Subset-Family of X st b1 is union-closed holds
b1 is cup-closed
proof end;
end;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> compl-closed ;
coherence
UniCl D is compl-closed
proof end;
end;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> cup-closed diff-closed ;
coherence
( UniCl D is cup-closed & UniCl D is diff-closed ) ;
end;

theorem :: UNIFORM3:33
for X being set
for D being a_partition of X holds UniCl D is Ring_of_sets
proof end;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> with_empty_element ;
coherence
UniCl D is with_empty_element
proof end;
end;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> non empty ;
coherence
not UniCl D is empty ;
end;

theorem :: UNIFORM3:34
for X being set
for D being a_partition of X holds UniCl D is Field_Subset of X ;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> sigma-additive ;
coherence
UniCl D is sigma-additive
proof end;
end;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> sigma-multiplicative ;
coherence
UniCl D is sigma-multiplicative ;
end;

theorem :: UNIFORM3:35
for X being set
for D being a_partition of X holds UniCl D is SigmaField of X ;

registration
let X be set ;
let D be a_partition of X;
cluster UniCl D -> closed_for_countable_unions closed_for_countable_meets ;
coherence
( UniCl D is closed_for_countable_unions & UniCl D is closed_for_countable_meets ) by TOPGEN_4:17;
end;

theorem :: UNIFORM3:36
for Omega being non empty set
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;
func partition_topology D -> TopSpace equals :: UNIFORM3:def 19
 TopStruct(# X,(UniCl D) #);
coherence
TopStruct(# X,(UniCl D) #) is TopSpace
proof end;
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) #);

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

registration
let X be non empty set ;
let D be a_partition of X;
cluster partition_topology D -> non empty ;
coherence
not partition_topology D is empty ;
end;

theorem :: UNIFORM3:40
for X being non empty set
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)
proof end;

definition
let X be set ;
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 } is non empty Subset-Family of [:X,X:]
proof end;
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 } ;

theorem :: UNIFORM3:42
for X being set
for R being Relation of X holds <.(rho R).] = rho R
proof end;

theorem :: UNIFORM3:43
for X being set
for R being Relation of X holds <.{R}.] = rho R
proof end;

theorem Th20: :: UNIFORM3:44
for X being set
for R being Relation of X holds
( rho R is upper & rho R is V288() )
proof end;

registration
let X be set ;
let R be Relation of X;
cluster rho R -> non empty quasi_basis ;
coherence
rho R is quasi_basis
proof end;
end;

theorem Th21: :: UNIFORM3:45
for X being set
for R being total reflexive Relation of X holds rho R is axiom_UP1
proof end;

theorem Th22: :: UNIFORM3:46
for X being set
for R being symmetric Relation of X holds rho R is axiom_UP2
proof end;

theorem Th24: :: UNIFORM3:47
for X being set
for R being total transitive Relation of X holds rho R is axiom_UP3
proof end;

definition
let X be set ;
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) #) is strict upper cap-closed UniformSpaceStr
proof end;
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) #);

theorem Th25: :: UNIFORM3:48
for X being set
for R being total reflexive Relation of X holds uniformity_induced_by R is axiom_U1
proof end;

theorem Th26: :: UNIFORM3:49
for X being set
for R being symmetric Relation of X holds uniformity_induced_by R is axiom_U2
proof end;

theorem Th27: :: UNIFORM3:50
for X being set
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;

theorem :: UNIFORM3:51
for X being set
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;

registration
let X be non empty set ;
let R be Tolerance of X;
cluster uniformity_induced_by R -> non empty strict upper cap-closed ;
coherence
not uniformity_induced_by R is empty ;
end;

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

definition
let US be non empty UniformSpace;
func @ US -> non empty axiom_U1 topological UniformSpaceStr equals :: UNIFORM3:def 22
US;
coherence
US is non empty axiom_U1 topological UniformSpaceStr ;
end;

:: deftheorem defines @ UNIFORM3:def 22 :
for US being non empty UniformSpace holds @ US = US;

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

definition
let USS be UniformSpaceStr ;
func Uniformity2InternalRel USS -> Relation of the carrier of USS equals :: UNIFORM3:def 23
 meet the entourages of USS;
coherence
meet the entourages of USS is Relation of the carrier of USS ;
end;

:: deftheorem defines Uniformity2InternalRel UNIFORM3:def 23 :
for USS being UniformSpaceStr holds Uniformity2InternalRel USS = meet the entourages of USS;

definition
let USS be UniformSpaceStr ;
func UniformSpaceStr2RelStr USS -> RelStr equals :: UNIFORM3:def 24
 RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #);
coherence
RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #) is RelStr ;
end;

:: deftheorem defines UniformSpaceStr2RelStr UNIFORM3:def 24 :
for USS being UniformSpaceStr holds UniformSpaceStr2RelStr USS = RelStr(# the carrier of USS,(Uniformity2InternalRel USS) #);

definition
let RS be RelStr ;
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 } is Subset-Family of [: the carrier of RS, the carrier of RS:]
proof end;
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 } ;

definition
let RS be RelStr ;
func RelStr2UniformSpaceStr RS -> strict UniformSpaceStr equals :: UNIFORM3:def 26
 UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #);
coherence
UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #) is strict UniformSpaceStr ;
end;

:: deftheorem defines RelStr2UniformSpaceStr UNIFORM3:def 26 :
for RS being RelStr holds RelStr2UniformSpaceStr RS = UniformSpaceStr(# the carrier of RS,(InternalRel2Uniformity RS) #);

definition
let RS be RelStr ;
func InternalRel2Element RS -> Element of the entourages of (RelStr2UniformSpaceStr RS) equals :: UNIFORM3:def 27
 the InternalRel of RS;
coherence
the InternalRel of RS is Element of the entourages of (RelStr2UniformSpaceStr RS)
proof end;
end;

:: deftheorem defines InternalRel2Element UNIFORM3:def 27 :
for RS being RelStr holds InternalRel2Element RS = the InternalRel of RS;

theorem Th28: :: UNIFORM3:54
for X being set
for R being Relation of X holds meet (rho R) = R
proof end;

theorem :: UNIFORM3:55
for RS being strict RelStr holds UniformSpaceStr2RelStr (RelStr2UniformSpaceStr RS) = RS
proof end;

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

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

theorem :: UNIFORM3:59
for X being set
for SF being upper Subset-Family of [:X,X:]
for R being Relation of X st R in SF & SF = rho R & meet SF in SF holds
rho (meet SF) = SF by Th29, Th30;

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

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;

theorem :: UNIFORM3:63
for X being set
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
proof end;

definition
let X be set ;
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:] is Subset of [:X,X:]
proof end;
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:];

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

definition
let X be set ;
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 } is Subset-Family of [:X,X:]
proof end;
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 } ;

registration
let X be set ;
let SF be Subset-Family of X;
cluster subbasis_Pervin_uniformity SF -> non empty ;
coherence
not subbasis_Pervin_uniformity SF is empty
proof end;
end;

definition
let X be set ;
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) is Subset-Family of [:X,X:] ;
end;

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

theorem Th36: :: UNIFORM3:68
for X being set
for SF being Subset-Family of X holds basis_Pervin_uniformity SF is V288()
proof end;

theorem Th37: :: UNIFORM3:69
for X being set
for SF being Subset-Family of X holds basis_Pervin_uniformity SF is quasi_basis
proof end;

theorem Th38: :: UNIFORM3:70
for X being set
for SF being Subset-Family of X holds basis_Pervin_uniformity SF is axiom_UP1
proof end;

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

theorem Th43: :: UNIFORM3:76
for X being set
for SF being Subset-Family of X holds basis_Pervin_uniformity SF is axiom_UP2
proof end;

theorem Th44: :: UNIFORM3:77
for X being set
for SF being Subset-Family of X holds basis_Pervin_uniformity SF is axiom_UP3
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;
func Pervin_uniform_space SF -> strict UniformSpace equals :: UNIFORM3:def 31
 UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #);
coherence
UniformSpaceStr(# X,<.(basis_Pervin_uniformity SF).] #) is strict UniformSpace
proof end;
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).] #);