:: Uniform Space :: by Roland Coghetto :: :: Received June 30, 2016 :: Copyright (c) 2016-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDERS_2, CONNSP_2, GROUP_1, YELLOW_6, FINTOPO7, FINTOPO2, RELAT_2, REAL_1, METRIC_1, PRE_TOPC, FUNCT_1, STRUCT_0, CARD_1, XBOOLE_0, SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1, RELAT_1, XXREAL_0, WAYBEL_0, NUMBERS, ARYTM_3, CANTOR_1, FILTER_0, XXREAL_1, ARYTM_1, PCOMPS_1, RCOMP_1, FINSUB_1, TOPGRP_1, BINOP_1, POLYNOM1, GROUP_1A, RLVECT_1, FCONT_2, FUNCOP_1, UNIFORM2, UNIFORM3, EQREL_1, PARTFUN1, SIMPLEX0, CARD_3, SRINGS_4, CAT_4, PROB_1, QC_LANG1, TOLER_1, ROUGHS_4, LATTICE7, MEASURE1, TOPGEN_4, DYNKIN, PROB_2, FINSET_1, LOPCLSET, FINSEQ_1; notations CANTOR_1, EQREL_1, TOLER_1, SIMPLEX0, TOPGEN_4, DYNKIN, SRINGS_4, ORDINAL1, IDEAL_1, TARSKI, RELAT_1, SETFAM_1, XXREAL_0, XBOOLE_0, RELSET_1, XREAL_0, FUNCT_1, ZFMISC_1, SUBSET_1, XCMPLX_0, STRUCT_0, METRIC_1, DOMAIN_1, MCART_1, CARDFIL2, FINSUB_1, FINTOPO2, PARTFUN1, TOPGRP_1, CONNSP_2, GROUP_1, GROUP_2, ALGSTR_0, FINTOPO7, PCOMPS_1, GROUP_1A, RLVECT_1, PRE_TOPC, UNIFORM2, RELAT_2, ROUGHS_4, LATTICE7, PROB_1, MEASURE1, ORDERS_2, FINSET_1, LOPCLSET; constructors CARDFIL2, TOPMETR, COMPTS_1, GROUP_2, PCOMPS_1, GROUP_1A, UNIFORM2, COHSP_1, CANTOR_1, TOPGEN_4, DYNKIN, SRINGS_4, ROUGHS_4, LATTICE7, MEASURE1, LOPCLSET; registrations CARDFIL2, FIN_TOPO, RELAT_1, ZFMISC_1, METRIC_1, XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, XXREAL_0, FINTOPO7, TOPGRP_1, GROUP_1, PCOMPS_1, GROUP_1A, XCMPLX_0, UNIFORM2, PARTFUN1, TOPGEN_4, PRE_TOPC, MEASURE1, FINSET_1, CANTOR_1; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: Preliminaries reserve X for set, D for a_partition of X, TG for non empty TopologicalGroup; reserve A for Subset of X; theorem :: UNIFORM3:1 [:A,A:] \/ [:X \ A,X \ A:] c= [:X \ A,X:] \/ [:X,A:]; theorem :: UNIFORM3:2 {1,2,3} \ {1} = {2,3}; theorem :: UNIFORM3:3 X = {1,2,3} & A = {1} implies [2,1] in [:X \ A,X:] \/ [:X,A:] & not [2,1] in [:A,A:] \/ [:X \ A,X \ A:]; theorem :: UNIFORM3:4 for A being Subset of X holds ([:A,A:] \/ [:X \ A,X \ A:])~ = [:A,A:] \/ [:X \ A,X \ A:]; theorem :: UNIFORM3:5 for P1,P2 being Subset of D st union P1 = union P2 holds P1 = P2; theorem :: UNIFORM3:6 :: EQREL_1:43 generalized for P being Subset of D holds union (D \ P) = union D \ union P; theorem :: UNIFORM3:7 for SF being upper Subset-Family of X, S being Element of SF holds meet SF c= S; theorem :: UNIFORM3:8 for G being addGroup,A,B,C,D being Subset of G st A c= B & C c= D holds A + C c= B + D; theorem :: UNIFORM3:9 for e being Element of TG, V being a_neighborhood of 1_TG holds {e} * V is a_neighborhood of e; theorem :: UNIFORM3:10 for e being Element of TG, V being a_neighborhood of 1_TG holds V * {e} is a_neighborhood of e; theorem :: UNIFORM3:11 for V being a_neighborhood of 1_TG holds V" is a_neighborhood of 1_TG; begin :: UniformSpace definition mode UniformSpace is upper cap-closed axiom_U1 axiom_U2 axiom_U3 UniformSpaceStr; end; reserve US for UniformSpace; theorem :: UNIFORM3:12 US is axiom_U2 Quasi-UniformSpace; theorem :: UNIFORM3:13 US is axiom_U3 Semi-UniformSpace; definition let X be set, cB be Subset-Family of [:X,X:]; attr cB is axiom_UP2 means :: UNIFORM3:def 1 for B1 being Element of cB holds ex B2 being Element of cB st B2 c= B1~; end; theorem :: UNIFORM3:14 for X being empty set,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; registration cluster strict for UniformSpace; end; theorem :: UNIFORM3:15 for X being set, SF being Subset-Family of [:X,X:] st X = {{}} & SF = {[:X,X:]} holds UniformSpaceStr(# X,SF #) is UniformSpace; registration cluster non empty for strict UniformSpace; end; theorem :: UNIFORM3:16 for X being set,cB being Subset-Family of [:X,X:] st cB is quasi_basis axiom_UP1 axiom_UP2 axiom_UP3 holds ex US being strict UniformSpace st the carrier of US = X & the entourages of US = <.cB.]; begin :: Open set and UniformSpace 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)) ; theorem :: UNIFORM3:18 for US being non empty UniformSpace, 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; theorem :: UNIFORM3:19 for US being non empty UniformSpace holds Family_open_set(FMT_induced_by(US)) = the set of all O where O is open Subset of FMT_induced_by(US); theorem :: UNIFORM3:20 for US being non empty UniformSpace, S being Subset of FMT_induced_by(US) holds S is open iff S in Family_open_set(FMT_induced_by(US)); theorem :: UNIFORM3:21 for US being non empty UniformSpace, 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; begin :: Pseudo-metric space and Uniform Space definition let MS be non empty MetrStruct, 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}; end; registration let MS be non empty Reflexive MetrStruct, r be positive Real; cluster fundamental_element_of_entourages(MS,r) -> non empty; 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 the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; end; 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) .] #); 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) .] #); end; theorem :: UNIFORM3:22 for MS being PseudoMetricSpace holds Family_open_set(FMT_induced_by(uniformity_induced_by(MS))) = Family_open_set MS; theorem :: UNIFORM3:23 for MS being PseudoMetricSpace holds TopSpace_induced_by(uniformity_induced_by(MS)) = TopSpaceMetr(MS); begin :: Uniform space and topological group 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 is Element of G,y is Element of G: x" * y in U}; end; definition let TG be non empty TopologicalGroup; func system_left_uniformity(TG) -> non empty Subset-Family of [:the carrier of TG,the carrier of TG:] equals :: UNIFORM3:def 7 the set of all element_left_uniformity(U) where U is a_neighborhood of 1_TG; end; definition let TG be non empty TopologicalGroup; func left_uniformity(TG) -> non empty UniformSpace equals :: UNIFORM3:def 8 UniformSpaceStr(# the carrier of TG, <. system_left_uniformity(TG) .] #); end; 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 is Element of G,y is Element of G: y * x" in U}; end; definition let TG be non empty TopologicalGroup; func system_right_uniformity(TG) -> non empty Subset-Family of [:the carrier of TG,the carrier of TG:] equals :: UNIFORM3:def 10 the set of all element_right_uniformity(U) where U is a_neighborhood of 1_TG; end; definition let TG be non empty TopologicalGroup; func right_uniformity(TG) -> non empty UniformSpace equals :: UNIFORM3:def 11 UniformSpaceStr(# the carrier of TG, <. system_right_uniformity(TG) .] #); end; theorem :: UNIFORM3:24 for TG being non empty commutative TopologicalGroup, U being a_neighborhood of 1_TG holds element_left_uniformity(U) = element_right_uniformity(U); theorem :: UNIFORM3:25 for TG being non empty commutative TopologicalGroup holds left_uniformity(TG) = right_uniformity(TG); 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 is Element of G,y is Element of G: (-x) + y in U}; end; definition let TG be non empty TopaddGroup; func system_left_uniformity(TG) -> non empty Subset-Family of [:the carrier of TG,the carrier of TG:] equals :: UNIFORM3:def 13 the set of all element_left_uniformity(U) where U is a_neighborhood of 0_TG; end; definition let TG be non empty TopologicaladdGroup; func left_uniformity(TG) -> non empty UniformSpace equals :: UNIFORM3:def 14 UniformSpaceStr(# the carrier of TG, <. system_left_uniformity(TG) .] #); end; 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 is Element of G,y is Element of G: y + (- x) in U}; end; definition let TG be non empty TopaddGroup; func system_right_uniformity(TG) -> non empty Subset-Family of [:the carrier of TG,the carrier of TG:] equals :: UNIFORM3:def 16 the set of all element_right_uniformity(U) where U is a_neighborhood of 0_TG; end; definition let TG be non empty TopologicaladdGroup; func right_uniformity(TG) -> non empty UniformSpace equals :: UNIFORM3:def 17 UniformSpaceStr(# the carrier of TG, <. system_right_uniformity(TG) .] #); end; theorem :: UNIFORM3:26 for TG being Abelian TopaddGroup, U being a_neighborhood of 0_TG holds element_left_uniformity(U) = element_right_uniformity(U); theorem :: UNIFORM3:27 for TG being non empty TopologicaladdGroup st TG is Abelian holds left_uniformity(TG) = right_uniformity(TG); theorem :: UNIFORM3:28 the topology of TopSpace_induced_by(left_uniformity(TG)) = the topology of TG ; theorem :: UNIFORM3:29 the topology of TopSpace_induced_by(right_uniformity(TG)) = the topology of TG; begin :: Function uniformly continuous definition let US1,US2 be UniformSpaceStr, f be Function of US1,US2; attr f is uniformly_continuous means :: UNIFORM3:def 18 for V being Element of the entourages of US2 holds 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; registration let US1, US2 be non empty axiom_U1 UniformSpaceStr; cluster uniformly_continuous for Function of US1,US2; end; begin :: Partition topology theorem :: UNIFORM3:30 the set of all union P where P is Subset of D = UniCl D; theorem :: UNIFORM3:31 X in UniCl D; theorem :: UNIFORM3:32 D = {} implies X is empty & UniCl D = {{}}; registration let X be set, D be a_partition of X; cluster UniCl D -> cap-closed; end; registration let X be set, D be a_partition of X; cluster UniCl D -> union-closed; end; registration let X be set; cluster union-closed -> cup-closed for Subset-Family of X; end; registration let X be set, D be a_partition of X; cluster UniCl D -> compl-closed; end; registration let X be set, D be a_partition of X; cluster UniCl D -> cup-closed diff-closed; end; theorem :: UNIFORM3:33 UniCl D is Ring_of_sets; registration let X, D; cluster UniCl D -> with_empty_element; end; registration let X be set,D be a_partition of X; cluster UniCl D -> non empty; end; theorem :: UNIFORM3:34 UniCl D is Field_Subset of X; registration let X be set,D be a_partition of X; cluster UniCl D -> sigma-additive; end; registration let X be set,D be a_partition of X; cluster UniCl D -> sigma-multiplicative; end; theorem :: UNIFORM3:35 UniCl D is SigmaField of X; registration let X be set,D be a_partition of X; cluster UniCl D -> closed_for_countable_unions closed_for_countable_meets; end; theorem :: UNIFORM3:36 for Omega being non empty set, D being a_partition of Omega holds UniCl D is Dynkin_System of Omega; definition let X be set,D be a_partition of X; func partition_topology(D) -> TopSpace equals :: UNIFORM3:def 19 TopStruct (# X,UniCl D #); end; theorem :: UNIFORM3:37 for O being open Subset of partition_topology(D) holds O is closed; theorem :: UNIFORM3:38 for O being closed Subset of partition_topology(D) holds O is open; theorem :: UNIFORM3:39 for S being Subset of partition_topology(D) holds S is open iff S is closed; registration let X be non empty set,D be a_partition of X; cluster partition_topology(D) -> non empty; end; theorem :: UNIFORM3:40 for X being non empty set,D being a_partition of X holds capOpCl partition_topology(D) = UniCl D; theorem :: UNIFORM3:41 for X being non empty set,D being a_partition of X holds OpenClosedSet(partition_topology(D)) = the topology of partition_topology(D); begin :: UniformSpace and partition topology reserve R for Relation of X; definition let X be set,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}; end; theorem :: UNIFORM3:42 <. rho(R).] = rho(R); theorem :: UNIFORM3:43 <. {R} .] = rho(R); theorem :: UNIFORM3:44 rho(R) is upper & rho(R) is cap-closed; registration let X,R; cluster rho(R) -> quasi_basis; end; theorem :: UNIFORM3:45 for R being total reflexive Relation of X holds rho(R) is axiom_UP1; theorem :: UNIFORM3:46 for R being symmetric Relation of X holds rho(R) is axiom_UP2; theorem :: UNIFORM3:47 for R being total transitive Relation of X holds rho(R) is axiom_UP3; definition let X be set, R be Relation of X; func uniformity_induced_by(R) -> upper cap-closed strict UniformSpaceStr equals :: UNIFORM3:def 21 UniformSpaceStr(# X,rho(R) #); end; theorem :: UNIFORM3:48 for X being set,R being total reflexive Relation of X holds uniformity_induced_by(R) is axiom_U1; theorem :: UNIFORM3:49 for X being set,R being symmetric Relation of X holds uniformity_induced_by(R) is axiom_U2; theorem :: UNIFORM3:50 for X being set, R being total transitive Relation of X holds uniformity_induced_by(R) is axiom_U3; definition let X be set, R be Tolerance of X; redefine func uniformity_induced_by(R) -> strict Semi-UniformSpace; end; theorem :: UNIFORM3:51 for X being set, R being Equivalence_Relation of X holds uniformity_induced_by(R) is UniformSpace; definition let X be set, R be Equivalence_Relation of X; redefine func uniformity_induced_by(R) -> strict UniformSpace; end; registration let X be non empty set, R be Tolerance of X; cluster uniformity_induced_by(R) -> non empty; end; registration cluster -> topological for non empty UniformSpace; end; definition let US be non empty UniformSpace; func @US -> topological non empty axiom_U1 UniformSpaceStr equals :: UNIFORM3:def 22 US; end; theorem :: UNIFORM3:52 for X being non empty set, R being Equivalence_Relation of X holds TopSpace_induced_by( @(uniformity_induced_by(R)) ) = partition_topology(Class R); begin :: Uniformity induced by a Tolerance or an Equivalence 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); definition let USS be UniformSpaceStr; func Uniformity2InternalRel(USS) -> Relation of the carrier of USS equals :: UNIFORM3:def 23 meet the entourages of USS; end; definition let USS be UniformSpaceStr; func UniformSpaceStr2RelStr(USS) -> RelStr equals :: UNIFORM3:def 24 RelStr(# the carrier of USS, Uniformity2InternalRel(USS) #); end; 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}; end; definition let RS be RelStr; func RelStr2UniformSpaceStr(RS) -> strict UniformSpaceStr equals :: UNIFORM3:def 26 UniformSpaceStr(# the carrier of RS, InternalRel2Uniformity RS #); end; definition let RS be RelStr; func InternalRel2Element(RS) -> Element of the entourages of RelStr2UniformSpaceStr(RS) equals :: UNIFORM3:def 27 the InternalRel of RS; end; theorem :: UNIFORM3:54 for R be Relation of X holds meet rho(R) = R; theorem :: UNIFORM3:55 for RS being strict RelStr holds UniformSpaceStr2RelStr(RelStr2UniformSpaceStr(RS)) = 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); theorem :: UNIFORM3:57 for SF being Subset-Family of [:X,X:],R being Relation of X st SF = rho(R) holds SF c= rho(meet SF); theorem :: UNIFORM3:58 for SF being upper Subset-Family of [:X,X:] st meet SF in SF holds rho(meet SF) c= SF; theorem :: UNIFORM3:59 for SF being upper Subset-Family of [:X,X:],R being Relation of X st R in SF & SF = rho(R) & meet SF in SF holds rho(meet SF) = SF; theorem :: 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); theorem :: UNIFORM3:61 for US being upper UniformSpaceStr, 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); theorem :: UNIFORM3:62 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; theorem :: UNIFORM3:63 for R being Tolerance of X holds RelStr2UniformSpaceStr(UniformSpaceStr2RelStr(uniformity_induced_by(R))) = uniformity_induced_by(R); theorem :: UNIFORM3:64 for R being Equivalence_Relation of X holds RelStr2UniformSpaceStr(UniformSpaceStr2RelStr(uniformity_induced_by(R))) = uniformity_induced_by(R); begin :: Uniform Pervin Space definition let X be set,SF be Subset-Family of X, A be Element of SF; func block_Pervin_uniformity(A) -> Subset of [:X,X:] equals :: UNIFORM3:def 28 [:X \ A,X \ A:] \/ [:A,A:]; end; reserve SF for Subset-Family of X, A for Element of SF; theorem :: UNIFORM3:65 A = {} implies block_Pervin_uniformity(A) = [:X,X:]; theorem :: UNIFORM3:66 X is non empty implies block_Pervin_uniformity(A) = {[x,y] where x,y is Element of X: x in A iff y in A}; theorem :: UNIFORM3:67 id X c= block_Pervin_uniformity(A) & block_Pervin_uniformity(A) * block_Pervin_uniformity(A) c= block_Pervin_uniformity(A); definition let X be set, SF be Subset-Family of X; func subbasis_Pervin_uniformity(SF) -> Subset-Family of [:X,X:] equals :: UNIFORM3:def 29 the set of all block_Pervin_uniformity(A) where A is Element of SF; end; registration let X be set, SF be Subset-Family of X; cluster subbasis_Pervin_uniformity(SF) -> non empty; end; definition let X be set, 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)); end; theorem :: UNIFORM3:68 basis_Pervin_uniformity(SF) is cap-closed; theorem :: UNIFORM3:69 basis_Pervin_uniformity(SF) is quasi_basis; theorem :: UNIFORM3:70 basis_Pervin_uniformity(SF) is axiom_UP1; theorem :: UNIFORM3:71 for A being Element of SF, R being Relation of X st R = block_Pervin_uniformity(A) holds R~ = block_Pervin_uniformity(A); theorem :: UNIFORM3:72 for R being Relation of X st R is Element of subbasis_Pervin_uniformity(SF) holds R~ is Element of subbasis_Pervin_uniformity(SF); theorem :: UNIFORM3:73 for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity(SF) holds Y[~] = Y; theorem :: UNIFORM3:74 for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity(SF) holds (meet Y)~ = meet (Y[~]); theorem :: UNIFORM3:75 for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity(SF) holds meet Y = (meet Y)~; theorem :: UNIFORM3:76 basis_Pervin_uniformity(SF) is axiom_UP2; theorem :: UNIFORM3:77 basis_Pervin_uniformity(SF) is axiom_UP3; definition let X be set, SF be Subset-Family of X; func Pervin_uniform_space SF -> strict UniformSpace equals :: UNIFORM3:def 31 UniformSpaceStr(# X, <.basis_Pervin_uniformity(SF).] #); end;