let MS be PseudoMetricSpace; :: thesis: ex US being strict UniformSpace st US = uniformity_induced_by MS
set US = uniformity_induced_by MS;
set cB = fundamental_system_of_entourages MS;
now :: thesis: ( fundamental_system_of_entourages MS is quasi_basis & fundamental_system_of_entourages MS is axiom_UP1 & fundamental_system_of_entourages MS is axiom_UP2 & fundamental_system_of_entourages MS is axiom_UP3 )
now :: thesis: for B1, B2 being Element of fundamental_system_of_entourages MS ex B being Element of fundamental_system_of_entourages MS st B c= B1 /\ B2
let B1, B2 be Element of fundamental_system_of_entourages MS; :: thesis: ex B being Element of fundamental_system_of_entourages MS st B c= B1 /\ B2
B1 in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
then consider r1 being positive Real such that
A1: B1 = fundamental_element_of_entourages (MS,r1) ;
B2 in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
then consider r2 being 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 } ;
{ [x,y] where x, y is Element of MS : dist (x,y) <= r3 } = fundamental_element_of_entourages (MS,r3) ;
then { [x,y] where x, y is Element of MS : dist (x,y) <= r3 } in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
then reconsider B3 = { [x,y] where x, y is Element of the carrier of MS : dist (x,y) <= r3 } as Element of fundamental_system_of_entourages MS ;
B3 c= B1 /\ B2
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B3 or t in B1 /\ B2 )
assume t in B3 ; :: thesis: t in B1 /\ B2
then consider x, y being 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 t in B1 /\ B2 by A5, XBOOLE_0:def 4; :: thesis: verum
end;
hence ex B being Element of fundamental_system_of_entourages MS st B c= B1 /\ B2 ; :: thesis: verum
end;
hence fundamental_system_of_entourages MS is quasi_basis ; :: thesis: ( fundamental_system_of_entourages MS is axiom_UP1 & fundamental_system_of_entourages MS is axiom_UP2 & fundamental_system_of_entourages MS is axiom_UP3 )
now :: thesis: for B being Element of fundamental_system_of_entourages MS holds id the carrier of MS c= B
let B be Element of fundamental_system_of_entourages MS; :: thesis: id the carrier of MS c= B
B in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
then consider r being positive Real such that
A6: B = fundamental_element_of_entourages (MS,r) ;
now :: thesis: for t being object st t in id the carrier of MS holds
t in B
let t be object ; :: thesis: ( t in id the carrier of MS implies t in B )
assume A7: t in id the carrier of MS ; :: thesis: t in B
then consider t1, t2 being 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 = t1, t2 = t2 as Element of MS ;
dist (t1,t1) <= r by METRIC_1:1;
hence t in B by A9, A8, A6; :: thesis: verum
end;
hence id the carrier of MS c= B ; :: thesis: verum
end;
hence fundamental_system_of_entourages MS is axiom_UP1 ; :: thesis: ( fundamental_system_of_entourages MS is axiom_UP2 & fundamental_system_of_entourages MS is axiom_UP3 )
now :: thesis: for B1 being Element of fundamental_system_of_entourages MS ex B2 being Element of fundamental_system_of_entourages MS st B2 c= B1 ~
let B1 be Element of fundamental_system_of_entourages MS; :: thesis: ex B2 being Element of fundamental_system_of_entourages MS st B2 c= B1 ~
B1 in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
then consider r being positive Real such that
A10: B1 = fundamental_element_of_entourages (MS,r) ;
B1 c= B1 ~
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B1 or t in B1 ~ )
assume A11: t in B1 ; :: thesis: t in B1 ~
then consider x, y being 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 ; :: according to TARSKI:def 3 :: thesis: ( not u in { [y,x] where x, y is Element of MS : dist (x,y) <= r } or u in [: the carrier of MS, the carrier of MS:] )
assume u in { [y,x] where x, y is Element of MS : dist (x,y) <= r } ; :: thesis: u in [: the carrier of MS, the carrier of MS:]
then ex u1, u2 being Element of MS st
( u = [u2,u1] & dist (u1,u2) <= r ) ;
hence u in [: the carrier of MS, the carrier of MS:] ; :: thesis: verum
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 ; :: according to TARSKI:def 3 :: thesis: ( not u in R1 ~ or u in R2 )
assume A15: u in R1 ~ ; :: thesis: u in R2
consider u1, u2 being 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 being 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 u in R2 by A16, A18; :: thesis: verum
end;
R2 c= R1 ~
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in R2 or u in R1 ~ )
assume A19: u in R2 ; :: thesis: u in R1 ~
then consider u1, u2 being object such that
A20: u = [u1,u2] by RELAT_1:def 1;
consider v1, v2 being 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 u in R1 ~ by A20, A21, RELAT_1:def 7; :: thesis: verum
end;
hence R1 ~ = { [y,x] where x, y is Element of MS : dist (x,y) <= r } by A14; :: thesis: verum
end;
consider x1, y1 being Element of MS such that
A23: [x,y] = [x1,y1] and
A24: dist (x1,y1) <= r by A10, A11, A12;
thus t in B1 ~ by A24, A13, A12, A23; :: thesis: verum
end;
hence ex B2 being Element of fundamental_system_of_entourages MS st B2 c= B1 ~ ; :: thesis: verum
end;
hence fundamental_system_of_entourages MS is axiom_UP2 ; :: thesis: fundamental_system_of_entourages MS is axiom_UP3
now :: thesis: for B1 being Element of fundamental_system_of_entourages MS ex B2 being Element of fundamental_system_of_entourages MS st B2 * B2 c= B1
let B1 be Element of fundamental_system_of_entourages MS; :: thesis: ex B2 being Element of fundamental_system_of_entourages MS st B2 * B2 c= B1
B1 in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
then consider r being 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 ;
{ [x,y] where x, y is Element of MS : dist (x,y) <= r / 2 } = fundamental_element_of_entourages (MS,r2) ;
then { [x,y] where x, y is Element of MS : dist (x,y) <= r / 2 } in fundamental_system_of_entourages MS ;
then reconsider B2 = { [x,y] where x, y is Element of MS : dist (x,y) <= r / 2 } as Element of fundamental_system_of_entourages MS ;
reconsider R1 = B2 as Relation of the carrier of MS ;
B2 * B2 c= B1
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in B2 * B2 or t in B1 )
assume t in B2 * B2 ; :: thesis: t in B1
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 being 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 being Element of MS such that
A31: [x,z] in R1 and
A32: [z,y] in R1 by A30;
consider x1, z1 being 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 being 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 t in B1 by A29, A25; :: thesis: verum
end;
hence ex B2 being Element of fundamental_system_of_entourages MS st B2 * B2 c= B1 ; :: thesis: verum
end;
hence fundamental_system_of_entourages MS is axiom_UP3 ; :: thesis: verum
end;
then ex US being strict UniformSpace st
( the carrier of US = the carrier of MS & the entourages of US = <.(fundamental_system_of_entourages MS).] ) by Th7;
hence ex US being strict UniformSpace st US = uniformity_induced_by MS ; :: thesis: verum