:: Uniform Space :: by Roland Coghetto :: :: Received June 30, 2016 :: Copyright (c) 2016-2019 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; definitions TARSKI, XBOOLE_0, UNIFORM2; equalities FINTOPO7, GROUP_1A, UNIFORM2, SRINGS_4, IDEAL_1, SUBSET_1, STRUCT_0, FINTOPO2, GROUP_2, PCOMPS_1, LOPCLSET; expansions CARDFIL2, TARSKI, XBOOLE_0, FINTOPO7, UNIFORM2, SETFAM_1, FINSUB_1, PRE_TOPC, ROUGHS_4, PROB_1, MEASURE1; theorems FUNCOP_1, CONNSP_2, GROUP_2, GROUP_3, SYSREL, ROUGHS_4, TARSKI, RELAT_1, XBOOLE_1, CARDFIL2, ZFMISC_1, XBOOLE_0, SETFAM_1, XTUPLE_0, XXREAL_0, XREAL_1, METRIC_1, FINSUB_1, SUBSET_1, FINTOPO7, TOPGRP_1, GROUP_1, PRE_TOPC, PCOMPS_1, GROUP_1A, RLVECT_1, UNIFORM2, EQREL_1, RELAT_2, ORDERS_1, YELLOW_9, COHSP_1, LATTICE7, CANTOR_1, PROB_1, TOPGEN_4, DYNKIN, CARD_3, MSSUBFAM, ENUMSET1; begin :: Preliminaries reserve X for set, D for a_partition of X, TG for non empty TopologicalGroup; reserve A for Subset of X; theorem [:A,A:] \/ [:X \ A,X \ A:] c= [:X \ A,X:] \/ [:X,A:] proof let x be object; assume x in [:A,A:] \/ [:X \ A,X \ A:]; then per cases by XBOOLE_0:def 3; suppose x in [:A,A:]; then consider y,z be object such that A1: y in A and A2: z in A and A3: x = [y,z] by ZFMISC_1:def 2; x in [:X \ A,X:] or x in [:X,A:] by A1,A2,A3,ZFMISC_1:87; hence thesis by XBOOLE_0:def 3; end; suppose x in [:X \ A, X \ A:]; then consider y,z be object such that A4: y in X \ A and A5: z in X \ A and A6: x = [y,z] by ZFMISC_1:def 2; x in [:X \ A,X:] or x in [:X,A:] by A4,A5,A6,ZFMISC_1:87; hence thesis by XBOOLE_0:def 3; end; end; theorem Th32: {1,2,3} \ {1} = {2,3} proof thus {1,2,3} \ {1} c= {2,3} proof let x be object; assume x in {1,2,3} \ {1}; then x in {1,2,3} & not x in {1} by XBOOLE_0:def 5; then (x = 1 or x = 2 or x = 3) & not x = 1 by ENUMSET1:def 1,TARSKI:def 1; hence thesis by TARSKI:def 2; end; let x be object; assume x in {2,3}; then x = 2 or x = 3 by TARSKI:def 2; then x in {1,2,3} & not x in {1} by ENUMSET1:def 1,TARSKI:def 1; hence thesis by XBOOLE_0:def 5; end; theorem 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:] proof assume that A1: X = {1,2,3} and A2: A = {1}; 1 in X & 2 in X \ A by A1,A2,Th32,TARSKI:def 2,ENUMSET1:def 1; then [2,1] in [:X \ A,X:] by ZFMISC_1:87; hence [2,1] in [:X \ A,X:] \/ [:X,A:] by XBOOLE_0:def 3; assume [2,1] in [:A,A:] \/ [:X\A,X\A:]; then [2,1] in [:A,A:] or [2,1] in [:X\A,X\A:] by XBOOLE_0:def 3; then 2 in {1} or 1 in {2,3} by A1,A2,Th32,ZFMISC_1:87; hence thesis by TARSKI:def 1,TARSKI:def 2; end; theorem Th33: for A being Subset of X holds ([:A,A:] \/ [:X \ A,X \ A:])~ = [:A,A:] \/ [:X \ A,X \ A:] proof let A be Subset of X; [:A,A:]~ = [:A,A:] & [:X\A,X\A:]~ = [:X\A,X\A:] by SYSREL:5; hence thesis by RELAT_1:23; end; Th1: for P1,P2 being Subset of D st union P1 = union P2 holds P1 c= P2 proof let P1,P2 be Subset of D; assume A1: union P1 = union P2; let x be object; assume A2: x in P1; assume A3: not x in P2; x in D by A2; then reconsider x as Subset of X; A4: x <> {} by A2,EQREL_1:def 4; set a = the Element of x; a in union P2 by A1,A2,A4,TARSKI:def 4; then consider y be set such that A5: a in y and A6: y in P2 by TARSKI:def 4; A7: not x misses y by A4,A5,XBOOLE_0:def 4; x in D & y in D by A2,A6; hence thesis by A3,A6,A7,EQREL_1:def 4; end; theorem for P1,P2 being Subset of D st union P1 = union P2 holds P1 = P2 by Th1; theorem Th2: :: EQREL_1:43 generalized for P being Subset of D holds union (D \ P) = union D \ union P proof let P be Subset of D; thus union (D \ P) c= union D \ union P proof let x be object; assume x in union (D\ P); then consider y be set such that A2: x in y and A3: y in D \ P by TARSKI:def 4; y in D & not y in P by A3,XBOOLE_0:def 5; then A4: x in union D by A2,TARSKI:def 4; not x in union P proof assume x in union P; then consider z be set such that A5: x in z and A6: z in P by TARSKI:def 4; z in D & y in D by A3,A6,XBOOLE_0:def 5; then y = z or y misses z by EQREL_1:def 4; hence thesis by A2,A5,A6,A3,XBOOLE_0:def 4,XBOOLE_0:def 5; end; hence thesis by A4,XBOOLE_0:def 5; end; let x be object; assume x in union D \ union P; then A7: x in union D & not x in union P by XBOOLE_0:def 5; then consider y be set such that A8: x in y and A9: y in D by TARSKI:def 4; y in D \ P proof assume not y in D \ P; then y in P or not y in D by XBOOLE_0:def 5; hence thesis by A7,A8,A9,TARSKI:def 4; end; hence thesis by A8,TARSKI:def 4; end; theorem for SF being upper Subset-Family of X, S being Element of SF holds meet SF c= S proof let SF be upper Subset-Family of X, S be Element of SF; let x be object; assume A1: x in meet SF; per cases; suppose SF is empty; hence thesis by A1,SETFAM_1:def 1; end; suppose SF is non empty; hence thesis by A1,SETFAM_1:def 1; end; end; theorem Th3: 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 proof let G be addGroup,A,B,C,D be Subset of G; assume that A1: A c= B and A2: C c= D; let x be object; assume x in A + C; then ex a,c be Element of G st x = a + c & a in A & c in C; hence thesis by A1,A2; end; theorem Th4: for e being Element of TG, V being a_neighborhood of 1_TG holds {e} * V is a_neighborhood of e proof let e be Element of TG, V be a_neighborhood of 1_TG; consider o be Subset of TG such that A1: o is open and A2: o c= V and A3: 1_TG in o by CONNSP_2:6; now thus e * o is open by A1; thus e * o c= {e} * V proof let x be object; assume A4: x in e * o; e * o c= e * V by A2,GROUP_3:5; hence thesis by A4; end; e = e * 1_TG by GROUP_1:def 4; hence e in e * o by A3,GROUP_2:27; end; hence thesis by CONNSP_2:6; end; theorem Th5: for e being Element of TG, V being a_neighborhood of 1_TG holds V * {e} is a_neighborhood of e proof let e be Element of TG, V be a_neighborhood of 1_TG; consider o be Subset of TG such that A1: o is open and A2: o c= V and A3: 1_TG in o by CONNSP_2:6; now thus o * e is open by A1; thus o * e c= V * {e} proof let x be object; assume A4: x in o * e; o * e c= V * e by A2,GROUP_3:5; hence thesis by A4; end; e = 1_TG * e by GROUP_1:def 4; hence e in o * e by A3,GROUP_2:28; end; hence thesis by CONNSP_2:6; end; theorem for V being a_neighborhood of 1_TG holds V" is a_neighborhood of 1_TG proof let V be a_neighborhood of 1_TG; V" is a_neighborhood of (1_TG)" by TOPGRP_1:54; hence thesis by GROUP_1:8; end; begin :: UniformSpace definition mode UniformSpace is upper cap-closed axiom_U1 axiom_U2 axiom_U3 UniformSpaceStr; end; reserve US for UniformSpace; theorem US is axiom_U2 Quasi-UniformSpace; theorem US is axiom_U3 Semi-UniformSpace; definition let X be set, cB be Subset-Family of [:X,X:]; attr cB is axiom_UP2 means for B1 being Element of cB holds ex B2 being Element of cB st B2 c= B1~; end; theorem 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 proof let X be empty set,cB be empty Subset-Family of [:X,X:]; for B1,B2 be Element of cB ex B be Element of cB st B c= B1 /\ B2 proof let B1,B2 be Element of cB; reconsider B = {} as Element of cB by SUBSET_1:def 1; take B; thus thesis; end; hence cB is quasi_basis; for B be Element of cB holds id X c= B; hence cB is axiom_UP1; for B1 be Element of cB holds ex B2 be Element of cB st B2 c= B1~ proof let B1 be Element of cB; reconsider B2 = {} as Element of cB by SUBSET_1:def 1; B2 c= B1~; hence thesis; end; hence cB is axiom_UP2; for B1 be Element of cB ex B2 be Element of cB st B2 * B2 c= B1 proof let B1 be Element of cB; reconsider B2 = {} as Element of cB by SUBSET_1:def 1; B2 * B2 c= B1; hence thesis; end; hence cB is axiom_UP3; end; registration cluster strict for UniformSpace; existence proof reconsider SF = {{}} as Subset-Family of [:{},{}:] by ZFMISC_1:1; set US = UniformSpaceStr (# {},SF #); now the entourages of US is upper; hence US is upper; the entourages of US is cap-closed; hence US is cap-closed; for S being Element of the entourages of US holds id the carrier of US c= S; hence US is axiom_U1; now let S be Element of the entourages of US; S[~] = {}; hence S~ in the entourages of US by TARSKI:def 1; end; hence US is axiom_U2; now let S be Element of the entourages of US; S [*] S = {}; then S * S = S by TARSKI:def 1; hence ex W being Element of the entourages of US st W * W c= S; end; hence US is axiom_U3; end; hence thesis; end; end; theorem Th6: for X being set, SF being Subset-Family of [:X,X:] st X = {{}} & SF = {[:X,X:]} holds UniformSpaceStr(# X,SF #) is UniformSpace proof set X = {{}}; reconsider SF = {[:X,X:]} as Subset-Family of [:X,X:] by ZFMISC_1:68; set US = UniformSpaceStr(# X,SF #); now for Y1,Y2 be Subset of [:the carrier of US,the carrier of US:] st Y1 in the entourages of US & Y1 c= Y2 holds Y2 in the entourages of US proof let Y1,Y2 be Subset of [:the carrier of US,the carrier of US:]; assume that A1: Y1 in the entourages of US and A2: Y1 c= Y2; A3: Y1 = [:X,X:] by A1,TARSKI:def 1; Y1 = Y2 by A2,A3; hence thesis by A1; end; then the entourages of US is upper; hence US is upper; for a,b be Subset of [:the carrier of US,the carrier of US:] st a in the entourages of US & b in the entourages of US holds a /\ b in the entourages of US proof let a,b be Subset of [:the carrier of US,the carrier of US:]; assume that A4: a in the entourages of US and A5: b in the entourages of US; a = [:X,X:] & b = [:X,X:] by A4,A5,TARSKI:def 1; hence a /\ b in the entourages of US by TARSKI:def 1; end; hence US is cap-closed by ROUGHS_4:def 2; for S being Element of the entourages of US holds id X c= S proof let S be Element of the entourages of US; S = [:X,X:] by TARSKI:def 1; hence thesis; end; hence US is axiom_U1; for S being Element of the entourages of US holds S[~] in the entourages of US proof let S be Element of the entourages of US; S = [:X,X:] by TARSKI:def 1; then S[~] = [:X,X:] by SYSREL:5; hence thesis by TARSKI:def 1; end; hence US is axiom_U2; for S being Element of the entourages of US holds ex W being Element of the entourages of US st W [*] W c= S proof let S be Element of the entourages of US; take S; S = [:X,X:] by TARSKI:def 1; hence thesis; end; hence US is axiom_U3; end; hence thesis; end; registration cluster non empty for strict UniformSpace; existence proof set X = {{}}; reconsider SF = {[:X,X:]} as Subset-Family of [:X,X:] by ZFMISC_1:68; set US = UniformSpaceStr(# X,SF #); A1: US is non empty; US is strict UniformSpace by Th6; hence thesis by A1; end; end; theorem Th7: 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.] proof let X be set,cB be Subset-Family of [:X,X:]; assume that A1: cB is quasi_basis and A2: cB is axiom_UP1 and A3: cB is axiom_UP2 and A4: cB is axiom_UP3; set US = UniformSpaceStr(# X,<.cB.] #); A5: <.cB.] = {x where x is Subset of [:X,X:]: ex b be Element of cB st b c= x} by CARDFIL2:14; now for Y1,Y2 being Subset of [:X,X:] st Y1 in <.cB.] & Y1 c= Y2 holds Y2 in <.cB.] proof let Y1,Y2 be Subset of [:X,X:]; assume that A6: Y1 in <.cB.] and A7: Y1 c= Y2; consider x be Subset of [:X,X:] such that A8: Y1 = x and A9: ex b be Element of cB st b c= x by A5,A6; consider B be Element of cB such that A10: B c= x by A9; B c= Y2 by A10,A8,A7; hence thesis by A5; end; then <.cB.] is upper; hence US is upper; for Y1,Y2 be set st Y1 in <.cB.] & Y2 in <.cB.] holds Y1 /\ Y2 in <.cB.] proof let Y1,Y2 be set; assume that A11: Y1 in <.cB.] and A12: Y2 in <.cB.]; consider x be Subset of [:X,X:] such that A13: Y1 = x and A14: ex b be Element of cB st b c= x by A5,A11; consider B1 be Element of cB such that A15: B1 c= x by A14; Y2 in {x where x is Subset of [:X,X:]: ex b be Element of cB st b c= x} by CARDFIL2:14,A12; then consider y be Subset of [:X,X:] such that A16: Y2 = y and A17: ex b be Element of cB st b c= y; consider B2 be Element of cB such that A18: B2 c= y by A17; A19: B1 /\ B2 c= Y1 /\ Y2 by A13,A15,A18,A16,XBOOLE_1:27; consider B3 be Element of cB such that A20: B3 c= B1 /\ B2 by A1; A21: Y1 /\ Y2 c= [:X,X:] /\ [:X,X:] by A11,A12,XBOOLE_1:27; B3 c= Y1 /\ Y2 by A20,A19; hence thesis by A5,A21; end; hence US is cap-closed by FINSUB_1:def 2; for S being Element of <.cB.] holds id X c= S proof let S be Element of <.cB.]; S in {x where x is Subset of [:X,X:]: ex b be Element of cB st b c= x} by A5; then consider x be Subset of [:X,X:] such that A22: S = x and A23: ex b be Element of cB st b c= x; consider B be Element of cB such that A24: B c= x by A23; id X c= B by A2; hence thesis by A24,A22; end; hence US is axiom_U1; for S being Element of <.cB.] holds S~ in <.cB.] proof let S be Element of <.cB.]; reconsider S1 = S as Subset of [:X,X:]; consider B be Element of cB such that A27: B c= S1 by CARDFIL2:def 8; A29: B~ c= S1~ by A27,SYSREL:11; consider B2 be Element of cB such that A30: B2 c= B~ by A3; B2 c= S1~ by A29,A30; hence thesis by CARDFIL2:def 8; end; hence US is axiom_U2; for S being Element of the entourages of US holds ex W being Element of the entourages of US st W * W c= S proof let S be Element of the entourages of US; S in <.cB.]; then consider B1 be Element of cB such that A31: B1 c= S by CARDFIL2:def 8; consider B2 be Element of cB such that A32: B2 * B2 c= B1 by A4; per cases; suppose A34: cB is empty; then A35: B2 = {} by SUBSET_1:def 1; {} c= [:X,X:]; then reconsider B2 as Element of the entourages of US by A35,A34,CARDFIL2:15; B2 [*] B2 c= S by A35; hence thesis; end; suppose A36: cB is non empty; cB c= <.cB.] by CARDFIL2:18; then reconsider W = B2 as Element of the entourages of US by A36; W [*] W c= S by A31,A32; hence thesis; end; end; hence US is axiom_U3; end; then reconsider US as strict UniformSpace; take US; thus the carrier of US = X; thus the entourages of US = <.cB.]; end; begin :: Open set and UniformSpace theorem 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: 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 proof let US be non empty UniformSpace, S be Subset of FMT_induced_by(US); hereby assume A1: S is open; hereby let x be Element of US; assume A2: x in S; reconsider x1 = x as Element of FMT_induced_by(US); U_FMT x1 = Neighborhood x by UNIFORM2:def 14; hence S in Neighborhood x by A1,A2; end; end; assume A3: for x being Element of US st x in S holds S in Neighborhood x; now let x be Element of FMT_induced_by(US); assume A4: x in S; consider y be Element of US such that A5: x = y and A6: U_FMT x = (Neighborhood(US)).y; U_FMT x = Neighborhood y by A6, UNIFORM2:def 14; hence S in U_FMT x by A3,A4,A5; end; hence S is open; end; theorem 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 Th9: 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)) proof let US be non empty UniformSpace, S be Subset of FMT_induced_by(US); thus S is open implies S in Family_open_set(FMT_induced_by(US)); assume S in Family_open_set(FMT_induced_by(US)); then ex O be open Subset of FMT_induced_by(US) st S = O; hence S is open; end; theorem 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 by Th8,Th9; 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 {[x,y] where x,y is Element of MS: dist(x,y) <= r}; coherence proof set S = {[x,y] where x,y is Element of MS: dist(x,y) <= r}; S c= [:the carrier of MS,the carrier of MS:] proof let t be object; assume t in S; then ex x,y be Element of MS st t = [x,y]& dist(x,y) <= r; hence thesis; end; hence thesis; end; end; registration let MS be non empty Reflexive MetrStruct, r be positive Real; cluster fundamental_element_of_entourages(MS,r) -> non empty; coherence proof the carrier of MS is non empty; then consider s be object such that A1: s in the carrier of MS; reconsider s as Element of MS by A1; dist(s,s) = 0 by METRIC_1:1; then [s,s] in fundamental_element_of_entourages(MS,r); hence thesis; 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 the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; coherence proof set SF = the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; SF c= bool [:the carrier of MS,the carrier of MS:] proof let t be object; assume t in SF; then consider r be positive Real such that A1: t = fundamental_element_of_entourages(MS,r); reconsider t1 = t as Subset of [:the carrier of MS,the carrier of MS:] by A1; t1 c= [:the carrier of MS,the carrier of MS:]; hence thesis; end; then reconsider SF as Subset-Family of [:the carrier of MS,the carrier of MS:]; fundamental_element_of_entourages(MS,1) in SF; hence thesis; end; end; definition let MS be non empty MetrStruct; func uniformity_induced_by MS -> UniformSpaceStr equals UniformSpaceStr(# the carrier of MS, <. fundamental_system_of_entourages(MS) .] #); coherence; end; Th10: for MS being PseudoMetricSpace holds ex US being strict UniformSpace st US = uniformity_induced_by MS proof let MS be PseudoMetricSpace; set US = uniformity_induced_by MS; set cB = fundamental_system_of_entourages(MS); now now let B1,B2 be Element of cB; B1 in the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; then consider r1 be positive Real such that A1: B1 = fundamental_element_of_entourages(MS,r1); B2 in the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; then consider r2 be positive Real such that A2: B2 = fundamental_element_of_entourages(MS,r2); reconsider r3 = min(r1,r2) as positive Real by XXREAL_0:def 9; set B3 = {[x,y] where x,y is Element of MS: dist(x,y) <= r3}; B3 = fundamental_element_of_entourages(MS,r3); then B3 in the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; then reconsider B3 = {[x,y] where x,y is Element of the carrier of MS: dist(x,y) <= r3} as Element of cB; B3 c= B1 /\ B2 proof let t be object; assume t in B3; then consider x,y be Element of MS such that A3: t = [x,y] and A4: dist(x,y) <= r3; r3 <= r1 by XXREAL_0:17; then dist(x,y) <= r1 by A4,XXREAL_0:2; then A5: t in B1 by A1,A3; r3 <= r2 by XXREAL_0:17; then dist(x,y) <= r2 by A4,XXREAL_0:2; then t in B2 by A3,A2; hence thesis by A5,XBOOLE_0:def 4; end; hence ex B be Element of cB st B c= B1 /\ B2; end; hence cB is quasi_basis; now let B be Element of cB; B in the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; then consider r be positive Real such that A6: B = fundamental_element_of_entourages(MS,r); now let t be object; assume A7: t in id the carrier of MS; then consider t1,t2 be object such that A8: t = [t1,t2] by RELAT_1:def 1; A9: t1 in the carrier of MS & t1 = t2 by A7,A8,RELAT_1:def 10; then reconsider t1,t2 as Element of MS; dist(t1,t1) <= r by METRIC_1:1; hence t in B by A9,A8,A6; end; hence id the carrier of MS c= B; end; hence cB is axiom_UP1; now let B1 be Element of cB; B1 in the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; then consider r be positive Real such that A10: B1 = fundamental_element_of_entourages(MS,r); B1 c= B1~ proof let t be object; assume A11: t in B1; then consider x,y be Element of MS such that A12: t = [x,y] and dist(x,y) <= r by A10; reconsider R1 = B1 as Relation of the carrier of MS; A13: R1~ = {[y,x] where x,y is Element of MS : dist(x,y) <= r} proof {[y,x] where x,y is Element of MS: dist(x,y) <= r} c= [:the carrier of MS,the carrier of MS:] proof let u be object; assume u in {[y,x] where x,y is Element of MS: dist(x,y) <= r}; then ex u1,u2 be Element of MS st u = [u2,u1] & dist(u1,u2) <= r; hence thesis; end; then reconsider R2 = {[y,x] where x,y is Element of the carrier of MS: dist(x,y) <= r} as Relation; A14: R1~ c= R2 proof let u be object; assume A15: u in R1~; consider u1,u2 be object such that A16: u = [u1,u2] by A15,RELAT_1:def 1; [u2,u1] in R1 by A15,A16,RELAT_1:def 7; then consider v1,v2 be Element of MS such that A17: [u2,u1] = [v1,v2] and A18: dist(v1,v2) <= r by A10; u2 = v1 & u1 = v2 by A17,XTUPLE_0:1; hence thesis by A16,A18; end; R2 c= R1~ proof let u be object; assume A19: u in R2; then consider u1,u2 be object such that A20: u = [u1,u2] by RELAT_1:def 1; consider v1,v2 be Element of MS such that A21: [u1,u2] = [v2,v1] and A22: dist(v1,v2) <= r by A19,A20; [v1,v2] in R1 by A10,A22; hence thesis by A20,A21,RELAT_1:def 7; end; hence thesis by A14; end; consider x1,y1 be Element of MS such that A23: [x,y] = [x1,y1] and A24: dist(x1,y1) <= r by A10,A11,A12; thus thesis by A24,A13,A12,A23; end; hence ex B2 being Element of cB st B2 c= B1~; end; hence cB is axiom_UP2; now let B1 be Element of cB; B1 in the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; then consider r be positive Real such that A25: B1 = fundamental_element_of_entourages(MS,r); set B2 = {[x,y] where x,y is Element of MS: dist(x,y) <= r/2}; reconsider r2 = r/2 as positive Real; B2 = fundamental_element_of_entourages(MS,r2); then B2 in cB; then reconsider B2 as Element of cB; reconsider R1 = B2 as Relation of the carrier of MS; B2 * B2 c= B1 proof let t be object; assume t in B2 * B2; then t in {[x,y] where x,y is Element of MS : ex z being Element of MS st [x,z] in R1 & [z,y] in R1} by UNIFORM2:3; then consider x,y be Element of MS such that A29: t = [x,y] and A30: ex z being Element of MS st [x,z] in R1 & [z,y] in R1; consider z be Element of MS such that A31: [x,z] in R1 and A32: [z,y] in R1 by A30; consider x1,z1 be Element of MS such that A33: [x,z] = [x1,z1] and A34: dist(x1,z1) <= r/2 by A31; A35: x = x1 & z = z1 by A33,XTUPLE_0:1; consider z1,y1 be Element of MS such that A36: [z,y] = [z1,y1] and A37: dist(z1,y1) <= r/2 by A32; A38: z = z1 & y = y1 by A36,XTUPLE_0:1; A39: dist(x,y) <= dist(x,z) + dist(z,y) by METRIC_1:4; A40: dist(x,z) + dist(z,y) <= dist(x,z) + r/2 by A38,A37,XREAL_1:6; dist(x,z) + r/2 <= r/2 + r/2 by A35,A34,XREAL_1:6; then dist(x,z) + dist(z,y) <= r by A40,XXREAL_0:2; then dist(x,y) <= r by A39,XXREAL_0:2; hence thesis by A29,A25; end; hence ex B2 being Element of cB st B2 * B2 c= B1; end; hence cB is axiom_UP3; end; then ex US be strict UniformSpace st the carrier of US = the carrier of MS & the entourages of US = <.cB.] by Th7; hence thesis; end; definition let MS be PseudoMetricSpace; func uniformity_induced_by(MS) -> non empty strict UniformSpace equals UniformSpaceStr(# the carrier of MS, <. fundamental_system_of_entourages(MS) .] #); coherence proof ex US being strict UniformSpace st US = uniformity_induced_by MS by Th10; hence thesis; end; end; theorem Th11: for MS being PseudoMetricSpace holds Family_open_set(FMT_induced_by(uniformity_induced_by(MS))) = Family_open_set MS proof let MS be PseudoMetricSpace; set X = Family_open_set(FMT_induced_by(uniformity_induced_by(MS))), Y = Family_open_set MS; thus X c= Y proof let t be object; assume A2: t in X; then reconsider t1 = t as Subset of FMT_induced_by(uniformity_induced_by(MS)); for x being Point of MS st x in t1 holds ex r being Real st r>0 & Ball(x,r) c= t1 proof let x be Point of MS; assume A3: x in t1; reconsider x1 = x as Element of uniformity_induced_by(MS); t1 in Neighborhood x1 by A3,A2,Th8,Th9; then consider V0 be Element of the entourages of uniformity_induced_by(MS) such that A4: t1 = Neighborhood(V0,x1); consider b be Element of fundamental_system_of_entourages(MS) such that A5: b c= V0 by CARDFIL2:def 8; b in the set of all fundamental_element_of_entourages(MS,r) where r is positive Real; then consider r0 be positive Real such that A6: b = fundamental_element_of_entourages(MS,r0); now take r0; thus r0 > 0; thus Ball(x,r0) c= t1 proof let u be object; assume A7: u in Ball(x,r0); then reconsider u1 = u as Element of MS; dist(x,u1) < r0 by A7,METRIC_1:11; then [x,u1] in b by A6; hence thesis by A4,A5; end; end; hence thesis; end; hence thesis by PCOMPS_1:def 4; end; let t be object; assume A8: t in Y; then reconsider t1 = t as Subset of MS; for x be Element of uniformity_induced_by(MS) st x in t1 holds t1 in Neighborhood x proof let x be Element of uniformity_induced_by(MS); assume A9: x in t1; reconsider x1 = x as Element of MS; consider r0 be Real such that A10: r0 > 0 and A11: Ball(x1,r0) c= t1 by A8,PCOMPS_1:def 4,A9; reconsider r1 = r0 / 2 as positive Real by A10; set V0 = fundamental_element_of_entourages(MS,r1); V0 in fundamental_system_of_entourages(MS); then reconsider V0 as Element of fundamental_system_of_entourages(MS); reconsider V1 = V0 \/ [:t1,t1:] as Subset of [:the carrier of MS,the carrier of MS:]; V0 c= V1 by XBOOLE_1:7; then reconsider V1 as Element of the entourages of uniformity_induced_by(MS) by CARDFIL2:def 8; set Z = {y where y is Element of uniformity_induced_by(MS): [x,y] in V1}; Z = t1 proof thus Z c= t1 proof let u be object; assume u in Z; then consider y0 be Element of uniformity_induced_by(MS) such that A13: u = y0 and A14: [x,y0] in V1; per cases by A14,XBOOLE_0:def 3; suppose [x,y0] in V0; then consider x2,y2 be Element of MS such that A15: [x,y0] = [x2,y2] and A16: dist(x2,y2) <= r1; r0 / 2 < r0 / 1 by A10,XREAL_1:76; then A17: dist(x2,y2) < r0 by A16,XXREAL_0:2; Ball(x2,r0) = Ball(x1,r0) by A15,XTUPLE_0:1; then y2 in t1 by A17,METRIC_1:11,A11; hence thesis by A13,A15,XTUPLE_0:1; end; suppose [x,y0] in [:t1,t1:]; then ex a,b be object st a in t1 & b in t1 & [x,y0] = [a,b] by ZFMISC_1:def 2; hence thesis by A13,XTUPLE_0:1; end; end; let v be object; assume A18: v in t1; then reconsider v1 = v as Element of uniformity_induced_by(MS); [x,v1] in [:t1,t1:] by A18,A9,ZFMISC_1:def 2; then [x,v1] in V1 by XBOOLE_0:def 3; hence thesis; end; then t1 = Neighborhood(V1,x); hence thesis; end; hence thesis by Th8,Th9; end; theorem for MS being PseudoMetricSpace holds TopSpace_induced_by(uniformity_induced_by(MS)) = TopSpaceMetr(MS) proof let MS be PseudoMetricSpace; the topology of FMT2TopSpace(FMT_induced_by(uniformity_induced_by(MS))) = Family_open_set(FMT_induced_by(uniformity_induced_by(MS))) by FINTOPO7:def 16; hence thesis by FINTOPO7:def 16,Th11; end; 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 {[x,y] where x is Element of G,y is Element of G: x" * y in U}; coherence proof set S = {[x,y] where x is Element of G,y is Element of G: x" * y in U}; S c= [:the carrier of G,the carrier of G:] proof let t be object; assume t in S; then ex x,y be Element of G st t = [x,y] & x" * y in U; hence thesis; end; hence thesis; end; 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 the set of all element_left_uniformity(U) where U is a_neighborhood of 1_TG; coherence proof set SF = the set of all element_left_uniformity(U) where U is a_neighborhood of 1_TG; reconsider nG = [#] TG as a_neighborhood of 1_TG by TOPGRP_1:21; A1: element_left_uniformity(nG) in SF; SF c= bool [:the carrier of TG,the carrier of TG:] proof let t be object; assume t in SF; then ex U be a_neighborhood of 1_TG st t = element_left_uniformity(U); hence thesis; end; hence thesis by A1; end; end; definition let TG be non empty TopologicalGroup; func left_uniformity(TG) -> non empty UniformSpace equals UniformSpaceStr(# the carrier of TG, <. system_left_uniformity(TG) .] #); coherence proof set cB = system_left_uniformity(TG); now now let B1,B2 be Element of cB; B1 in system_left_uniformity(TG); then consider U1 be a_neighborhood of 1_TG such that A1: B1 = element_left_uniformity(U1); B2 in system_left_uniformity(TG); then consider U2 be a_neighborhood of 1_TG such that A2: B2 = element_left_uniformity(U2); reconsider U3 = U1 /\ U2 as a_neighborhood of 1_TG by CONNSP_2:2; set B3 = element_left_uniformity(U3); B3 in cB; then reconsider B3 as Element of cB; B3 c= B1 /\ B2 proof let t be object; assume t in B3; then consider x,y be Element of TG such that A3: t = [x,y] and A4: x" * y in U3; x" * y in U1 & x" * y in U2 by A4,XBOOLE_0:def 4; then t in B1 & t in B2 by A3,A1,A2; hence thesis by XBOOLE_0:def 4; end; hence ex B3 be Element of cB st B3 c= B1 /\ B2; end; hence cB is quasi_basis; now let B be Element of cB; B in system_left_uniformity(TG); then consider U be a_neighborhood of 1_TG such that A5: B = element_left_uniformity(U); now let t be object; assume A6: t in id the carrier of TG; then consider x,y be object such that A7: x in the carrier of TG and A8: y in the carrier of TG and A9: t = [x,y] by ZFMISC_1:def 2; reconsider x,y as Element of TG by A7,A8; x = y by A6,A9,RELAT_1:def 10; then x" * y = 1_TG by GROUP_1:def 5; then x is Element of TG & y is Element of TG & x" * y in U by CONNSP_2:4; hence t in B by A5,A9; end; hence id the carrier of TG c= B; end; hence cB is axiom_UP1; now let B1 be Element of cB; B1 in system_left_uniformity(TG); then consider U be a_neighborhood of 1_TG such that A10: B1 = element_left_uniformity(U); consider R1 be Relation of the carrier of TG such that A11: B1 = R1 and A12: R1~ = B1~; U" is a_neighborhood of (1_TG)" by TOPGRP_1:54; then reconsider U2 = U" as a_neighborhood of 1_TG by GROUP_1:8; set B2 = element_left_uniformity(U2); B2 in cB; then reconsider B2 as Element of cB; B2 c= B1~ proof let t be object; assume t in B2; then consider a,b be Element of TG such that A13: t = [a,b] and A14: a" * b in U2; consider g be Element of TG such that A15: (a" * b) = g" and A16: g in U by A14; (a" * b)" in U by A15,A16; then b" * (a")" in U by GROUP_1:17; then [b,a] in R1 by A10,A11; hence thesis by A12,A13,RELAT_1:def 7; end; hence ex B2 be Element of cB st B2 c= B1~; end; hence cB is axiom_UP2; now let B1 be Element of cB; B1 in system_left_uniformity(TG); then consider U be a_neighborhood of 1_TG such that A17: B1 = element_left_uniformity(U); U is a_neighborhood of 1_TG * 1_TG by GROUP_1:def 4; then consider A be open a_neighborhood of 1_TG, B be open a_neighborhood of 1_TG such that A17bis: A * B c= U by TOPGRP_1:37; reconsider AB = A /\ B as a_neighborhood of 1_TG by CONNSP_2:2; AB c= A & AB c= B by XBOOLE_1:17; then A18: AB * AB c= A * B by GROUP_3:4; set B2 = element_left_uniformity(AB); B2 in cB; then reconsider B2 as Element of cB; B2 * B2 c= B1 proof let t be object; assume A19: t in B2 * B2; reconsider R1 = B2 as Relation of the carrier of TG; t in {[x,y] where x,y is Element of TG : ex z being Element of TG st [x,z] in R1 & [z,y] in R1} by A19,UNIFORM2:3; then consider x,y be Element of TG such that A23: t = [x,y] and A24: ex z be Element of TG st [x,z] in R1 & [z,y] in R1; consider z be Element of TG such that A25: [x,z] in R1 and A26: [z,y] in R1 by A24; consider a,b be Element of TG such that A27: [x,z] = [a,b] and A28: a" * b in AB by A25; A29: x = a & z = b by A27,XTUPLE_0:1; consider c,d be Element of TG such that A30: [z,y] = [c,d] and A31: c" * d in AB by A26; A32: z = c & y = d by A30,XTUPLE_0:1; A33: (a" * b) * (c" *d) = x" * (z * (z" * y)) by A29,A32,GROUP_1:def 3 .= x" * ((z * z") * y) by GROUP_1:def 3 .= x" * (1_TG * y) by GROUP_1:def 5 .= x" * y by GROUP_1:def 4; (a" * b) * (c" * d) in AB * AB by A31,A28; then x" * y in U by A18,A33,A17bis; hence t in B1 by A17,A23; end; hence ex B2 be Element of cB st B2 * B2 c= B1; end; hence cB is axiom_UP3; end; then ex US being strict UniformSpace st the carrier of US = the carrier of TG & the entourages of US = <.cB.] by Th7; hence thesis; end; 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 {[x,y] where x is Element of G,y is Element of G: y * x" in U}; coherence proof set S = {[x,y] where x is Element of G,y is Element of G: y * x" in U}; S c= [:the carrier of G,the carrier of G:] proof let t be object; assume t in S; then ex x,y be Element of G st t = [x,y] & y * x" in U; hence thesis; end; hence thesis; end; 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 the set of all element_right_uniformity(U) where U is a_neighborhood of 1_TG; coherence proof set SF = the set of all element_right_uniformity(U) where U is a_neighborhood of 1_TG; reconsider nG = [#] TG as a_neighborhood of 1_TG by TOPGRP_1:21; A1: element_right_uniformity(nG) in SF; SF c= bool [:the carrier of TG,the carrier of TG:] proof let t be object; assume t in SF; then ex U be a_neighborhood of 1_TG st t = element_right_uniformity(U); hence thesis; end; hence thesis by A1; end; end; definition let TG be non empty TopologicalGroup; func right_uniformity(TG) -> non empty UniformSpace equals UniformSpaceStr(# the carrier of TG, <. system_right_uniformity(TG) .] #); coherence proof set cB = system_right_uniformity(TG); now now let B1,B2 be Element of cB; B1 in system_right_uniformity(TG); then consider U1 be a_neighborhood of 1_TG such that A1: B1 = element_right_uniformity(U1); B2 in system_right_uniformity(TG); then consider U2 be a_neighborhood of 1_TG such that A2: B2 = element_right_uniformity(U2); reconsider U3 = U1 /\ U2 as a_neighborhood of 1_TG by CONNSP_2:2; set B3 = element_right_uniformity(U3); B3 in cB; then reconsider B3 as Element of cB; B3 c= B1 /\ B2 proof let t be object; assume t in B3; then consider x,y be Element of TG such that A3: t = [x,y ] and A4: y * x" in U3; y * x" in U1 & y * x" in U2 by A4,XBOOLE_0:def 4; then t in B1 & t in B2 by A3,A1,A2; hence thesis by XBOOLE_0:def 4; end; hence ex B3 be Element of cB st B3 c= B1 /\ B2; end; hence cB is quasi_basis; now let B be Element of cB; B in system_right_uniformity(TG); then consider U be a_neighborhood of 1_TG such that A5: B = element_right_uniformity(U); now let t be object; assume A6: t in id the carrier of TG; then consider x,y be object such that A7: x in the carrier of TG and A8: y in the carrier of TG and A9: t = [x,y] by ZFMISC_1:def 2; reconsider x,y as Element of TG by A7,A8; x = y by A6,A9,RELAT_1:def 10; then y * x" = 1_TG by GROUP_1:def 5; then x is Element of TG & y is Element of TG & y * x" in U by CONNSP_2:4; hence t in B by A5,A9; end; hence id the carrier of TG c= B; end; hence cB is axiom_UP1; now let B1 be Element of cB; B1 in system_right_uniformity(TG); then consider U be a_neighborhood of 1_TG such that A10: B1 = element_right_uniformity(U); consider R1 be Relation of the carrier of TG such that A11: B1 = R1 and A12: R1~ = B1~; U" is a_neighborhood of (1_TG)" by TOPGRP_1:54; then reconsider U2 = U" as a_neighborhood of 1_TG by GROUP_1:8; set B2 = element_right_uniformity(U2); B2 in cB; then reconsider B2 as Element of cB; B2 c= B1~ proof let t be object; assume t in B2; then consider a,b be Element of TG such that A13: t = [a,b] and A14: b * a" in U2; consider g be Element of TG such that A15: (b * a") = g" and A16: g in U by A14; (b * a")" in U by A15,A16; then (a")" * b" in U by GROUP_1:17; then [b,a] in R1 by A10,A11; hence thesis by A12,A13,RELAT_1:def 7; end; hence ex B2 be Element of cB st B2 c= B1~; end; hence cB is axiom_UP2; now let B1 be Element of cB; B1 in system_right_uniformity(TG); then consider U be a_neighborhood of 1_TG such that A17: B1 = element_right_uniformity(U); U is a_neighborhood of 1_TG * 1_TG by GROUP_1:def 4; then consider A be open a_neighborhood of 1_TG, B be open a_neighborhood of 1_TG such that A17bis: A * B c= U by TOPGRP_1:37; reconsider AB = A /\ B as a_neighborhood of 1_TG by CONNSP_2:2; AB c= A & AB c= B by XBOOLE_1:17; then A18: AB * AB c= A * B by GROUP_3:4; set B2 = element_right_uniformity(AB); B2 in cB; then reconsider B2 as Element of cB; B2 * B2 c= B1 proof let t be object; assume A19: t in B2 * B2; consider R1,R2 be Relation of the carrier of TG such that A20: R1 = B2 and R2 = B2 and B2 * B2 = R1 * R2; t in {[x,y] where x,y is Element of TG : ex z being Element of TG st [x,z] in R1 & [z,y] in R1} by A19,A20,UNIFORM2:3; then consider x,y be Element of TG such that A23: t = [x,y] and A24: ex z be Element of TG st [x,z] in R1 & [z,y] in R1; consider z be Element of TG such that A25: [x,z] in R1 and A26: [z,y] in R1 by A24; consider a,b be Element of TG such that A27: [x,z] = [a,b] and A28: b * a" in AB by A20,A25; A29: x = a & z = b by A27,XTUPLE_0:1; consider c,d be Element of TG such that A30: [z,y] = [c,d] and A31: d * c" in AB by A26,A20; A32: z = c & y = d by A30,XTUPLE_0:1; A33: (d * c") * (b * a") = y * (z" * (z * x")) by A29,A32,GROUP_1:def 3 .= y * ((z" * z) * x") by GROUP_1:def 3 .= y * (1_TG * x") by GROUP_1:def 5 .= y * x" by GROUP_1:def 4; (d * c") * (b * a") in AB * AB by A31,A28; then y * x" in U by A18,A33,A17bis; hence t in B1 by A17,A23; end; hence ex B2 be Element of cB st B2 * B2 c= B1; end; hence cB is axiom_UP3; end; then ex US being strict UniformSpace st the carrier of US = the carrier of TG & the entourages of US = <.cB.] by Th7; hence thesis; end; end; theorem Th12: for TG being non empty commutative TopologicalGroup, U being a_neighborhood of 1_TG holds element_left_uniformity(U) = element_right_uniformity(U) proof let TG be non empty commutative TopologicalGroup, U be a_neighborhood of 1_TG; now thus element_left_uniformity(U) c= element_right_uniformity(U) proof let x be object; assume x in element_left_uniformity(U); then consider u,v be Element of TG such that A1: x = [u,v] and A2: u" * v in U; v * u" in U by A2,GROUP_1:def 12; hence thesis by A1; end; thus element_right_uniformity(U) c= element_left_uniformity(U) proof let x be object; assume x in element_right_uniformity(U); then consider u,v be Element of TG such that A3: x = [u,v] and A4: v * u" in U; u" * v in U by A4,GROUP_1:def 12; hence thesis by A3; end; end; hence thesis; end; theorem for TG being non empty commutative TopologicalGroup holds left_uniformity(TG) = right_uniformity(TG) proof let TG be non empty commutative TopologicalGroup; set X = the set of all element_left_uniformity(U) where U is a_neighborhood of 1_TG; set Y = the set of all element_right_uniformity(U) where U is a_neighborhood of 1_TG; now thus X c= Y proof let x be object; assume x in X; then consider U be a_neighborhood of 1_TG such that A1: x = element_left_uniformity(U); x = element_right_uniformity(U) by A1,Th12; hence thesis; end; thus Y c= X proof let x be object; assume x in Y; then consider U be a_neighborhood of 1_TG such that A2: x = element_right_uniformity(U); x = element_left_uniformity(U) by A2,Th12; hence thesis; end; end; then system_left_uniformity(TG) = system_right_uniformity(TG); hence thesis; 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 {[x,y] where x is Element of G,y is Element of G: (-x) + y in U}; coherence proof set S = {[x,y] where x is Element of G,y is Element of G: (-x) + y in U}; S c= [:the carrier of G,the carrier of G:] proof let t be object; assume t in S; then ex x,y be Element of G st t = [x,y] & (-x) + y in U; hence thesis; end; hence thesis; end; 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 the set of all element_left_uniformity(U) where U is a_neighborhood of 0_TG; coherence proof set SF = the set of all element_left_uniformity(U) where U is a_neighborhood of 0_TG; reconsider nG = [#] TG as a_neighborhood of 0_TG by TOPGRP_1:21; A1: element_left_uniformity(nG) in SF; SF c= bool [:the carrier of TG,the carrier of TG:] proof let t be object; assume t in SF; then ex U be a_neighborhood of 0_TG st t = element_left_uniformity(U); hence thesis; end; hence thesis by A1; end; end; definition let TG be non empty TopologicaladdGroup; func left_uniformity(TG) -> non empty UniformSpace equals UniformSpaceStr(# the carrier of TG, <. system_left_uniformity(TG) .] #); coherence proof set cB = system_left_uniformity(TG); now now let B1,B2 be Element of cB; B1 in system_left_uniformity(TG); then consider U1 be a_neighborhood of 0_TG such that A1: B1 = element_left_uniformity(U1); B2 in system_left_uniformity(TG); then consider U2 be a_neighborhood of 0_TG such that A2: B2 = element_left_uniformity(U2); reconsider U3 = U1 /\ U2 as a_neighborhood of 0_TG by CONNSP_2:2; set B3 = element_left_uniformity(U3); B3 in cB; then reconsider B3 as Element of cB; B3 c= B1 /\ B2 proof let t be object; assume t in B3; then consider x,y be Element of TG such that A3: t = [x,y] and A4: (-x) + y in U3; (-x) + y in U1 & (-x) + y in U2 by A4,XBOOLE_0:def 4; then t in B1 & t in B2 by A3,A1,A2; hence thesis by XBOOLE_0:def 4; end; hence ex B3 be Element of cB st B3 c= B1 /\ B2; end; hence cB is quasi_basis; now let B be Element of cB; B in system_left_uniformity(TG); then consider U be a_neighborhood of 0_TG such that A5: B = element_left_uniformity(U); now let t be object; assume A6: t in id the carrier of TG; then consider x,y be object such that A7: x in the carrier of TG and A8: y in the carrier of TG and A9: t = [x,y] by ZFMISC_1:def 2; reconsider x,y as Element of TG by A7,A8; x = y by A6,A9,RELAT_1:def 10; then (-x) + y = 0_TG by GROUP_1A:def 4; then x is Element of TG & y is Element of TG & (-x) + y in U by CONNSP_2:4; hence t in B by A5,A9; end; hence id the carrier of TG c= B; end; hence cB is axiom_UP1; now let B1 be Element of cB; B1 in system_left_uniformity(TG); then consider U be a_neighborhood of 0_TG such that A10: B1 = element_left_uniformity(U); consider R1 be Relation of the carrier of TG such that A11: B1 = R1 and A12: R1~ = B1~; -U is a_neighborhood of -(0_TG) by GROUP_1A:371; then reconsider U2 = -U as a_neighborhood of 0_TG by GROUP_1A:8; set B2 = element_left_uniformity(U2); B2 in cB; then reconsider B2 as Element of cB; B2 c= B1~ proof let t be object; assume t in B2; then consider a,b be Element of TG such that A13: t = [a,b] and A14: (-a) + b in U2; consider g be Element of TG such that A15: ((-a) + b) = -g and A16: g in U by A14; -((-a) + b) in U by A15,A16; then (-b) + (-(-a)) in U by GROUP_1A:16; then [b,a] in R1 by A10,A11; hence thesis by A12,A13,RELAT_1:def 7; end; hence ex B2 be Element of cB st B2 c= B1~; end; hence cB is axiom_UP2; now let B1 be Element of cB; B1 in system_left_uniformity(TG); then consider U be a_neighborhood of 0_TG such that A17: B1 = element_left_uniformity(U); U is a_neighborhood of 0_TG + 0_TG by GROUP_1A:def 3; then consider A be open a_neighborhood of 0_TG, B be open a_neighborhood of 0_TG such that A17bis: A + B c= U by GROUP_1A:354; reconsider AB = A /\ B as a_neighborhood of 0_TG by CONNSP_2:2; AB c= A & AB c= B by XBOOLE_1:17; then A18: AB + AB c= A + B by Th3; set B2 = element_left_uniformity(AB); B2 in cB; then reconsider B2 as Element of cB; B2 * B2 c= B1 proof let t be object; assume A19: t in B2 * B2; consider R1,R2 be Relation of the carrier of TG such that A20: R1 = B2 and R2 = B2 and B2 * B2 = R1 * R2; t in {[x,y] where x,y is Element of TG : ex z being Element of TG st [x,z] in R1 & [z,y] in R1} by A19,A20,UNIFORM2:3; then consider x,y be Element of TG such that A23: t = [x,y] and A24: ex z be Element of TG st [x,z] in R1 & [z,y] in R1; consider z be Element of TG such that A25: [x,z] in R1 and A26: [z,y] in R1 by A24; consider a,b be Element of TG such that A27: [x,z] = [a,b] and A28: (-a) + b in AB by A20,A25; A29: x = a & z = b by A27,XTUPLE_0:1; consider c,d be Element of TG such that A30: [z,y] = [c,d] and A31: (-c) + d in AB by A26,A20; A32: z = c & y = d by A30,XTUPLE_0:1; A33: ((-a) + b) + ((-c) + d) = (-x) + (z + ((-z) + y)) by A29,A32,RLVECT_1:def 3 .= (-x) + ((z + (-z)) + y) by RLVECT_1:def 3 .= (-x) + (0_TG + y) by GROUP_1A:def 4 .= (-x) + y by GROUP_1A:def 3; ((-a) + b) + ((-c) + d) in AB + AB by A28,A31; then (-x) + y in U by A18,A33,A17bis; hence t in B1 by A17,A23; end; hence ex B2 be Element of cB st B2 * B2 c= B1; end; hence cB is axiom_UP3; end; then ex US being strict UniformSpace st the carrier of US = the carrier of TG & the entourages of US = <.cB.] by Th7; hence thesis; end; 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 {[x,y] where x is Element of G,y is Element of G: y + (- x) in U}; coherence proof set S = {[x,y] where x is Element of G,y is Element of G: y + (- x) in U}; S c= [:the carrier of G,the carrier of G:] proof let t be object; assume t in S; then ex x,y be Element of G st t = [x,y] & y + (- x) in U; hence thesis; end; hence thesis; end; 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 the set of all element_right_uniformity(U) where U is a_neighborhood of 0_TG; coherence proof set SF = the set of all element_right_uniformity(U) where U is a_neighborhood of 0_TG; reconsider nG = [#] TG as a_neighborhood of 0_TG by TOPGRP_1:21; A1: element_right_uniformity(nG) in SF; SF c= bool [:the carrier of TG,the carrier of TG:] proof let t be object; assume t in SF; then ex U be a_neighborhood of 0_TG st t = element_right_uniformity(U); hence thesis; end; hence thesis by A1; end; end; definition let TG be non empty TopologicaladdGroup; func right_uniformity(TG) -> non empty UniformSpace equals UniformSpaceStr(# the carrier of TG, <. system_right_uniformity(TG) .] #); coherence proof set cB = system_right_uniformity(TG); now now let B1,B2 be Element of cB; B1 in system_right_uniformity(TG); then consider U1 be a_neighborhood of 0_TG such that A1: B1 = element_right_uniformity(U1); B2 in system_right_uniformity(TG); then consider U2 be a_neighborhood of 0_TG such that A2: B2 = element_right_uniformity(U2); reconsider U3 = U1 /\ U2 as a_neighborhood of 0_TG by CONNSP_2:2; set B3 = element_right_uniformity(U3); B3 in cB; then reconsider B3 as Element of cB; B3 c= B1 /\ B2 proof let t be object; assume t in B3; then consider x,y be Element of TG such that A3: t = [x,y ] and A4: y + (-x) in U3; y + (-x) in U1 & y + (- x) in U2 by A4,XBOOLE_0:def 4; then t in B1 & t in B2 by A3,A1,A2; hence thesis by XBOOLE_0:def 4; end; hence ex B3 be Element of cB st B3 c= B1 /\ B2; end; hence cB is quasi_basis; now let B be Element of cB; B in system_right_uniformity(TG); then consider U be a_neighborhood of 0_TG such that A5: B = element_right_uniformity(U); now let t be object; assume A6: t in id the carrier of TG; then consider x,y be object such that A7: x in the carrier of TG and A8: y in the carrier of TG and A9: t = [x,y] by ZFMISC_1:def 2; reconsider x,y as Element of TG by A7,A8; x = y by A6,A9,RELAT_1:def 10; then y + (-x) = 0_TG by GROUP_1A:def 4; then x is Element of TG & y is Element of TG & y + (-x) in U by CONNSP_2:4; hence t in B by A5,A9; end; hence id the carrier of TG c= B; end; hence cB is axiom_UP1; now let B1 be Element of cB; B1 in system_right_uniformity(TG); then consider U be a_neighborhood of 0_TG such that A10: B1 = element_right_uniformity(U); consider R1 be Relation of the carrier of TG such that A11: B1 = R1 and A12: R1~ = B1~; -U is a_neighborhood of -(0_TG) by GROUP_1A:371; then reconsider U2 = -U as a_neighborhood of 0_TG by GROUP_1A:8; set B2 = element_right_uniformity(U2); B2 in cB; then reconsider B2 as Element of cB; B2 c= B1~ proof let t be object; assume t in B2; then consider a,b be Element of TG such that A13: t = [a,b] and A14: b + (- a) in U2; consider g be Element of TG such that A15: (b + (- a)) = -g and A16: g in U by A14; -(b + (- a)) in U by A15,A16; then (-(-a)) + (-b) in U by GROUP_1A:16; then [b,a] in R1 by A10,A11; hence thesis by A12,A13,RELAT_1:def 7; end; hence ex B2 be Element of cB st B2 c= B1~; end; hence cB is axiom_UP2; now let B1 be Element of cB; B1 in system_right_uniformity(TG); then consider U be a_neighborhood of 0_TG such that A17: B1 = element_right_uniformity(U); U is a_neighborhood of 0_TG + 0_TG by GROUP_1A:def 3; then consider A be open a_neighborhood of 0_TG, B be open a_neighborhood of 0_TG such that A17bis: A + B c= U by GROUP_1A:354; reconsider AB = A /\ B as a_neighborhood of 0_TG by CONNSP_2:2; AB c= A & AB c= B by XBOOLE_1:17; then A18: AB + AB c= A + B by Th3; set B2 = element_right_uniformity(AB); B2 in cB; then reconsider B2 as Element of cB; B2 * B2 c= B1 proof let t be object; assume A19: t in B2 * B2; consider R1,R2 be Relation of the carrier of TG such that A20: R1 = B2 and R2 = B2 and B2 * B2 = R1 * R2; t in {[x,y] where x,y is Element of TG : ex z being Element of TG st [x,z] in R1 & [z,y] in R1} by A19,A20,UNIFORM2:3; then consider x,y be Element of TG such that A23: t = [x,y] and A24: ex z be Element of TG st [x,z] in R1 & [z,y] in R1; consider z be Element of TG such that A25: [x,z] in R1 and A26: [z,y] in R1 by A24; consider a,b be Element of TG such that A27: [x,z] = [a,b] and A28: b + (- a) in AB by A20,A25; A29: x = a & z = b by A27,XTUPLE_0:1; consider c,d be Element of TG such that A30: [z,y] = [c,d] and A31: d + (- c) in AB by A26,A20; A32: z = c & y = d by A30,XTUPLE_0:1; A33: (d + (-c)) + (b + (-a)) = y + ( -z + (z + (-x))) by A29,A32,RLVECT_1:def 3 .= y + (((-z) + z) + (-x)) by RLVECT_1:def 3 .= y + (0_TG + (-x)) by GROUP_1A:def 4 .= y + (-x) by GROUP_1A:def 3; (d + (-c)) + (b + (-a)) in AB + AB by A28,A31; then y + (-x) in U by A18,A33,A17bis; hence t in B1 by A17,A23; end; hence ex B2 be Element of cB st B2 * B2 c= B1; end; hence cB is axiom_UP3; end; then ex US being strict UniformSpace st the carrier of US = the carrier of TG & the entourages of US = <.cB.] by Th7; hence thesis; end; end; theorem Th13: for TG being Abelian TopaddGroup, U being a_neighborhood of 0_TG holds element_left_uniformity(U) = element_right_uniformity(U) proof let TG be Abelian TopaddGroup, U be a_neighborhood of 0_TG; now thus element_left_uniformity(U) c= element_right_uniformity(U) proof let x be object; assume x in element_left_uniformity(U); then ex u,v be Element of TG st x = [u,v] & (-u) + v in U; hence thesis; end; thus element_right_uniformity(U) c= element_left_uniformity(U) proof let x be object; assume x in element_right_uniformity(U); then ex u,v be Element of TG st x = [u,v] & v + (-u) in U; hence thesis; end; end; hence thesis; end; theorem for TG being non empty TopologicaladdGroup st TG is Abelian holds left_uniformity(TG) = right_uniformity(TG) proof let TG be non empty TopologicaladdGroup; assume A1: TG is Abelian; set X = the set of all element_left_uniformity(U) where U is a_neighborhood of 0_TG; set Y = the set of all element_right_uniformity(U) where U is a_neighborhood of 0_TG; now thus X c= Y proof let x be object; assume x in X; then consider U be a_neighborhood of 0_TG such that A2: x = element_left_uniformity(U); x = element_right_uniformity(U) by A1,A2,Th13; hence thesis; end; thus Y c= X proof let x be object; assume x in Y; then consider U be a_neighborhood of 0_TG such that A3: x = element_right_uniformity(U); x = element_left_uniformity(U) by A1,A3,Th13; hence thesis; end; end; then system_left_uniformity(TG) = system_right_uniformity(TG); hence thesis; end; theorem the topology of TopSpace_induced_by(left_uniformity(TG)) = the topology of TG proof set X = the topology of FMT2TopSpace(FMT_induced_by(left_uniformity(TG))), Y = the topology of TG; A2: X c= Y proof let x be object; assume x in X; then x in Family_open_set(FMT_induced_by(left_uniformity(TG))) by FINTOPO7:def 16; then consider y be open Subset of FMT_induced_by(left_uniformity(TG)) such that A3: x = y; reconsider z = x as Subset of TG by A3; z is open proof now let t be Point of TG; assume A4: t in z; reconsider t1 = t as Point of FMT_induced_by(left_uniformity(TG)); A5: y in U_FMT t1 by A3,A4,FINTOPO7:def 1; reconsider t2 = t1 as Element of left_uniformity(TG); z in Neighborhood t2 by A3,A5,UNIFORM2:def 14; then consider V0 be Element of the entourages of (left_uniformity(TG)) such that A6: z = Neighborhood(V0,t2); consider tg be Element of system_left_uniformity(TG) such that A7: tg c= V0 by CARDFIL2:def 8; tg in the set of all element_left_uniformity(U) where U is a_neighborhood of 1_TG; then consider U0 be a_neighborhood of 1_TG such that A8: tg = element_left_uniformity(U0); reconsider A = {t} * U0 as a_neighborhood of t by Th4; A c= z proof let u be object; assume u in A; then consider u0,u1 be Element of TG such that A9: u = u0 * u1 and A10: u0 in {t} and A11: u1 in U0; reconsider u2 = u as Element of TG by A9; 1_TG * u1 in U0 by A11,GROUP_1:def 4; then (t" * t) * u1 in U0 by GROUP_1:def 5; then t" * (t * u1) in U0 by GROUP_1:def 3; then t" * u2 in U0 by A9,A10,TARSKI:def 1; then [t,u2] in element_left_uniformity(U0); hence thesis by A6,A7,A8; end; hence ex A be Subset of TG st A is a_neighborhood of t & A c= z; end; hence thesis by CONNSP_2:7; end; hence x in Y; end; Y c= X proof let u be object; assume A12: u in Y; then reconsider u as Subset of TG; reconsider v = u as Subset of FMT_induced_by(left_uniformity(TG)); for x being Element of FMT_induced_by(left_uniformity(TG)) st x in v holds v in U_FMT x proof let x be Element of FMT_induced_by(left_uniformity(TG)); assume A13: x in v; reconsider t2 = x as Element of left_uniformity(TG); reconsider t3 = x as Element of TG; reconsider w = v as Subset of TG; now {t3"} = {t3}" by GROUP_2:3; then t3" in {t3}" by TARSKI:def 1; then t3" * t3 in {t3}" * w by A13; hence 1_TG in {t3}" * w by GROUP_1:def 5; w is open by A12; hence {t3}" * w is open; end; then reconsider U0 = {t3}" * w as a_neighborhood of 1_TG by CONNSP_2:6; element_left_uniformity(U0) in system_left_uniformity(TG); then reconsider V0 = element_left_uniformity(U0) as Element of the entourages of left_uniformity(TG) by CARDFIL2:def 8; v = {y where y is Element of TG: [t2,y] in V0} proof set v2 = {y where y is Element of TG: [t2,y] in V0}; A15: v c= v2 proof let t be object; assume A16: t in v; then reconsider t4 = t as Element of TG; {t3"} = {t3}" by GROUP_2:3; then A17: t3" in {t3}" by TARSKI:def 1; t3" * t4 in {t3}" * w by A16,A17; then [t2,t4] in element_left_uniformity(U0); hence thesis; end; v2 c= v proof let t be object; assume t in v2; then consider y0 be Element of TG such that A18: t = y0 and A19: [t2,y0] in V0; consider xt,yt be Element of TG such that A20: [t2,y0] = [xt,yt] and A21: xt" * yt in U0 by A19; t2 = xt & y0 = yt by A20,XTUPLE_0:1; then consider u1,u2 be Element of TG such that A22: t3" * y0 = u1 * u2 and A23: u1 in {t3}" and A24: u2 in w by A21; {t3"} = {t3}" by GROUP_2:3; then u1 = t3" by A23,TARSKI:def 1; hence thesis by A18,A22,A24,GROUP_1:6; end; hence thesis by A15; end; then v = Neighborhood(V0,t2); then v in Neighborhood t2; hence thesis by UNIFORM2:def 14; end; then v is open; then u in Family_open_set(FMT_induced_by(left_uniformity(TG))); hence thesis by FINTOPO7:def 16; end; hence thesis by A2; end; theorem the topology of TopSpace_induced_by(right_uniformity(TG)) = the topology of TG proof set X = the topology of FMT2TopSpace(FMT_induced_by(right_uniformity(TG))), Y = the topology of TG; A2: X c= Y proof let x be object; assume x in X; then x in Family_open_set(FMT_induced_by(right_uniformity(TG))) by FINTOPO7:def 16; then consider y be open Subset of FMT_induced_by(right_uniformity(TG)) such that A3: x = y; reconsider z = x as Subset of TG by A3; z is open proof now let t be Point of TG; assume A4: t in z; reconsider t1 = t as Point of FMT_induced_by(right_uniformity(TG)); A5: y in U_FMT t1 by A3,A4,FINTOPO7:def 1; reconsider t2 = t1 as Element of right_uniformity(TG); z in Neighborhood t2 by A3,A5,UNIFORM2:def 14; then consider V0 be Element of the entourages of right_uniformity(TG) such that A6: z = Neighborhood(V0,t2); consider tg be Element of system_right_uniformity(TG) such that A7: tg c= V0 by CARDFIL2:def 8; tg in the set of all element_right_uniformity(U) where U is a_neighborhood of 1_TG; then consider U0 be a_neighborhood of 1_TG such that A8: tg = element_right_uniformity(U0); reconsider A = U0 * {t} as a_neighborhood of t by Th5; A c= z proof let u be object; assume u in A; then consider u0,u1 be Element of TG such that A9: u = u0 * u1 and A10: u0 in U0 and A11: u1 in {t}; reconsider u2 = u as Element of TG by A9; u0 * 1_TG in U0 by A10,GROUP_1:def 4; then u0 * (t * t") in U0 by GROUP_1:def 5; then (u0 * t) * t" in U0 by GROUP_1:def 3; then u2 * t" in U0 by A9,A11,TARSKI:def 1; then [t,u2] in element_right_uniformity(U0); hence thesis by A6,A7,A8; end; hence ex A be Subset of TG st A is a_neighborhood of t & A c= z; end; hence thesis by CONNSP_2:7; end; hence x in Y; end; Y c= X proof let u be object; assume A12: u in Y; then reconsider u as Subset of TG; reconsider v = u as Subset of FMT_induced_by(right_uniformity(TG)); for x being Element of FMT_induced_by(right_uniformity(TG)) st x in v holds v in U_FMT x proof let x be Element of FMT_induced_by(right_uniformity(TG)); assume A13: x in v; reconsider t2 = x as Element of right_uniformity(TG); reconsider t3 = x as Element of TG; reconsider w = v as Subset of TG; now {t3"} = {t3}" by GROUP_2:3; then t3" in {t3}" by TARSKI:def 1; then t3 * t3" in w * {t3}" by A13; hence 1_TG in w * {t3}" by GROUP_1:def 5; w is open by A12; hence w * {t3}" is open; end; then reconsider U0 = w * {t3}" as a_neighborhood of 1_TG by CONNSP_2:6; element_right_uniformity(U0) in system_right_uniformity(TG); then reconsider V0 = element_right_uniformity(U0) as Element of the entourages of right_uniformity(TG) by CARDFIL2:def 8; v = {y where y is Element of TG: [t2,y] in V0} proof set v2 = {y where y is Element of TG: [t2,y] in V0}; A15: v c= v2 proof let t be object; assume A16: t in v; then reconsider t4 = t as Element of TG; {t3"} = {t3}" by GROUP_2:3; then t3" in {t3}" by TARSKI:def 1; then t4 * t3" in w * {t3}" by A16; then [t2,t4] in element_right_uniformity(U0); hence thesis; end; v2 c= v proof let t be object; assume t in v2; then consider y0 be Element of TG such that A18: t = y0 and A19: [t2,y0] in V0; consider xt,yt be Element of TG such that A20: [t2,y0] = [xt,yt] and A21: yt * xt" in U0 by A19; t2 = xt & y0 = yt by A20,XTUPLE_0:1; then consider u1,u2 be Element of TG such that A22: y0 * t3" = u1 * u2 and A23: u1 in w and A24: u2 in {t3}" by A21; {t3"} = {t3}" by GROUP_2:3; then u2 = t3" by A24,TARSKI:def 1; hence thesis by A22,A23,A18,GROUP_1:6; end; hence thesis by A15; end; then v = Neighborhood(V0,t2); then v in Neighborhood t2; hence thesis by UNIFORM2:def 14; end; then v is open; then u in Family_open_set(FMT_induced_by(right_uniformity(TG))); hence thesis by FINTOPO7:def 16; end; hence thesis by A2; end; begin :: Function uniformly continuous definition let US1,US2 be UniformSpaceStr, f be Function of US1,US2; attr f is uniformly_continuous means 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; existence proof set e = the Element of US2; set f = US1 --> e; 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 proof let V be Element of the entourages of US2; per cases; suppose A1: [e,e] in V; set U = the Element of the entourages of US1; take U; thus for x,y be object st [x,y] in U holds [f.x,f.y] in V proof let x,y be object; assume A2: [x,y] in U; consider a,b be object such that A3: a in the carrier of US1 and A4: b in the carrier of US1 and A5: [x,y] = [a,b] by A2,ZFMISC_1:def 2; A6: x = a & y = b by A5,XTUPLE_0:1; f.b = e by A4,FUNCOP_1:7; hence thesis by A1,A6,A3,FUNCOP_1:7; end; end; suppose A8: not [e,e] in V; US2 is axiom_U1; then A9: id the carrier of US2 c= V; [e,e] in id the carrier of US2 by RELAT_1:def 10; hence thesis by A8,A9; end; end; then f is uniformly_continuous; hence thesis; end; end; begin :: Partition topology theorem Th14: the set of all union P where P is Subset of D = UniCl D proof set F = the set of all union P where P is Subset of D; thus F c= UniCl D proof let x be object; assume x in F; then consider P be Subset of D such that A2: x = union P; P c= D & D c= bool X; then P c= bool X; then reconsider Y = P as Subset-Family of X; Y c= D & union Y = union P; hence thesis by A2,CANTOR_1:def 1; end; let x be object; assume x in UniCl D; then consider Y be Subset-Family of X such that A3: Y c= D and A4: x = union Y by CANTOR_1:def 1; reconsider P = Y as Subset of D by A3; x = union P by A4; hence thesis; end; theorem Th15: X in UniCl D proof D c= D; then union D in the set of all union P where P is Subset of D; then X in the set of all union P where P is Subset of D by EQREL_1:def 4; hence thesis by Th14; end; theorem Th16: D = {} implies X is empty & UniCl D = {{}} proof set DU = the set of all union P where P is Subset of D; assume A1: D = {}; hence X is empty by ZFMISC_1:2,EQREL_1:def 4; UniCl D = {{}} by A1,YELLOW_9:16; hence thesis; end; registration let X be set, D be a_partition of X; cluster UniCl D -> cap-closed; coherence proof set DU = the set of all union P where P is Subset of D; now let a,b be set; assume that A1: a in DU and A2: b in DU; consider Pa be Subset of D such that A3: a = union Pa by A1; consider Pb be Subset of D such that A4: b = union Pb by A2; now let X,Y be set; assume that A5: X <> Y and A6: X in Pa \/ Pb and A7: Y in Pa \/ Pb; X in D & Y in D by A6,A7; hence X misses Y by A5,EQREL_1:def 4; end; then union Pa /\ union Pb = union (Pa /\ Pb) by ZFMISC_1:83; hence a /\ b in DU by A3,A4; end; then DU is cap-closed; hence thesis by Th14; end; end; registration let X be set, D be a_partition of X; cluster UniCl D -> union-closed; coherence proof the set of all union P where P is Subset of D c= bool X proof let x be object; assume x in the set of all union P where P is Subset of D; then consider P be Subset of D such that A1: x = union P; union P c= union D by ZFMISC_1:77; then union P c= X by EQREL_1:def 4; hence thesis by A1; end; then reconsider DU = the set of all union P where P is Subset of D as Subset-Family of X; for a being Subset-Family of X st a c= DU holds union a in DU proof let a be Subset-Family of X; assume A2: a c= DU; set P = {x where x is Element of D: x c= union a}; per cases; suppose A3: D = {}; then UniCl D = {{}} by Th16; then a c= {{}} by A2,Th14; then a = {} or a = {{}} by ZFMISC_1:33; hence union a in DU by A3,ZFMISC_1:2; end; suppose A4: D <> {}; P c= D proof let t be object; assume t in P; then ex x be Element of D st t = x & x c= union a; hence thesis by A4; end; then reconsider P as Subset of D; union a = union P proof thus union a c= union P proof let x be object; assume x in union a; then consider t be set such that A6: x in t and A7: t in a by TARSKI:def 4; t in DU by A2,A7; then consider Q be Subset of D such that A8: t = union Q; consider y be set such that A9: x in y and A10: y in Q by A6,A8,TARSKI:def 4; reconsider y as Element of D by A10; y c= union a proof let b be object; assume b in y; then b in union Q by A10,TARSKI:def 4; hence thesis by A7,A8,TARSKI:def 4; end; then y in P; hence thesis by A9,TARSKI:def 4; end; let t be object; assume t in union P; then consider u be set such that A11: t in u and A12: u in P by TARSKI:def 4; ex xu be Element of D st u = xu & xu c= union a by A12; hence thesis by A11; end; hence union a in DU; end; end; then DU is union-closed; hence thesis by Th14; end; end; registration let X be set; cluster union-closed -> cup-closed for Subset-Family of X; coherence proof now let SF be Subset-Family of X; assume A1: SF is union-closed; now let a,b be set; assume that A2: a in SF and A3: b in SF; A4: {a,b} c= SF by A2,A3,TARSKI:def 2; SF c= bool X; then {a,b} c= bool X by A4; then reconsider c = {a,b} as Subset-Family of X; {a,b} c= SF by A2,A3,TARSKI:def 2; then union c in SF by A1; hence a \/ b in SF by ZFMISC_1:75; end; hence SF is cup-closed; end; hence thesis; end; end; registration let X be set, D be a_partition of X; cluster UniCl D -> compl-closed; coherence proof now let A be Subset of X; assume A in UniCl D; then A in the set of all union P where P is Subset of D by Th14; then consider P be Subset of D such that A1: A = union P; reconsider P1 = D \ P as Subset of D by XBOOLE_1:36; union P1 = union D \ union P by Th2 .= A` by A1,EQREL_1:def 4; then A` in the set of all union P where P is Subset of D; hence A` in UniCl D by Th14; end; hence thesis; end; end; registration let X be set, D be a_partition of X; cluster UniCl D -> cup-closed diff-closed; coherence; end; theorem UniCl D is Ring_of_sets proof set DU = the set of all union P where P is Subset of D; UniCl D is cap-closed cup-closed; then DU is cap-closed cup-closed by Th14; then for x,y be set st x in DU & y in DU holds x/\y in DU & x\/y in DU; then DU is Ring_of_sets by COHSP_1:def 7,LATTICE7:def 8; hence thesis by Th14; end; registration let X, D; cluster UniCl D -> with_empty_element; coherence proof {} c= D; then union {} in the set of all union P where P is Subset of D; hence thesis by ZFMISC_1:2,Th14; end; end; registration let X be set,D be a_partition of X; cluster UniCl D -> non empty; coherence; end; theorem UniCl D is Field_Subset of X; registration let X be set,D be a_partition of X; cluster UniCl D -> sigma-additive; coherence proof per cases; suppose A1: D is empty; now let M be N_Sub_set_fam of X; assume M c= UniCl D; then M c= {{}} by A1,YELLOW_9:16; then per cases by ZFMISC_1:33; suppose M = {}; hence union M in UniCl D; end; suppose A2: M = {{}}; {} c= D; then reconsider P = {} as Subset of D; union P = union M by A2,ZFMISC_1:2; then union M in the set of all union P where P is Subset of D; hence union M in UniCl D by Th14; end; end; hence thesis; end; suppose A3: D is non empty; now let M be N_Sub_set_fam of X; assume A4: M c= UniCl D; {p where p is Element of D:p c= union M} c= D proof let t be object; assume t in {p where p is Element of D:p c= union M}; then ex p be Element of D st t = p & p c= union M; hence thesis by A3; end; then reconsider P = {p where p is Element of D:p c= union M} as Subset of D; union M = union P proof thus union M c= union P proof let t be object; assume t in union M; then consider y be set such that A6: t in y and A7: y in M by TARSKI:def 4; y in UniCl D by A7,A4; then y in the set of all union Q where Q is Subset of D by Th14; then consider Q be Subset of D such that A8: y = union Q; consider z be set such that A9: t in z and A10: z in Q by A6,A8,TARSKI:def 4; reconsider z as Element of D by A10; A11: z c= y by A8,A10,ZFMISC_1:74; y c= union M by A7,ZFMISC_1:74; then z c= union M by A11; then z in P; hence thesis by A9,TARSKI:def 4; end; let x be object; assume x in union P; then consider y be set such that A12: x in y and A13: y in P by TARSKI:def 4; ex p be Element of D st y = p & p c= union M by A13; hence thesis by A12; end; then union M in the set of all union P where P is Subset of D; hence union M in UniCl D by Th14; end; hence thesis; end; end; end; registration let X be set,D be a_partition of X; cluster UniCl D -> sigma-multiplicative; coherence; end; theorem 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; coherence by TOPGEN_4:17; end; theorem for Omega being non empty set, D being a_partition of Omega holds UniCl D is Dynkin_System of Omega proof let Omega be non empty set, D be a_partition of Omega; now hereby let f be SetSequence of Omega; assume that A1: rng f c= UniCl D and f is disjoint_valued; UniCl D c= bool Omega; then rng f c= bool Omega by A1; then reconsider a = rng f as Subset-Family of Omega; union a in UniCl D by A1,ROUGHS_4:def 3; hence Union f in UniCl D by CARD_3:def 4; end; thus for X be Subset of Omega st X in UniCl D holds X` in UniCl D by PROB_1:def 1; UniCl D is with_empty_element; hence {} in UniCl D; end; hence thesis by DYNKIN:def 5; end; definition let X be set,D be a_partition of X; func partition_topology(D) -> TopSpace equals TopStruct (# X,UniCl D #); coherence proof set TS = TopStruct(# X,UniCl D #); (the carrier of TS in the topology of TS) & (for a being Subset-Family of TS st a c= the topology of TS holds union a in the topology of TS) & (for a,b being Subset of TS st a in the topology of TS & b in the topology of TS holds a /\ b in the topology of TS) by Th15,ROUGHS_4:def 3,FINSUB_1:def 2; hence thesis by PRE_TOPC:def 1; end; end; theorem Th18: for O being open Subset of partition_topology(D) holds O is closed proof let O be open Subset of partition_topology(D); O` in UniCl D by PRE_TOPC:def 2,PROB_1:def 1; hence thesis by PRE_TOPC:def 2; end; theorem Th19: for O being closed Subset of partition_topology(D) holds O is open proof let O be closed Subset of partition_topology(D); [#]partition_topology(D) \ O in UniCl D by PRE_TOPC:def 2,PRE_TOPC:def 3; then A1: (X \ O)` in UniCl D by PROB_1:def 1; O = X /\ O by XBOOLE_1:18,XBOOLE_1:19; hence thesis by A1,XBOOLE_1:48; end; theorem 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,D be a_partition of X; cluster partition_topology(D) -> non empty; coherence; end; theorem for X being non empty set,D being a_partition of X holds capOpCl partition_topology(D) = UniCl D proof let X be non empty set,D be a_partition of X; set Y = {A /\ B where A, B is Subset of partition_topology(D): A is open & B is closed}; A1: Y c= UniCl D proof let x be object; assume x in Y; then consider A,B be Subset of partition_topology(D) such that A2: x = A /\ B and A3: A is open and A4: B is closed; B is open by A4,Th19; hence thesis by A2,A3,FINSUB_1:def 2; end; UniCl D c= Y proof let x be object; assume A5: x in UniCl D; then reconsider y = x as Subset of partition_topology(D); X in UniCl D by Th15; then reconsider XX = X as Subset of partition_topology(D); A6: y = y /\ X by XBOOLE_1:18,XBOOLE_1:19; y is open & XX is closed by A5; hence thesis by A6; end; hence thesis by A1; end; theorem for X being non empty set,D being a_partition of X holds OpenClosedSet(partition_topology(D)) = the topology of partition_topology(D) proof let X be non empty set,D be a_partition of X; thus OpenClosedSet(partition_topology(D)) c= the topology of partition_topology(D) proof let x be object; assume x in OpenClosedSet(partition_topology(D)); then ex y be Subset of partition_topology(D) st x = y & y is open closed; hence thesis; end; let x be object; assume A2: x in the topology of partition_topology(D); then reconsider y = x as Subset of partition_topology(D); y is open by A2; then y is open closed by Th18; hence thesis; end; 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 {S where S is Subset of [:X,X:] : R c= S}; coherence proof A1: R in {S where S is Subset of [:X,X:] : R c= S}; now let x be object; assume x in {S where S is Subset of [:X,X:] : R c= S}; then ex S be Subset of [:X,X:] st x = S & R c= S; hence x in bool [:X,X:]; end; then {S where S is Subset of [:X,X:] : R c= S} c= bool [:X,X:]; hence thesis by A1; end; end; theorem <. rho(R).] = rho(R) proof <. rho(R).] c= rho(R) proof let t be object; assume A1: t in <. rho(R).]; then reconsider u = t as Subset of [:X,X:]; consider b be Element of rho(R) such that A2: b c= u by A1,CARDFIL2:def 8; b in rho(R); then ex c be Subset of [:X,X:] st b = c & R c= c; then R c= u by A2; hence thesis; end; hence thesis by CARDFIL2:18; end; theorem <. {R} .] = rho(R) proof thus <. {R} .] c= rho(R) proof let x be object; assume A2: x in <. {R} .]; then reconsider y = x as Subset of [:X,X:]; consider b be Element of {R} such that A3: b c= y by A2,CARDFIL2:def 8; R c= y by A3,TARSKI:def 1; hence thesis; end; let x be object; assume x in rho(R); then consider S be Relation of X such that A4: x = S and A5: R c= S; R is Element of {R} by TARSKI:def 1; hence thesis by A4,A5,CARDFIL2:def 8; end; theorem Th20: rho(R) is upper & rho(R) is cap-closed proof now let Y1,Y2 be Subset of [:X,X:]; assume that A1: Y1 in rho(R) and A2: Y1 c= Y2; consider S be Subset of [:X,X:] such that A3: Y1 = S and A4: R c= S by A1; R c= Y2 by A2,A3,A4; hence Y2 in rho(R); end; hence rho(R) is upper; now let X1,Y1 be set; assume that A5: X1 in rho(R) and A6: Y1 in rho(R); consider SX be Subset of [:X,X:] such that A7: X1 = SX and A8: R c= SX by A5; consider SY be Subset of [:X,X:] such that A9: Y1 = SY and A10: R c= SY by A6; R c= SX /\ SY by A8,A10,XBOOLE_1:19; hence X1 /\ Y1 in rho(R) by A7,A9; end; hence rho(R) is cap-closed; end; registration let X,R; cluster rho(R) -> quasi_basis; coherence proof now let Y,Z be Element of rho(R); Y in rho(R); then consider SY be Subset of [:X,X:] such that A1: Y = SY and A2: R c= SY; Z in rho(R); then consider SZ be Subset of [:X,X:] such that A3: Z = SZ and A4: R c= SZ; R in rho(R); then reconsider T = R as Element of rho(R); T c= Y /\ Z by A1,A3,A2,A4,XBOOLE_1:19; hence ex T be Element of rho(R) st T c= Y /\ Z; end; hence thesis; end; end; theorem Th21: for R being total reflexive Relation of X holds rho(R) is axiom_UP1 proof let R be total reflexive Relation of X; now let B be Element of rho(R); B in rho(R); then consider C be Subset of [:X,X:] such that A1: B = C and A2: R c= C; A3: field R = X by ORDERS_1:12; id X c= R proof let t be object; assume A4: t in id X; then consider a,b be object such that a in X and A5: b in X and A6: t = [a,b] by ZFMISC_1:def 2; a = b by A4,A6,RELAT_1:def 10; hence thesis by A5,A3,A6,RELAT_2:def 9,RELAT_2:def 1; end; hence id X c= B by A1,A2; end; hence thesis; end; theorem Th22: for R being symmetric Relation of X holds rho(R) is axiom_UP2 proof let R be symmetric Relation of X; let B1 be Element of rho(R); B1 in rho(R); then consider C1 be Subset of [:X,X:] such that A1: B1 = C1 and A2: R c= C1; reconsider R1 = C1 as Relation of X; A3: R~ c= R1~ by A2,SYSREL:11; R in rho(R); then reconsider B2 = R as Element of rho(R); B2 c= B1~ by A3,A1,RELAT_2:13; hence ex B2 be Element of rho(R) st B2 c= B1~; end; theorem Th24: for R being total transitive Relation of X holds rho(R) is axiom_UP3 proof let R be total transitive Relation of X; let B1 be Element of rho(R); B1 in rho(R); then consider C be Subset of [:X,X:] such that A1: B1 = C and A2: R c= C; R in rho(R); then reconsider B2 = R as Element of rho(R); R * R c= R by RELAT_2:27; then B2 * B2 c= B1 by A1,A2; hence ex B2 being Element of rho(R) st B2 * B2 c= B1; end; definition let X be set, R be Relation of X; func uniformity_induced_by(R) -> upper cap-closed strict UniformSpaceStr equals UniformSpaceStr(# X,rho(R) #); coherence proof UniformSpaceStr(# X,rho(R) #) is upper cap-closed by Th20; hence thesis; end; end; theorem Th25: for X being set,R being total reflexive Relation of X holds uniformity_induced_by(R) is axiom_U1 proof let X be set, R be total reflexive Relation of X; rho(R) is axiom_UP1 by Th21; hence thesis; end; theorem Th26: for X being set,R being symmetric Relation of X holds uniformity_induced_by(R) is axiom_U2 proof let X be set, R be symmetric Relation of X; A1: rho(R) is axiom_UP2 by Th22; now let S be Element of the entourages of uniformity_induced_by(R); reconsider S1 = S as Element of rho(R); consider T be Element of rho(R) such that A2: T c= S1~ by A1; T in rho(R); then consider S2 be Subset of [:X,X:] such that A3: T = S2 and A4: R c= S2; R c= S[~] by A2,A3,A4; hence S[~] in the entourages of uniformity_induced_by(R); end; hence thesis; end; theorem Th27: for X being set, R being total transitive Relation of X holds uniformity_induced_by(R) is axiom_U3 proof let X be set, R be total transitive Relation of X; A1: rho(R) is axiom_UP3 by Th24; let S be Element of the entourages of uniformity_induced_by(R); reconsider S1 = S as Element of rho(R); consider W be Element of rho(R) such that A2: W * W c= S1 by A1; thus ex W be Element of the entourages of uniformity_induced_by(R) st W * W c= S by A2; end; definition let X be set, R be Tolerance of X; redefine func uniformity_induced_by(R) -> strict Semi-UniformSpace; coherence by Th25,Th26; end; theorem for X being set, R being Equivalence_Relation of X holds uniformity_induced_by(R) is UniformSpace by Th27; definition let X be set, R be Equivalence_Relation of X; redefine func uniformity_induced_by(R) -> strict UniformSpace; coherence by Th25,Th26,Th27; end; registration let X be non empty set, R be Tolerance of X; cluster uniformity_induced_by(R) -> non empty; coherence; end; registration cluster -> topological for non empty UniformSpace; coherence; end; definition let US be non empty UniformSpace; func @US -> topological non empty axiom_U1 UniformSpaceStr equals US; coherence; end; theorem for X being non empty set, R being Equivalence_Relation of X holds TopSpace_induced_by( @(uniformity_induced_by(R)) ) = partition_topology(Class R) proof let X be non empty set, R be Equivalence_Relation of X; set T1 = TopSpace_induced_by( @(uniformity_induced_by(R)) ), T2 = partition_topology(Class R); now thus the carrier of T1 = the carrier of T2 by FINTOPO7:def 16; A1: the topology of T1 = Family_open_set(FMT_induced_by( @(uniformity_induced_by(R)))) by FINTOPO7:def 16 .= the set of all O where O is open Subset of FMT_induced_by( @(uniformity_induced_by(R))); A2: the topology of T2 = the set of all union P where P is Subset of Class R by Th14; A3: the topology of T1 c= the topology of T2 proof let t be object; assume t in the topology of T1; then consider O be open Subset of FMT_induced_by( @(uniformity_induced_by(R))) such that A4: t = O by A1; per cases; suppose A5: O is empty; {} c= Class R; then reconsider P = {} as Subset of Class R; t = union P by A4,A5,ZFMISC_1:2; hence thesis by A2; end; suppose A6: O is non empty; set P = the set of all Class(R,u) where u is Element of O; P c= Class R proof let u be object; assume u in P; then consider u0 be Element of O such that A7: u = Class(R,u0); A8: u0 in O by A6; thus thesis by A7,A8,EQREL_1:def 3; end; then reconsider P as Subset of Class R; reconsider t1 = t as Subset of X by A4; t1 = union P proof thus t1 c= union P proof let a be object; assume A10: a in t1; then reconsider b = a as Element of O by A4; b in Class(R,b) & Class(R,b) in P by A10,EQREL_1:20; hence thesis by TARSKI:def 4; end; let a be object; assume a in union P; then consider Q be set such that A11: a in Q and A12: Q in P by TARSKI:def 4; consider v be Element of O such that A13: Q = Class(R,v) by A12; v in O by A6; then reconsider w = v as Element of @(uniformity_induced_by(R)); O in Neighborhood w by Th8,A6; then consider V be Element of the entourages of @(uniformity_induced_by(R)) such that A14: O = Neighborhood(V,w); V in rho(R); then consider W be Relation of the carrier of @(uniformity_induced_by(R)) such that A15: V = W and A16: R c= W; A17: Neighborhood(V,w) = V.:{w} & Neighborhood(V,w) = rng(V|{w}) & Neighborhood(V,w) = Im(V,w) & Neighborhood(V,w) = Class(V,w) & Neighborhood(V,w) = neighbourhood(w,V) by UNIFORM2:14; Class(R,w) c= Class(W,w) proof let z be object; assume z in Class(R,w); then [w,z] in W by A16,EQREL_1:18; hence thesis by EQREL_1:18; end; hence thesis by A11,A13,A4,A17,A15,A14; end; hence thesis by A2; end; end; the topology of T2 c= the topology of T1 proof let t be object; assume A18: t in the topology of T2; then consider P be Subset of Class R such that A19: t = union P by A2; reconsider Q = union P as Subset of FMT_induced_by( @(uniformity_induced_by(R))) by A18,A19; for x being Element of @(uniformity_induced_by(R)) st x in Q holds Q in Neighborhood x proof let x be Element of @(uniformity_induced_by(R)); assume A20: x in Q; then consider T be set such that A21: x in T and A22: T in P by TARSKI:def 4; T in Class R by A22; then consider b be object such that A23: b in X and A24: T = Class(R,b) by EQREL_1:def 3; set S1 = the set of all [x,y] where y is Element of Q; set S = R \/ S1; S1 c= [:X,X:] proof let s be object; assume s in S1; then consider y be Element of Q such that A25: s = [x,y]; Q c= X; then y in X by A20; hence thesis by A25,ZFMISC_1:def 2; end; then reconsider S as Subset of [:X,X:] by XBOOLE_1:8; R c= S by XBOOLE_1:7; then S in rho(R); then reconsider V = S as Element of the entourages of @(uniformity_induced_by(R)); Q = Neighborhood(V,x) proof thus Q c= Neighborhood(V,x) proof let a be object; assume a in Q; then reconsider b = a as Element of Q; A27: [x,b] in S1; A28: S1 c= R \/ S1 by XBOOLE_1:7; b in Q by A20; then reconsider c = b as Element of @(uniformity_induced_by(R)); [x,c] in V by A28,A27; hence thesis; end; let a be object; assume a in Neighborhood(V,x); then consider y be Element of @(uniformity_induced_by(R)) such that A29: a = y and A30: [x,y] in V; per cases by A29,A30,XBOOLE_0:def 3; suppose [x,a] in S1; then consider y be Element of Q such that A31: [x,a] = [x,y]; a = y by A31,XTUPLE_0:1; hence thesis by A20; end; suppose [x,a] in R; then A32: a in Class(R,x) by EQREL_1:18; Class(R,b) = Class(R,x) by A21,A23,A24,EQREL_1:23; hence thesis by A22,A24,A32,TARSKI:def 4; end; end; hence thesis; end; then reconsider O = union P as open Subset of FMT_induced_by( @(uniformity_induced_by(R))) by Th8; t = O by A19; hence thesis by A1; end; hence the topology of T1 = the topology of T2 by A3; end; hence thesis; end; begin :: Uniformity induced by a Tolerance or an Equivalence theorem 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 let USS be upper UniformSpaceStr; assume A1: meet the entourages of USS in the entourages of USS; reconsider R = meet the entourages of USS as Relation of the carrier of USS; take R; A2: rho(R) c= the entourages of USS proof let x be object; assume x in rho(R); then consider S be Subset of [:the carrier of USS,the carrier of USS:] such that A3: x = S and A4: R c= S; the entourages of USS is upper by UNIFORM2:def 7; hence thesis by A1,A3,A4; end; the entourages of USS c= rho(R) proof let x be object; assume x in the entourages of USS; then consider S be Subset of [:the carrier of USS,the carrier of USS:] such that A5: x = S and A6: S in the entourages of USS; R c= S by A6,SETFAM_1:3; hence thesis by A5; end; hence thesis by A2; end; definition let USS be UniformSpaceStr; func Uniformity2InternalRel(USS) -> Relation of the carrier of USS equals meet the entourages of USS; coherence; end; definition let USS be UniformSpaceStr; func UniformSpaceStr2RelStr(USS) -> RelStr equals RelStr(# the carrier of USS, Uniformity2InternalRel(USS) #); coherence; end; definition let RS be RelStr; func InternalRel2Uniformity(RS) -> Subset-Family of [:the carrier of RS,the carrier of RS:] equals {R where R is Relation of the carrier of RS : the InternalRel of RS c= R}; coherence proof set IRS = {R where R is Relation of the carrier of RS : the InternalRel of RS c= R}; IRS c= bool [:the carrier of RS,the carrier of RS:] proof let x be object; assume x in IRS; then ex R be Relation of the carrier of RS st x = R & the InternalRel of RS c= R; hence thesis; end; hence thesis; end; end; definition let RS be RelStr; func RelStr2UniformSpaceStr(RS) -> strict UniformSpaceStr equals UniformSpaceStr(# the carrier of RS, InternalRel2Uniformity RS #); coherence; end; definition let RS be RelStr; func InternalRel2Element(RS) -> Element of the entourages of RelStr2UniformSpaceStr(RS) equals the InternalRel of RS; coherence proof the InternalRel of RS in the entourages of RelStr2UniformSpaceStr(RS); hence thesis; end; end; theorem Th28: for R be Relation of X holds meet rho(R) = R proof let R be Relation of X; thus meet rho(R) c= R proof let x be object; assume A2: x in meet rho(R); R in rho(R); hence thesis by A2,SETFAM_1:def 1; end; let x be object; assume A3: x in R; now let Y be set; assume Y in rho(R); then ex S be Relation of X st Y = S & R c= S; hence x in Y by A3; end; hence thesis by SETFAM_1:def 1; end; theorem for RS being strict RelStr holds UniformSpaceStr2RelStr(RelStr2UniformSpaceStr(RS)) = RS proof let RS be strict RelStr; set US = UniformSpaceStr2RelStr (RelStr2UniformSpaceStr(RS)); now thus the carrier of US = the carrier of RS; the InternalRel of US = meet rho(the InternalRel of RS); hence the InternalRel of US = the InternalRel of RS by Th28; end; hence thesis; end; theorem 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: for SF being Subset-Family of [:X,X:],R being Relation of X st SF = rho(R) holds SF c= rho(meet SF) proof let SF be Subset-Family of [:X,X:],R be Relation of X; assume A1: SF = rho(R); SF c= rho(meet(SF)) proof let x be object; assume A2: x in SF; then consider S be Subset of [:X,X:] such that A3: x = S and R c= S by A1; meet(SF) c= S by A3,A2,SETFAM_1:def 1; hence thesis by A3; end; hence thesis; end; theorem Th30: for SF being upper Subset-Family of [:X,X:] st meet SF in SF holds rho(meet SF) c= SF proof let SF be upper Subset-Family of [:X,X:]; assume A1: meet SF in SF; thus rho(meet(SF)) c= SF proof let x be object; assume x in rho(meet(SF)); then consider S be Subset of [:X,X:] such that A2: x = S and A3: meet(SF) c= S; SF is upper; hence thesis by A2,A3,A1; end; thus thesis; end; theorem 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 by Th29,Th30; theorem Th31: 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 let US be upper UniformSpaceStr; given R being Relation of the carrier of US such that A2: the entourages of US = rho(R) and A3: meet the entourages of US in the entourages of US; the entourages of US is upper by UNIFORM2:def 7; hence thesis by A2,A3,Th29,Th30; end; theorem 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) by Th31; theorem 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 for R being Tolerance of X holds RelStr2UniformSpaceStr(UniformSpaceStr2RelStr(uniformity_induced_by(R))) = uniformity_induced_by(R) proof let R be Tolerance of X; the carrier of RelStr2UniformSpaceStr(UniformSpaceStr2RelStr(uniformity_induced_by(R))) = the carrier of uniformity_induced_by(R) & the entourages of RelStr2UniformSpaceStr(UniformSpaceStr2RelStr(uniformity_induced_by(R))) = rho (meet(the entourages of uniformity_induced_by(R))); hence thesis by Th28; end; theorem for R being Equivalence_Relation of X holds RelStr2UniformSpaceStr(UniformSpaceStr2RelStr(uniformity_induced_by(R))) = uniformity_induced_by(R) proof let R be Equivalence_Relation of X; the carrier of RelStr2UniformSpaceStr(UniformSpaceStr2RelStr( uniformity_induced_by(R)))= the carrier of uniformity_induced_by(R) & the entourages of RelStr2UniformSpaceStr(UniformSpaceStr2RelStr( uniformity_induced_by(R)))= rho (meet(the entourages of uniformity_induced_by(R))); hence thesis by Th28; end; 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 [:X \ A,X \ A:] \/ [:A,A:]; coherence proof per cases; suppose SF is empty; then A is empty by SUBSET_1:def 1; then [:A,A:] c= [:X,X:]; hence thesis by XBOOLE_1:8; end; suppose SF is non empty; then A in SF; then [:A,A:] c= [:X,X:] by ZFMISC_1:96; hence thesis by XBOOLE_1:8; end; end; end; reserve SF for Subset-Family of X, A for Element of SF; theorem Th34: A = {} implies block_Pervin_uniformity(A) = [:X,X:] proof assume A = {}; then block_Pervin_uniformity(A) = [:X \ {},X \ {}:] \/ [:{},{}:]; hence thesis; end; theorem 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} proof assume A1: X is non empty; set S = {[x,y] where x,y is Element of X: x in A iff y in A}; A2: block_Pervin_uniformity(A) c= S proof let x be object; assume A3: x in block_Pervin_uniformity(A); then A4: x in [: A, A :] or x in [: X \ A, X \ A :] by XBOOLE_0:def 3; consider a,b be object such that A9: a in X and A10: b in X and A11: x = [a,b] by A3,ZFMISC_1:def 2; (a in A & b in A) or (a in X \ A & b in X \ A) by A4,A11,ZFMISC_1:87; then (a in A & b in A) or ((a in X & not a in A) & (b in X & not b in A)) by XBOOLE_0:def 5; hence thesis by A9,A10,A11; end; S c= block_Pervin_uniformity(A) proof let x be object; assume x in S; then consider a,b be Element of X such that A12: x = [a,b] and A13: a in A iff b in A; x in [:A,A:] or (a in X\A & b in X\A) by A1,A13,A12,ZFMISC_1:87,XBOOLE_0:def 5; then x in [: A, A:] or x in [: X\A, X\A :] by A12,ZFMISC_1:87; hence thesis by XBOOLE_0:def 3; end; hence thesis by A2; end; theorem Th35: id X c= block_Pervin_uniformity(A) & block_Pervin_uniformity(A) * block_Pervin_uniformity(A) c= block_Pervin_uniformity(A) proof thus id X c= block_Pervin_uniformity(A) proof let t be object; assume A1: t in id X; then consider a,b be object such that A2: t = [a,b] by RELAT_1:def 1; A3: a in X & a = b by A1,A2,RELAT_1:def 10; per cases; suppose a in A; then a in A & b in A by A1,A2,RELAT_1:def 10; then [a,b] in [:A,A:] by ZFMISC_1:def 2; hence thesis by A2,XBOOLE_0:def 3; end; suppose not a in A; then a in X \ A by A3,XBOOLE_0:def 5; then t in [:X \ A,X \ A:] by A2,A3,ZFMISC_1:def 2; hence thesis by XBOOLE_0:def 3; end; end; now let t be object; assume A4: t in (block_Pervin_uniformity(A)) * (block_Pervin_uniformity(A)); then consider a,b be object such that A5: t = [a,b] by RELAT_1:def 1; [a,b] in {[x,y] where x,y is Element of X : ex z being Element of X st [x,z] in block_Pervin_uniformity(A) & [z,y] in block_Pervin_uniformity(A)} by A5,A4,UNIFORM2:3; then consider x,y be Element of X such that A6: [a,b] = [x,y] and A7: ex z being Element of X st [x,z] in block_Pervin_uniformity(A) & [z,y] in block_Pervin_uniformity(A); consider z being Element of X such that A8: [x,z] in block_Pervin_uniformity(A) and A9: [z,y] in block_Pervin_uniformity(A) by A7; per cases; suppose A10: x in A; [x,z] in [:A,A:] proof per cases by A8,XBOOLE_0:def 3; suppose [x,z] in [:X \ A,X \ A:]; then x in X \ A by ZFMISC_1:87; hence thesis by A10,XBOOLE_0:def 5; end; suppose [x,z] in [:A,A:]; hence thesis; end; end; then A11: z in A by ZFMISC_1:87; [z,y] in [:A,A:] proof per cases by A9,XBOOLE_0:def 3; suppose [z,y] in [:X \ A,X \ A:]; then z in X \ A & y in X by ZFMISC_1:87; hence thesis by A11,XBOOLE_0:def 5; end; suppose [z,y] in [:A,A:]; hence thesis; end; end; then y in A by ZFMISC_1:87; then [x,y] in [:A,A:] by A10,ZFMISC_1:def 2; hence t in block_Pervin_uniformity(A) by A5,A6,XBOOLE_0:def 3; end; suppose A12: not x in A; per cases; suppose X is empty; hence t in block_Pervin_uniformity(A) by A9; end; suppose X is non empty; then A13: x in X \ A by A12,XBOOLE_0:def 5; [x,z] in [: X \ A,X \ A:] proof per cases by A8,XBOOLE_0:def 3; suppose [x,z] in [:X \ A,X \ A:]; hence thesis; end; suppose [x,z] in [:A,A:]; hence thesis by A12,ZFMISC_1:87; end; end; then A14: z in X \ A by ZFMISC_1:87; [z,y] in [:X \ A,X \ A:] proof per cases by A9,XBOOLE_0:def 3; suppose [z,y] in [:X \ A,X \ A:]; hence thesis; end; suppose [z,y] in [:A,A:]; then z in A & y in A by ZFMISC_1:87; hence thesis by A14,XBOOLE_0:def 5; end; end; then y in X \ A by ZFMISC_1:87; then [x,y] in [:X\ A,X \ A:] by A13,ZFMISC_1:def 2; hence t in block_Pervin_uniformity(A) by A5,A6,XBOOLE_0:def 3; end; end; end; hence thesis; end; definition let X be set, SF be Subset-Family of X; func subbasis_Pervin_uniformity(SF) -> Subset-Family of [:X,X:] equals the set of all block_Pervin_uniformity(A) where A is Element of SF; coherence proof the set of all block_Pervin_uniformity(A) where A is Element of SF c= bool [:X,X:] proof let x be object; assume x in the set of all block_Pervin_uniformity(A) where A is Element of SF; then consider A be Element of SF such that A1: x = block_Pervin_uniformity(A); thus thesis by A1; end; hence thesis; end; end; registration let X be set, SF be Subset-Family of X; cluster subbasis_Pervin_uniformity(SF) -> non empty; coherence proof set A = the Element of SF; set S = block_Pervin_uniformity(A); S in subbasis_Pervin_uniformity(SF); hence thesis; end; end; definition let X be set, SF be Subset-Family of X; func basis_Pervin_uniformity(SF) -> Subset-Family of [:X,X:] equals FinMeetCl(subbasis_Pervin_uniformity(SF)); coherence; end; theorem Th36: basis_Pervin_uniformity(SF) is cap-closed proof now let x,y be set; assume that A1: x in basis_Pervin_uniformity(SF) and A2: y in basis_Pervin_uniformity(SF); consider Y being Subset-Family of [: X,X :] such that A3: Y c= subbasis_Pervin_uniformity(SF) and A4: Y is finite and A5: x = Intersect Y by A1,CANTOR_1:def 3; consider Z being Subset-Family of [:X,X:] such that A6: Z c= subbasis_Pervin_uniformity(SF) and A7: Z is finite and A8: y = Intersect Z by A2,CANTOR_1:def 3; A9: x /\ y = Intersect (Y \/ Z) by A5,A8,MSSUBFAM:8; Y \/ Z c= subbasis_Pervin_uniformity(SF) by A3,A6,XBOOLE_1:8; hence x /\ y in basis_Pervin_uniformity(SF) by A9,A4,A7,CANTOR_1:def 3; end; hence thesis; end; theorem Th37: basis_Pervin_uniformity(SF) is quasi_basis proof basis_Pervin_uniformity(SF) is cap-closed by Th36; hence thesis; end; theorem Th38: basis_Pervin_uniformity(SF) is axiom_UP1 proof for B being Element of basis_Pervin_uniformity(SF) holds id X c= B proof let B be Element of basis_Pervin_uniformity(SF); B in FinMeetCl(subbasis_Pervin_uniformity(SF)); then consider Y being Subset-Family of [:X,X:] such that A1: Y c= subbasis_Pervin_uniformity(SF) and Y is finite and A2: B = Intersect Y by CANTOR_1:def 3; id X c= B proof let t be object; assume A3: t in id X; then consider a,b be object such that A4: t = [a,b] by RELAT_1:def 1; A5: a in X & a = b by A3,A4,RELAT_1:def 10; per cases; suppose Y is empty; then B = [:X,X:] by A2,SETFAM_1:def 9; hence thesis by A3; end; suppose A7: Y is non empty; then A8: Intersect Y = meet Y by SETFAM_1:def 9; now let y be set; assume y in Y; then y in the set of all block_Pervin_uniformity(O) where O is Element of SF by A1; then consider O be Element of SF such that A9: y = block_Pervin_uniformity(O); A10: [:X \ O,X \ O:] c= y & [:O,O:] c= y by A9,XBOOLE_1:10; per cases by A5,XBOOLE_0:def 5; suppose a in X \ O; then [a,b] in [:X \ O,X \ O:] by A5,ZFMISC_1:def 2; hence t in y by A4,A10; end; suppose a in O; then [a,b] in [:O,O:] by A5,ZFMISC_1:def 2; hence t in y by A4,A10; end; end; hence thesis by A2,A8,A7,SETFAM_1:def 1; end; end; hence thesis; end; hence thesis; end; theorem Th39: for A being Element of SF, R being Relation of X st R = block_Pervin_uniformity(A) holds R~ = block_Pervin_uniformity(A) proof let A be Element of SF, R be Relation of X; assume A1: R = block_Pervin_uniformity(A); per cases; suppose SF is empty; then F1: A = {} by SUBSET_1:def 1; then R = [:X,X:] by A1,Th34; then R~ = [:X,X:] by SYSREL:5; hence thesis by F1,Th34; end; suppose SF is non empty; then A in SF; then reconsider A as Subset of X; R~ = [:A,A:] \/ [: X \ A, X \ A:] by A1,Th33; hence thesis; end; end; theorem 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 let R be Relation of X; assume A1: R is Element of subbasis_Pervin_uniformity(SF); then R in the set of all block_Pervin_uniformity(A) where A is Element of SF; then ex A be Element of SF st R = block_Pervin_uniformity(A); hence thesis by A1,Th39; end; theorem Th40: for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity(SF) holds Y[~] = Y proof let Y be non empty Subset-Family of [:X,X:]; assume A1: Y c= subbasis_Pervin_uniformity(SF); A2: Y[~] c= Y proof let x be object; assume x in Y[~]; then consider y be Element of Y such that A3: x = y~; y in subbasis_Pervin_uniformity(SF) by A1; then consider A be Element of SF such that A4: y = block_Pervin_uniformity(A); reconsider z = y as Relation of X; z~ = y by A4,Th39; hence thesis by A3; end; Y c= Y[~] proof let x be object; assume x in Y; then consider y be Element of Y such that A5: x = y; y in subbasis_Pervin_uniformity(SF) by A1; then consider A be Element of SF such that A6: y = block_Pervin_uniformity(A); reconsider z = y as Relation of X; reconsider t = z~ as Element of Y by A6,Th39; t~ in Y[~]; hence thesis by A5; end; hence thesis by A2; end; theorem Th41: for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity(SF) holds (meet Y)~ = meet (Y[~]) proof let Y be non empty Subset-Family of [:X,X:]; assume A1: Y c= subbasis_Pervin_uniformity(SF); thus (meet Y)~ c= meet (Y[~]) proof let x be object; assume A3: x in (meet Y)~; then consider a,b be object such that a in X and b in X and A4: [a,b] = x by ZFMISC_1:def 2; A5: [b,a] in meet Y by A3,A4,RELAT_1:def 7; Y is non empty; then consider y be object such that A6: y in Y; reconsider y as Element of Y by A6; reconsider z = y as Relation of X; A7: y~ in Y[~]; now let Z be set; assume A8: Z in Y[~]; then A9: Z in Y by A1,Th40; reconsider T = Z as Relation of X by A8; T in subbasis_Pervin_uniformity(SF) by A9,A1; then consider A be Element of SF such that A10: T = block_Pervin_uniformity(A); T~ = T by A10,Th39; then [b,a] in T~ by A9,A5,SETFAM_1:def 1; hence [a,b] in Z by RELAT_1:def 7; end; hence thesis by A7,A4,SETFAM_1:def 1; end; let x be object; assume A11: x in meet (Y[~]); then consider a,b be object such that a in X and b in X and A12: [a,b] = x by ZFMISC_1:def 2; now let Z be set; assume A13: Z in Y; then reconsider T = Z as Relation of X; reconsider R = T as Element of Y by A13; R~ = T~; then T~ in Y[~]; then [a,b] in T~ by A11,A12,SETFAM_1:def 1; hence [b,a] in Z by RELAT_1:def 7; end; then [b,a] in meet Y by SETFAM_1:def 1; hence thesis by A12,RELAT_1:def 7; end; theorem Th42: for Y being non empty Subset-Family of [:X,X:] st Y c= subbasis_Pervin_uniformity(SF) holds meet Y = (meet Y)~ proof let Y be non empty Subset-Family of [:X,X:]; assume A1: Y c= subbasis_Pervin_uniformity(SF); then meet (Y[~]) = meet Y by Th40; hence thesis by A1,Th41; end; theorem Th43: basis_Pervin_uniformity(SF) is axiom_UP2 proof let B1 be Element of basis_Pervin_uniformity(SF); B1 in FinMeetCl(subbasis_Pervin_uniformity(SF)); then consider Y being Subset-Family of [:X,X:] such that A1: Y c= subbasis_Pervin_uniformity(SF) and Y is finite and A2: B1 = Intersect Y by CANTOR_1:def 3; per cases; suppose Y is empty; then A3: B1 = [:X,X:] by A2,SETFAM_1:def 9; B1 c= B1~ proof let x be object; assume x in B1; then consider a,b be object such that A4: a in X and A5: b in X and A6: x = [a,b] by A2,ZFMISC_1:def 2; [b,a] in B1 by A3,A4,A5,ZFMISC_1:def 2; hence thesis by A6,RELAT_1:def 7; end; hence thesis; end; suppose A9: Y is non empty; then A10: B1 = meet Y by A2,SETFAM_1:def 9; set Y2 = Y[~]; Y[~] = Y by A1,A9,Th40; then reconsider B2 = meet Y2 as Element of basis_Pervin_uniformity(SF) by A9,A2,SETFAM_1:def 9; B2 c= B1~ proof let x be object; assume x in B2; then x in meet Y by A1,A9,Th40; hence thesis by A10,A1,A9,Th42; end; hence thesis; end; end; theorem Th44: basis_Pervin_uniformity(SF) is axiom_UP3 proof for B1 being Element of basis_Pervin_uniformity(SF) ex B2 being Element of basis_Pervin_uniformity(SF) st B2 [*] B2 c= B1 proof let B1 be Element of basis_Pervin_uniformity(SF); B1 in FinMeetCl(subbasis_Pervin_uniformity(SF)); then consider Y being Subset-Family of [:X,X:] such that A1: Y c= subbasis_Pervin_uniformity(SF) and Y is finite and A2: B1 = Intersect Y by CANTOR_1:def 3; per cases; suppose Y is empty; then A3: B1 = [:X,X:] by A2,SETFAM_1:def 9; take B1; thus thesis by A3; end; suppose A4: Y is non empty; then A5: B1 = meet Y by A2,SETFAM_1:def 9; reconsider B2 = B1 as Element of basis_Pervin_uniformity(SF); take B2; B2 * B2 c= B1 proof let t be object; assume A6: t in B2 * B2; then consider a,b be object such that A10: t = [a,b] by RELAT_1:def 1; consider c be object such that A11: [a,c] in B1 and A12: [c,b] in B1 by A6,A10,RELAT_1:def 8; t in B1 proof for Z be set st Z in Y holds t in Z proof let Z be set; assume A13: Z in Y; then Z in the set of all block_Pervin_uniformity(O) where O is Element of SF by A1; then consider O be Element of SF such that A14: Z = block_Pervin_uniformity(O); [a,c] in meet Y by A4,A2,SETFAM_1:def 9,A11; then A15: [a,c] in block_Pervin_uniformity(O) by A14,A13,SETFAM_1:def 1; [c,b] in block_Pervin_uniformity(O) by A12,A5,A14,A13,SETFAM_1:def 1; then A16: [a,b] in (block_Pervin_uniformity(O)) * (block_Pervin_uniformity(O)) by A15,RELAT_1:def 8; (block_Pervin_uniformity(O)) * (block_Pervin_uniformity(O)) c= block_Pervin_uniformity(O) by Th35; hence thesis by A14,A10,A16; end; hence thesis by A5,A4,SETFAM_1:def 1; end; hence thesis; end; hence thesis; end; end; hence thesis; end; Th45: ex US being strict UniformSpace st the carrier of US = X & the entourages of US = <.basis_Pervin_uniformity(SF).] proof basis_Pervin_uniformity(SF) is quasi_basis & basis_Pervin_uniformity(SF) is axiom_UP1 & basis_Pervin_uniformity(SF) is axiom_UP2 & basis_Pervin_uniformity(SF) is axiom_UP3 by Th37,Th38,Th44,Th43; hence thesis by Th7; end; definition let X be set, SF be Subset-Family of X; func Pervin_uniform_space SF -> strict UniformSpace equals UniformSpaceStr(# X, <.basis_Pervin_uniformity(SF).] #); coherence proof ex US be strict UniformSpace st the carrier of US = X & the entourages of US = <.basis_Pervin_uniformity(SF).] by Th45; hence thesis; end; end;