set TM = TopSpaceMetr M;
consider G being Subset-Family of (TopSpaceMetr M) such that
A1:
G c= F
and
A2:
G is Cover of (TopSpaceMetr M)
and
A3:
G is finite
by B1, B2, B3, COMPTS_1:def 1;
per cases
( [#] (TopSpaceMetr M) in G or not [#] (TopSpaceMetr M) in G )
;
suppose A5:
not
[#] (TopSpaceMetr M) in G
;
ex b1 being positive Real st
for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,b1) c= A )set cTM =
[#] (TopSpaceMetr M);
set FUNCS =
Funcs (
([#] (TopSpaceMetr M)),
REAL);
consider g being
FinSequence such that A6:
rng g = G
and
g is
one-to-one
by A3, FINSEQ_4:58;
defpred S1[
Nat,
set ,
set ]
means for
f1,
f2 being
Function of
(TopSpaceMetr M),
R^1 st
f1 = $2 &
f2 = $3 &
f1 is
continuous holds
(
f2 is
continuous & ex
A being non
empty Subset of
(TopSpaceMetr M) st
(
A ` = g . ($1 + 1) & ( for
x being
Point of
(TopSpaceMetr M) holds
f2 . x = max (
(f1 . x),
((dist_min A) . x)) ) ) );
not
union G is
empty
by A2, SETFAM_1:45;
then A7:
not
g is
empty
by A6, ZFMISC_1:2;
then A8:
len g >= 1
by NAT_1:14;
then A9:
1
in dom g
by FINSEQ_3:25;
then A10:
g . 1
in rng g
by FUNCT_1:def 3;
then reconsider g1 =
g . 1 as
Subset of
(TopSpaceMetr M) by A6;
A11:
(g1 `) ` <> [#] (TopSpaceMetr M)
by A5, A6, A9, FUNCT_1:def 3;
g1 is
open
by B2, A1, A6, A10, TOPS_2:def 1;
then reconsider g19 =
g1 ` as non
empty closed Subset of
(TopSpaceMetr M) by A11;
reconsider Dg19 =
dist_min g19 as
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL)
by FUNCT_2:8, TOPMETR:17;
A12:
for
n being
Nat st 1
<= n &
n < len g holds
for
x being
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL) ex
y being
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL) st
S1[
n,
x,
y]
proof
let n be
Nat;
( 1 <= n & n < len g implies for x being Element of Funcs (([#] (TopSpaceMetr M)),REAL) ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y] )
assume that
1
<= n
and A13:
n < len g
;
for x being Element of Funcs (([#] (TopSpaceMetr M)),REAL) ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
let x be
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL);
ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
reconsider fx =
x as
Function of
(TopSpaceMetr M),
R^1 by TOPMETR:17;
per cases
( not fx is continuous or fx is continuous )
;
suppose A15:
fx is
continuous
;
ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
( 1
<= n + 1 &
n + 1
<= len g )
by A13, NAT_1:11, NAT_1:13;
then A16:
n + 1
in dom g
by FINSEQ_3:25;
then
g . (n + 1) in G
by A6, FUNCT_1:def 3;
then reconsider A =
g . (n + 1) as
Subset of
(TopSpaceMetr M) ;
(A `) ` <> [#] (TopSpaceMetr M)
by A5, A6, A16, FUNCT_1:def 3;
then reconsider A9 =
A ` as non
empty Subset of
(TopSpaceMetr M) ;
R^1 is
SubSpace of
R^1
by TSEP_1:2;
then consider h being
continuous Function of
(TopSpaceMetr M),
R^1 such that A17:
for
x being
Point of
(TopSpaceMetr M) holds
h . x = max (
(fx . x),
((dist_min A9) . x))
by A15, TOPGEN_5:50;
reconsider y =
h as
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL)
by FUNCT_2:8, TOPMETR:17;
take
y
;
S1[n,x,y]let f1,
f2 be
Function of
(TopSpaceMetr M),
R^1;
( f1 = x & f2 = y & f1 is continuous implies ( f2 is continuous & ex A being non empty Subset of (TopSpaceMetr M) st
( A ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A) . x)) ) ) ) )assume that A18:
f1 = x
and A19:
f2 = y
and
f1 is
continuous
;
( f2 is continuous & ex A being non empty Subset of (TopSpaceMetr M) st
( A ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A) . x)) ) ) )thus
f2 is
continuous
by A19;
ex A being non empty Subset of (TopSpaceMetr M) st
( A ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A) . x)) ) )take
A9
;
( A9 ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A9) . x)) ) )thus
(
A9 ` = g . (n + 1) & ( for
x being
Point of
(TopSpaceMetr M) holds
f2 . x = max (
(f1 . x),
((dist_min A9) . x)) ) )
by A17, A18, A19;
verum
end; consider p being
FinSequence of
Funcs (
([#] (TopSpaceMetr M)),
REAL)
such that A20:
len p = len g
and A21:
(
p /. 1
= Dg19 or
len g = 0 )
and A22:
for
n being
Nat st 1
<= n &
n < len g holds
S1[
n,
p /. n,
p /. (n + 1)]
from NAT_2:sch 1(A12);
A23:
len p in dom p
by A8, A20, FINSEQ_3:25;
p /. (len p) is
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL)
;
then reconsider pL =
p /. (len p) as
Function of
(TopSpaceMetr M),
R^1 by TOPMETR:17;
reconsider rngPL =
rng pL as
Subset of
R^1 by RELAT_1:def 19;
set cRpL =
[#] rngPL;
A24:
[#] rngPL = rng pL
by WEIERSTR:def 1;
A25:
dom p = dom g
by A20, FINSEQ_3:29;
defpred S2[
Nat]
means for
f being
Function of
(TopSpaceMetr M),
R^1 st $1
in dom p &
f = p /. $1 holds
(
f is
continuous & ( for
j being
Nat for
h being
Function of
(TopSpaceMetr M),
R^1 st
j <= $1 &
j in dom p &
h = p /. j holds
for
x being
Point of
(TopSpaceMetr M) holds
h . x <= f . x ) );
A26:
for
n being
Nat st
S2[
n] holds
S2[
n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
assume A27:
S2[
n]
;
S2[n + 1]
let f be
Function of
(TopSpaceMetr M),
R^1;
( n + 1 in dom p & f = p /. (n + 1) implies ( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) ) )
assume that A28:
n + 1
in dom p
and A29:
f = p /. (n + 1)
;
( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) )
per cases
( n = 0 or n > 0 )
;
suppose A30:
n = 0
;
( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) )hence
f is
continuous
by A7, A21, A29;
for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . xlet j be
Nat;
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . xlet g be
Function of
(TopSpaceMetr M),
R^1;
( j <= n + 1 & j in dom p & g = p /. j implies for x being Point of (TopSpaceMetr M) holds g . x <= f . x )assume that A31:
j <= n + 1
and A32:
j in dom p
and A33:
g = p /. j
;
for x being Point of (TopSpaceMetr M) holds g . x <= f . x
1
<= j
by A32, FINSEQ_3:25;
hence
for
x being
Point of
(TopSpaceMetr M) holds
g . x <= f . x
by A29, A30, A31, A33, XXREAL_0:1;
verum end; suppose
n > 0
;
( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) )then reconsider n1 =
n - 1 as
Element of
NAT by NAT_1:20;
p /. n is
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL)
;
then reconsider pn =
p /. n as
Function of
(TopSpaceMetr M),
R^1 by TOPMETR:17;
n + 1
<= len p
by A28, FINSEQ_3:25;
then A34:
( 1
<= n1 + 1 &
n < len p )
by NAT_1:11, NAT_1:13;
then A35:
n in dom p
by FINSEQ_3:25;
then A36:
pn is
continuous
by A27;
hence
f is
continuous
by A20, A22, A29, A34;
for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . xconsider A being non
empty Subset of
(TopSpaceMetr M) such that
A ` = g . (n + 1)
and A37:
for
y being
Point of
(TopSpaceMetr M) holds
f . y = max (
(pn . y),
((dist_min A) . y))
by A20, A22, A29, A34, A36;
let j be
Nat;
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . xlet h be
Function of
(TopSpaceMetr M),
R^1;
( j <= n + 1 & j in dom p & h = p /. j implies for x being Point of (TopSpaceMetr M) holds h . x <= f . x )assume that A38:
j <= n + 1
and A39:
j in dom p
and A40:
h = p /. j
;
for x being Point of (TopSpaceMetr M) holds h . x <= f . xlet x be
Point of
(TopSpaceMetr M);
h . x <= f . xA41:
f . x = max (
(pn . x),
((dist_min A) . x))
by A37;
end;
end; A44:
S2[
0 ]
by FINSEQ_3:25;
A45:
for
n being
Nat holds
S2[
n]
from NAT_1:sch 2(A44, A26);
A46:
dom pL = [#] (TopSpaceMetr M)
by FUNCT_2:def 1;
then
pL .: ([#] (TopSpaceMetr M)) = rng pL
by RELAT_1:113;
then A47:
rngPL is
compact
by B1, A23, A45, WEIERSTR:9;
then A48:
[#] rngPL is
compact
by WEIERSTR:13;
reconsider cRpL =
[#] rngPL as non
empty real-bounded Subset of
REAL by A47, WEIERSTR:11, WEIERSTR:def 1;
set L =
lower_bound cRpL;
lower_bound cRpL in cRpL
by A48, RCOMP_1:14;
then consider x being
set such that A49:
x in dom pL
and A50:
pL . x = lower_bound cRpL
by A24, FUNCT_1:def 3;
union G = [#] (TopSpaceMetr M)
by A2, SETFAM_1:45;
then consider Y being
set such that A51:
x in Y
and A52:
Y in rng g
by A6, A49, TARSKI:def 4;
reconsider x =
x as
Point of
(TopSpaceMetr M) by A49;
consider j being
set such that A53:
j in dom g
and A54:
g . j = Y
by A52, FUNCT_1:def 3;
reconsider j =
j as
Nat by A53;
A55:
j <= len g
by A53, FINSEQ_3:25;
A56:
1
<= j
by A53, FINSEQ_3:25;
now 0 < lower_bound cRpLper cases
( j = 1 or j > 1 )
by A56, XXREAL_0:1;
suppose A57:
j = 1
;
0 < lower_bound cRpLthen
not
x in g19
by A51, A54, XBOOLE_0:def 5;
then
(dist_min g19) . x <> 0
by HAUSDORF:9;
then
(dist_min g19) . x > 0
by JORDAN1K:9;
hence
0 < lower_bound cRpL
by A20, A21, A23, A25, A45, A50, A53, A55, A57;
verum end; suppose A58:
j > 1
;
0 < lower_bound cRpLthen reconsider j1 =
j - 1 as
Element of
NAT by NAT_1:20;
(
p /. j1 is
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL) &
p /. j is
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL) )
;
then reconsider pj1 =
p /. j1,
pj =
p /. j as
Function of
(TopSpaceMetr M),
R^1 by TOPMETR:17;
j1 + 1
> 1
by A58;
then A59:
( 1
<= j1 &
j1 < len g )
by A55, NAT_1:13;
then
j1 in dom p
by A20, FINSEQ_3:25;
then A60:
pj1 is
continuous
by A45;
S1[
j1,
pj1,
pj]
by A22, A25, A45, A53, A59;
then consider A being non
empty Subset of
(TopSpaceMetr M) such that A61:
A ` = g . j
and A62:
for
x being
Point of
(TopSpaceMetr M) holds
pj . x = max (
(pj1 . x),
((dist_min A) . x))
by A60;
A ` is
open
by B2, A1, A6, A52, A54, A61, TOPS_2:def 1;
then A63:
A is
closed
by TOPS_1:3;
not
x in A
by A51, A54, A61, XBOOLE_0:def 5;
then
(dist_min A) . x <> 0
by A63, HAUSDORF:9;
then A64:
(dist_min A) . x > 0
by JORDAN1K:9;
pj . x = max (
(pj1 . x),
((dist_min A) . x))
by A62;
then
pj . x > 0
by A64, XXREAL_0:25;
hence
0 < lower_bound cRpL
by A20, A23, A25, A45, A50, A53, A55;
verum end; then reconsider L =
lower_bound cRpL as
positive Real ;
take
L
;
for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,L) c= A )let X be
Point of
M;
ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (X,L) c= A )defpred S3[
Nat]
means ( $1
in dom p & ( for
f1 being
Function of
(TopSpaceMetr M),
R^1 st
p /. $1
= f1 holds
f1 . X >= L ) );
pL . X in cRpL
by A24, A46, FUNCT_1:def 3;
then
S3[
len p]
by A8, A20, FINSEQ_3:25, XXREAL_2:3;
then A65:
ex
k being
Nat st
S3[
k]
;
consider k being
Nat such that A66:
S3[
k]
and A67:
for
n being
Nat st
S3[
n] holds
k <= n
from NAT_1:sch 5(A65);
A68:
1
<= k
by A66, FINSEQ_3:25;
A69:
k <= len p
by A66, FINSEQ_3:25;
per cases
( k = 1 or k > 1 )
by A68, XXREAL_0:1;
suppose A70:
k = 1
;
ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (X,L) c= A )take
g1
;
( g1 in F & Ball (X,L) c= g1 )thus
g1 in F
by A1, A6, A10;
Ball (X,L) c= g1let y be
set ;
TARSKI:def 3 ( not y in Ball (X,L) or y in g1 )assume A71:
y in Ball (
X,
L)
;
y in g1reconsider Y =
y as
Point of
M by A71;
A72:
dist (
X,
Y)
< L
by A71, METRIC_1:11;
assume
not
y in g1
;
contradictionthen
Y in g19
by XBOOLE_0:def 5;
then A73:
(dist_min g19) . X <= dist (
X,
Y)
by HAUSDORF:13;
(dist_min g19) . X >= L
by A7, A21, A66, A70;
hence
contradiction
by A72, A73, XXREAL_0:2;
verum end; suppose A74:
k > 1
;
ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (X,L) c= A )then reconsider k1 =
k - 1 as
Element of
NAT by NAT_1:20;
(
p /. k1 is
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL) &
p /. k is
Element of
Funcs (
([#] (TopSpaceMetr M)),
REAL) )
;
then reconsider pk1 =
p /. k1,
pk =
p /. k as
Function of
(TopSpaceMetr M),
R^1 by TOPMETR:17;
k1 + 1
> 1
by A74;
then A75:
( 1
<= k1 &
k1 < len g )
by A20, A69, NAT_1:13;
then
k1 in dom p
by A20, FINSEQ_3:25;
then A76:
pk1 is
continuous
by A45;
S1[
k1,
pk1,
pk]
by A22, A45, A66, A75;
then consider A being non
empty Subset of
(TopSpaceMetr M) such that A77:
A ` = g . k
and A78:
for
x being
Point of
(TopSpaceMetr M) holds
pk . x = max (
(pk1 . x),
((dist_min A) . x))
by A76;
take
A `
;
( A ` in F & Ball (X,L) c= A ` )
A ` in G
by A6, A25, A66, A77, FUNCT_1:def 3;
hence
A ` in F
by A1;
Ball (X,L) c= A ` let y be
set ;
TARSKI:def 3 ( not y in Ball (X,L) or y in A ` )assume A79:
y in Ball (
X,
L)
;
y in A ` reconsider Y =
y as
Point of
M by A79;
assume
not
y in A `
;
contradictionthen
Y in A
by XBOOLE_0:def 5;
then A80:
(dist_min A) . X <= dist (
X,
Y)
by HAUSDORF:13;
dist (
X,
Y)
< L
by A79, METRIC_1:11;
then A81:
(dist_min A) . X < L
by A80, XXREAL_0:2;
A82:
pk . X >= L
by A66;
pk . X = max (
(pk1 . X),
((dist_min A) . X))
by A78;
then
S3[
k1]
by A20, A75, A81, A82, FINSEQ_3:25, XXREAL_0:16;
then
k1 >= k1 + 1
by A67;
hence
contradiction
by NAT_1:13;
verum end; end;