:: Uniform Space
:: by Roland Coghetto
::
:: Received June 30, 2016
:: Copyright (c) 2016-2026 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 = {{}}
by ZFMISC_1:2,EQREL_1:def 4,YELLOW_9:16;
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; :: redefines uniformity_induced_by (UNIFORM3, definition)
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; :: redefines uniformity_induced_by (UNIFORM3, definition)
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;