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 A1:
( G is Cover of (TopSpaceMetr N) & G is open & 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 assume A2:
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: contradictiondefpred S1[
set ,
set ]
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 ) ) );
A3:
for
e being
set st
e in NAT holds
ex
u being
set st
(
u in the
carrier of
N &
S1[
e,
u] )
ex
f being
Function of
NAT ,the
carrier of
N st
for
e being
set st
e in NAT holds
S1[
e,
f . e]
from FUNCT_2:sch 1(A3);
then consider f being
Function of
NAT ,the
carrier of
N such that A5:
for
e being
set 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 ) ) )
;
set TM =
TopSpaceMetr N;
A6:
TopSpaceMetr N = TopStruct(# the
carrier of
N,
(Family_open_set N) #)
by PCOMPS_1:def 6;
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 A7:
for
B being
Subset of
(TopSpaceMetr N) holds
(
B in F iff
S2[
B] )
from SUBSET_1:sch 3();
A8:
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 ) } <> {}
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] } ;
A9:
{ x where x is Point of N : S3[x] } is
Subset of
N
from DOMAIN_1:sch 7();
then A10:
{ x where x is Point of N : S3[x] } in F
by A6, A7;
reconsider F =
F as
Subset-Family of
(TopSpaceMetr N) ;
set G1 =
clf F;
reconsider B0 =
{ x where x is Point of N : S3[x] } as
Subset of
(TopSpaceMetr N) by A6, A9;
A11:
Cl B0 in clf F
by A10, PCOMPS_1:def 3;
A12:
clf F is
closed
by PCOMPS_1:14;
(
clf F <> {} & ( for
Gd being
set st
Gd <> {} &
Gd c= clf F &
Gd is
finite holds
meet Gd <> {} ) )
proof
thus
clf F <> {}
by A11;
:: 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 A13:
H <> {}
and A14:
H c= clf F
and A15:
H is
finite
;
:: thesis: meet H <> {}
reconsider H =
H as
Subset-Family of
(TopSpaceMetr N) by A14, TOPS_2:3;
H is
c=-linear
proof
let B,
C be
set ;
:: according to ORDINAL1:def 9 :: thesis: ( not B in H or not C in H or not R7(B,C) )
assume A16:
(
B in H &
C in H )
;
:: thesis: R7(B,C)
then reconsider B =
B as
Subset of
(TopSpaceMetr N) ;
reconsider C =
C as
Subset of
(TopSpaceMetr N) by A16;
consider V being
Subset of
(TopSpaceMetr N) such that A17:
(
B = Cl V &
V in F )
by A14, A16, PCOMPS_1:def 3;
consider W being
Subset of
(TopSpaceMetr N) such that A18:
(
C = Cl W &
W in F )
by A14, A16, PCOMPS_1:def 3;
consider p being
Element of
NAT such that A19:
V = { x where x is Point of N : ex n being Element of NAT st
( p <= n & x = f . n ) }
by A7, A17;
consider q being
Element of
NAT such that A20:
W = { x where x is Point of N : ex n being Element of NAT st
( q <= n & x = f . n ) }
by A7, A18;
(
V c= W or
W c= V )
then
(
B c= C or
C c= B )
by A17, A18, PRE_TOPC:49;
hence
R7(
B,
C)
by XBOOLE_0:def 9;
:: thesis: verum
end;
then consider m being
set such that A27:
m in H
and A28:
for
C being
set st
C in H holds
m c= C
by A13, A15, FINSET_1:30;
A29:
m c= meet H
by A13, A28, SETFAM_1:6;
reconsider m =
m as
Subset of
(TopSpaceMetr N) by A27;
consider A being
Subset of
(TopSpaceMetr N) such that A30:
(
m = Cl A &
A in F )
by A14, A27, PCOMPS_1:def 3;
A <> {}
by A7, A8, A30;
then
m <> {}
by A30, PRE_TOPC:48, XBOOLE_1:3;
hence
meet H <> {}
by A29;
:: thesis: verum
end; then
clf F is
centered
by FINSET_1:def 3;
then
meet (clf F) <> {}
by A1, A12, COMPTS_1:13;
then consider c being
Point of
(TopSpaceMetr N) such that A31:
c in meet (clf F)
by SUBSET_1:10;
reconsider c =
c as
Point of
N by A6;
consider Ge being
Subset of
(TopSpaceMetr N) such that A32:
(
c in Ge &
Ge in G )
by A1, PCOMPS_1:5;
reconsider Ge =
Ge as
Subset of
(TopSpaceMetr N) ;
Ge is
open
by A1, A32, TOPS_2:def 1;
then consider r being
real number such that A33:
(
r > 0 &
Ball c,
r c= Ge )
by A32, TOPMETR:22;
reconsider r =
r as
Real by XREAL_0:def 1;
A34:
r / 2
> 0
by A33, XREAL_1:217;
then consider n being
Element of
NAT such that A35:
(
n > 0 & 1
/ n < r / 2 )
by Th2;
n <= n + 1
by NAT_1:11;
then
1
/ n >= 1
/ (n + 1)
by A35, XREAL_1:87;
then A36:
1
/ (n + 1) < r / 2
by A35, XXREAL_0:2;
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();
A37:
the
carrier of
(TopSpaceMetr N) = the
carrier of
N
by TOPMETR:16;
then
B2 in F
by A7;
then
Cl B2 in clf F
by PCOMPS_1:def 3;
then A38:
c in Cl B2
by A31, SETFAM_1:def 1;
reconsider Q1 =
Ball c,
(r / 2) as
Subset of
(TopSpaceMetr N) by TOPMETR:16;
A39:
c in Q1
by A34, GOBOARD6:4;
Q1 is
open
by TOPMETR:21;
then
B2 meets Q1
by A38, A39, TOPS_1:39;
then consider x being
set such that A40:
(
x in B2 &
x in Q1 )
by XBOOLE_0:3;
consider y being
Point of
N such that A41:
(
x = y & ex
n2 being
Element of
NAT st
(
n <= n2 &
y = f . n2 ) )
by A37, A40;
A42:
dist c,
y < r / 2
by A40, A41, METRIC_1:12;
r / 1
> r / 2
by A33, XREAL_1:78;
then
dist c,
y < r
by A42, XXREAL_0:2;
then A43:
y in Ball c,
r
by METRIC_1:12;
consider n2 being
Element of
NAT such that A44:
(
n <= n2 &
y = f . n2 )
by A41;
consider w2 being
Element of
N such that A45:
(
dist y,
w2 < 1
/ (n2 + 1) & ( for
Ga being
Subset of
(TopSpaceMetr N) holds
( not
y in Ga or not
w2 in Ga or not
Ga in G ) ) )
by A5, A44;
n + 1
<= n2 + 1
by A44, XREAL_1:9;
then
1
/ (n + 1) >= 1
/ (n2 + 1)
by XREAL_1:120;
then
dist y,
w2 < 1
/ (n + 1)
by A45, XXREAL_0:2;
then A46:
dist y,
w2 < r / 2
by A36, XXREAL_0:2;
A47:
dist c,
w2 <= (dist c,y) + (dist y,w2)
by METRIC_1:4;
A48:
(dist c,y) + (dist y,w2) < (r / 2) + (dist y,w2)
by A42, XREAL_1:8;
A49:
(r / 2) + (dist y,w2) < (r / 2) + (r / 2)
by A46, XREAL_1:8;
dist c,
w2 < (r / 2) + (dist y,w2)
by A47, A48, XXREAL_0:2;
then
dist c,
w2 < (r / 2) + (r / 2)
by A49, XXREAL_0:2;
then
w2 in Ball c,
r
by METRIC_1:12;
hence
contradiction
by A32, A33, A43, A45;
:: 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