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