:: 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 b₁ being UniformSpace st b₁ 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 b₁ being strict UniformSpace holds b₁ 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 b₁ being Function of US1,US2 st b₁ 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 b₁ being Subset-Family of X st b₁ is union-closed holds
b₁ 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 b₁ being non empty UniformSpace holds b₁ 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).] #);