let N be non empty MetrSpace; :: thesis: for G being Subset-Family of (TopSpaceMetr N) st G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact holds
ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )
let G be Subset-Family of (TopSpaceMetr N); :: thesis: ( G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact implies ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) ) )
assume that
A1: G is Cover of (TopSpaceMetr N) and
A2: G is open and
A3: TopSpaceMetr N is compact ; :: thesis: ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )
now :: thesis: ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )
set TM = TopSpaceMetr N;
defpred S1[ object , object ] means for n being Element of NAT
for w1 being Element of N st n = $1 & w1 = $2 holds
ex w2 being Element of N st
( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) );
A4: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def 5;
assume A5: for r being Real holds
( not r > 0 or ex w1, w2 being Element of N st
( dist (w1,w2) < r & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ) ; :: thesis: contradiction
A6: for e being object st e in NAT holds
ex u being object st
( u in the carrier of N & S1[e,u] )
proof
let e be object ; :: thesis: ( e in NAT implies ex u being object st
( u in the carrier of N & S1[e,u] ) )
assume e in NAT ; :: thesis: ex u being object st
( u in the carrier of N & S1[e,u] )
then reconsider m = e as Element of NAT ;
set r = 1 / (m + 1);
consider w1, w2 being Element of N such that
A7: ( dist (w1,w2) < 1 / (m + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) by A5;
for n being Element of NAT
for w4 being Element of N st n = e & w4 = w1 holds
ex w5 being Element of N st
( dist (w4,w5) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w4 in Ga or not w5 in Ga or not Ga in G ) ) ) by A7;
hence ex u being object st
( u in the carrier of N & S1[e,u] ) ; :: thesis: verum
end;
ex f being sequence of the carrier of N st
for e being object st e in NAT holds
S1[e,f . e] from FUNCT_2:sch 1(A6);
then consider f being sequence of the carrier of N such that
A8: for e being object st e in NAT holds
for n being Element of NAT
for w1 being Element of N st n = e & w1 = f . e holds
ex w2 being Element of N st
( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds
( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ;
defpred S2[ Subset of (TopSpaceMetr N)] means ex p being Element of NAT st $1 = { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } ;
consider F being Subset-Family of (TopSpaceMetr N) such that
A9: for B being Subset of (TopSpaceMetr N) holds
( B in F iff S2[B] ) from SUBSET_1:sch 3();
defpred S3[ set ] means ex n being Element of NAT st
( 0 <= n & $1 = f . n );
set B0 = { x where x is Point of N : S3[x] } ;
A10: { x where x is Point of N : S3[x] } is Subset of N from DOMAIN_1:sch 7();
then A11: { x where x is Point of N : S3[x] } in F by A4, A9;
A12: for p being Element of NAT holds { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } <> {}
proof
let p be Element of NAT ; :: thesis: { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } <> {}
f . p in { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } ;
hence { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } <> {} ; :: thesis: verum
end;
reconsider B0 = { x where x is Point of N : S3[x] } as Subset of (TopSpaceMetr N) by A4, A10;
reconsider F = F as Subset-Family of (TopSpaceMetr N) ;
set G1 = clf F;
A13: Cl B0 in clf F by A11, PCOMPS_1:def 2;
( clf F <> {} & ( for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds
meet Gd <> {} ) )
proof
thus clf F <> {} by A13; :: thesis: for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds
meet Gd <> {}
let H be set ; :: thesis: ( H <> {} & H c= clf F & H is finite implies meet H <> {} )
assume that
A14: H <> {} and
A15: H c= clf F and
A16: H is finite ; :: thesis: meet H <> {}
reconsider H = H as Subset-Family of (TopSpaceMetr N) by A15, TOPS_2:2;
H is c=-linear
proof
let B, C be set ; :: according to ORDINAL1:def 8 :: thesis: ( not B in H or not C in H or B,C are_c=-comparable )
assume that
A17: B in H and
A18: C in H ; :: thesis: B,C are_c=-comparable
reconsider B = B as Subset of (TopSpaceMetr N) by A17;
consider V being Subset of (TopSpaceMetr N) such that
A19: B = Cl V and
A20: V in F by A15, A17, PCOMPS_1:def 2;
consider p being Element of NAT such that
A21: V = { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) } by A9, A20;
reconsider C = C as Subset of (TopSpaceMetr N) by A18;
consider W being Subset of (TopSpaceMetr N) such that
A22: C = Cl W and
A23: W in F by A15, A18, PCOMPS_1:def 2;
consider q being Element of NAT such that
A24: W = { x where x is Point of N : ex n being Element of NAT st
( q <= n & x = f . n ) } by A9, A23;
now :: thesis: ( ( q <= p & V c= W ) or ( p <= q & W c= V ) )
per cases ( q <= p or p <= q ) ;
case A25: q <= p ; :: thesis: V c= W
thus V c= W :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in V or y in W )
assume y in V ; :: thesis: y in W
then consider x being Point of N such that
A26: y = x and
A27: ex n being Element of NAT st
( p <= n & x = f . n ) by A21;
consider n being Element of NAT such that
A28: p <= n and
A29: x = f . n by A27;
q <= n by A25, A28, XXREAL_0:2;
hence y in W by A24, A26, A29; :: thesis: verum
end;
end;
case A30: p <= q ; :: thesis: W c= V
thus W c= V :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in W or y in V )
assume y in W ; :: thesis: y in V
then consider x being Point of N such that
A31: y = x and
A32: ex n being Element of NAT st
( q <= n & x = f . n ) by A24;
consider n being Element of NAT such that
A33: q <= n and
A34: x = f . n by A32;
p <= n by A30, A33, XXREAL_0:2;
hence y in V by A21, A31, A34; :: thesis: verum
end;
end;
end;
end;
then ( B c= C or C c= B ) by A19, A22, PRE_TOPC:19;
hence B,C are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum
end;
then consider m being set such that
A35: m in H and
A36: for C being set st C in H holds
m c= C by A14, A16, FINSET_1:11;
A37: m c= meet H by A14, A36, SETFAM_1:5;
reconsider m = m as Subset of (TopSpaceMetr N) by A35;
consider A being Subset of (TopSpaceMetr N) such that
A38: m = Cl A and
A39: A in F by A15, A35, PCOMPS_1:def 2;
A <> {} by A9, A12, A39;
then m <> {} by A38, PRE_TOPC:18, XBOOLE_1:3;
hence meet H <> {} by A37; :: thesis: verum
end;
then ( clf F is closed & clf F is centered ) by FINSET_1:def 3, PCOMPS_1:11;
then meet (clf F) <> {} by A3, COMPTS_1:4;
then consider c being Point of (TopSpaceMetr N) such that
A40: c in meet (clf F) by SUBSET_1:4;
reconsider c = c as Point of N by A4;
consider Ge being Subset of (TopSpaceMetr N) such that
A41: c in Ge and
A42: Ge in G by A1, PCOMPS_1:3;
reconsider Ge = Ge as Subset of (TopSpaceMetr N) ;
Ge is open by A2, A42, TOPS_2:def 1;
then consider r being Real such that
A43: r > 0 and
A44: Ball (c,r) c= Ge by A41, TOPMETR:15;
reconsider r = r as Real ;
consider n being Nat such that
A45: n > 0 and
A46: 1 / n < r / 2 by A43, Th1, XREAL_1:215;
reconsider Q1 = Ball (c,(r / 2)) as Subset of (TopSpaceMetr N) by TOPMETR:12;
A47: Q1 is open by TOPMETR:14;
defpred S4[ set ] means ex n2 being Element of NAT st
( n <= n2 & $1 = f . n2 );
reconsider B2 = { x where x is Point of (TopSpaceMetr N) : S4[x] } as Subset of (TopSpaceMetr N) from DOMAIN_1:sch 7();
A48: n in NAT by ORDINAL1:def 12;
A49: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12;
then B2 in F by A9, A48;
then Cl B2 in clf F by PCOMPS_1:def 2;
then A50: c in Cl B2 by A40, SETFAM_1:def 1;
c in Q1 by A43, GOBOARD6:1, XREAL_1:215;
then B2 meets Q1 by A50, A47, TOPS_1:12;
then consider x being object such that
A51: x in B2 and
A52: x in Q1 by XBOOLE_0:3;
consider y being Point of N such that
A53: x = y and
A54: ex n2 being Element of NAT st
( n <= n2 & y = f . n2 ) by A49, A51;
A55: dist (c,y) < r / 2 by A52, A53, METRIC_1:11;
1 / n >= 1 / (n + 1) by A45, NAT_1:11, XREAL_1:85;
then A56: 1 / (n + 1) < r / 2 by A46, XXREAL_0:2;
consider n2 being Element of NAT such that
A57: n <= n2 and
A58: y = f . n2 by A54;
consider w2 being Element of N such that
A59: dist (y,w2) < 1 / (n2 + 1) and
A60: for Ga being Subset of (TopSpaceMetr N) holds
( not y in Ga or not w2 in Ga or not Ga in G ) by A8, A58;
n + 1 <= n2 + 1 by A57, XREAL_1:7;
then 1 / (n + 1) >= 1 / (n2 + 1) by XREAL_1:118;
then dist (y,w2) < 1 / (n + 1) by A59, XXREAL_0:2;
then dist (y,w2) < r / 2 by A56, XXREAL_0:2;
then A61: (r / 2) + (dist (y,w2)) < (r / 2) + (r / 2) by XREAL_1:6;
r / 1 > r / 2 by A43, XREAL_1:76;
then dist (c,y) < r by A55, XXREAL_0:2;
then A62: y in Ball (c,r) by METRIC_1:11;
( dist (c,w2) <= (dist (c,y)) + (dist (y,w2)) & (dist (c,y)) + (dist (y,w2)) < (r / 2) + (dist (y,w2)) ) by A55, METRIC_1:4, XREAL_1:6;
then dist (c,w2) < (r / 2) + (dist (y,w2)) by XXREAL_0:2;
then dist (c,w2) < (r / 2) + (r / 2) by A61, XXREAL_0:2;
then w2 in Ball (c,r) by METRIC_1:11;
hence contradiction by A42, A44, A62, A60; :: thesis: verum
end;
hence ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) ) ; :: thesis: verum