:: HEINE semantic presentation
begin
theorem Th1: :: HEINE:1
for x, y being real number
for A being SubSpace of RealSpace
for p, q being Point of A st x = p & y = q holds
dist (p,q) = abs (x - y)
proof
let x, y be real number ; ::_thesis: for A being SubSpace of RealSpace
for p, q being Point of A st x = p & y = q holds
dist (p,q) = abs (x - y)
let A be SubSpace of RealSpace ; ::_thesis: for p, q being Point of A st x = p & y = q holds
dist (p,q) = abs (x - y)
let p, q be Point of A; ::_thesis: ( x = p & y = q implies dist (p,q) = abs (x - y) )
assume A1: ( x = p & y = q ) ; ::_thesis: dist (p,q) = abs (x - y)
A2: ( x is Real & y is Real ) by XREAL_0:def_1;
thus dist (p,q) = the distance of A . (p,q) by METRIC_1:def_1
.= real_dist . (x,y) by A1, METRIC_1:def_13, TOPMETR:def_1
.= abs (x - y) by A2, METRIC_1:def_12 ; ::_thesis: verum
end;
theorem Th2: :: HEINE:2
for n being Element of NAT
for seq being Real_Sequence st seq is V40() & rng seq c= NAT holds
n <= seq . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V40() & rng seq c= NAT holds
n <= seq . n
let seq be Real_Sequence; ::_thesis: ( seq is V40() & rng seq c= NAT implies n <= seq . n )
defpred S1[ Element of NAT ] means $1 <= seq . $1;
assume that
A1: seq is V40() and
A2: rng seq c= NAT ; ::_thesis: n <= seq . n
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: k <= seq . k ; ::_thesis: S1[k + 1]
k + 1 in NAT ;
then k + 1 in dom seq by FUNCT_2:def_1;
then seq . (k + 1) in rng seq by FUNCT_1:def_3;
then reconsider k9 = seq . (k + 1) as Element of NAT by A2;
seq . k < seq . (k + 1) by A1, SEQM_3:def_6;
then k < k9 by A4, XXREAL_0:2;
hence S1[k + 1] by NAT_1:13; ::_thesis: verum
end;
0 in NAT ;
then 0 in dom seq by FUNCT_2:def_1;
then seq . 0 in rng seq by FUNCT_1:def_3;
then A5: S1[ 0 ] by A2, NAT_1:2;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3);
hence n <= seq . n ; ::_thesis: verum
end;
definition
let seq be Real_Sequence;
let k be Element of NAT ;
funck to_power seq -> Real_Sequence means :Def1: :: HEINE:def 1
for n being Element of NAT holds it . n = k to_power (seq . n);
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = k to_power (seq . n)
proof
deffunc H1( Element of NAT ) -> Element of REAL = k to_power (seq . $1);
thus ex s being Real_Sequence st
for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = k to_power (seq . n) ) & ( for n being Element of NAT holds b2 . n = k to_power (seq . n) ) holds
b1 = b2
proof
let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = k to_power (seq . n) ) & ( for n being Element of NAT holds s2 . n = k to_power (seq . n) ) implies s1 = s2 )
assume that
A1: for n being Element of NAT holds s1 . n = k to_power (seq . n) and
A2: for n being Element of NAT holds s2 . n = k to_power (seq . n) ; ::_thesis: s1 = s2
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K77(s1,n) = K77(s2,n)
thus s1 . n = k to_power (seq . n) by A1
.= s2 . n by A2 ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines to_power HEINE:def_1_:_
for seq being Real_Sequence
for k being Element of NAT
for b3 being Real_Sequence holds
( b3 = k to_power seq iff for n being Element of NAT holds b3 . n = k to_power (seq . n) );
theorem Th3: :: HEINE:3
for seq being Real_Sequence st seq is divergent_to+infty holds
2 to_power seq is divergent_to+infty
proof
let seq be Real_Sequence; ::_thesis: ( seq is divergent_to+infty implies 2 to_power seq is divergent_to+infty )
assume A1: seq is divergent_to+infty ; ::_thesis: 2 to_power seq is divergent_to+infty
let r be Real; :: according to LIMFUNC1:def_4 ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not (2 to_power seq) . b2 <= r )
consider p being Element of NAT such that
A2: p > r by SEQ_4:3;
consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
p < seq . m by A1, LIMFUNC1:def_4;
take n ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not (2 to_power seq) . b1 <= r )
let m be Element of NAT ; ::_thesis: ( not n <= m or not (2 to_power seq) . m <= r )
assume m >= n ; ::_thesis: not (2 to_power seq) . m <= r
then p < seq . m by A3;
then A4: 2 to_power p < 2 to_power (seq . m) by POWER:39;
2 to_power p = 2 |^ p by POWER:41;
then p < 2 to_power (seq . m) by A4, NEWTON:86, XXREAL_0:2;
then r < 2 to_power (seq . m) by A2, XXREAL_0:2;
hence not (2 to_power seq) . m <= r by Def1; ::_thesis: verum
end;
theorem :: HEINE:4
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is compact
proof
let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is compact )
set M = Closed-Interval-MSpace (a,b);
assume A1: a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is compact
reconsider a = a, b = b as Real by XREAL_0:def_1;
set r = b - a;
now__::_thesis:_Closed-Interval-TSpace_(a,b)_is_compact
percases ( b - a = 0 or b - a > 0 ) by A1, XREAL_1:48;
suppose b - a = 0 ; ::_thesis: Closed-Interval-TSpace (a,b) is compact
then ( [.a,b.] = {a} & the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] ) by TOPMETR:18, XXREAL_1:17;
hence Closed-Interval-TSpace (a,b) is compact by COMPTS_1:18; ::_thesis: verum
end;
supposeA2: b - a > 0 ; ::_thesis: Closed-Interval-TSpace (a,b) is compact
A3: TopSpaceMetr (Closed-Interval-MSpace (a,b)) = Closed-Interval-TSpace (a,b) by TOPMETR:def_7;
assume not Closed-Interval-TSpace (a,b) is compact ; ::_thesis: contradiction
then not Closed-Interval-MSpace (a,b) is compact by A3, TOPMETR:def_5;
then consider F being Subset-Family of (Closed-Interval-MSpace (a,b)) such that
A4: F is being_ball-family and
A5: F is Cover of (Closed-Interval-MSpace (a,b)) and
A6: for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds
( not G c= F or not G is Cover of (Closed-Interval-MSpace (a,b)) or not G is finite ) by TOPMETR:16;
defpred S1[ Element of NAT , Element of REAL , Element of REAL ] means ( ( ( for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds
( not G c= F or not [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G or not G is finite ) ) implies $3 = $2 - ((b - a) / (2 |^ ($1 + 2))) ) & ( ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st
( G c= F & [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G & G is finite ) implies $3 = $2 + ((b - a) / (2 |^ ($1 + 2))) ) );
A7: for n being Element of NAT
for p being Real ex w being Real st S1[n,p,w]
proof
let n be Element of NAT ; ::_thesis: for p being Real ex w being Real st S1[n,p,w]
let p be Real; ::_thesis: ex w being Real st S1[n,p,w]
now__::_thesis:_ex_y_being_Element_of_REAL_st_S1[n,p,y]
percases ( for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds
( not G c= F or not [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G or not G is finite ) or ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st
( G c= F & [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G & G is finite ) ) ;
supposeA8: for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds
( not G c= F or not [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G or not G is finite ) ; ::_thesis: ex y being Element of REAL st S1[n,p,y]
take y = p - ((b - a) / (2 |^ (n + 2))); ::_thesis: S1[n,p,y]
thus S1[n,p,y] by A8; ::_thesis: verum
end;
supposeA9: ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st
( G c= F & [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G & G is finite ) ; ::_thesis: ex y being Element of REAL st S1[n,p,y]
take y = p + ((b - a) / (2 |^ (n + 2))); ::_thesis: S1[n,p,y]
thus S1[n,p,y] by A9; ::_thesis: verum
end;
end;
end;
hence ex w being Real st S1[n,p,w] ; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A10: f . 0 = (a + b) / 2 and
A11: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A7);
defpred S2[ Element of NAT ] means for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds
( not G c= F or not [.((f . $1) - ((b - a) / (2 |^ ($1 + 1)))),((f . $1) + ((b - a) / (2 |^ ($1 + 1)))).] c= union G or not G is finite );
A12: (f . 0) + ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) + ((b - a) / 2) by A10, NEWTON:5
.= b ;
defpred S3[ Element of NAT ] means ( a <= (f . $1) - ((b - a) / (2 |^ ($1 + 1))) & (f . $1) + ((b - a) / (2 |^ ($1 + 1))) <= b );
A13: for n being Element of NAT holds
( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) )
proof
let n be Element of NAT ; ::_thesis: ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) )
S1[n,f . n,f . (n + 1)] by A11;
hence ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) ) ; ::_thesis: verum
end;
A14: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
A15: ((b - a) / (2 * (2 |^ (k + 1)))) + ((b - a) / (2 * (2 |^ (k + 1)))) = (b - a) / (2 |^ (k + 1)) by XCMPLX_1:118;
A16: ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ (k + (1 + 1)))) = ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ ((k + 1) + 1)))
.= ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 * (2 |^ (k + 1)))) by NEWTON:6
.= (b - a) / (2 |^ ((k + 1) + 1)) by A15, NEWTON:6
.= (b - a) / (2 |^ (k + (1 + 1))) ;
assume A17: S3[k] ; ::_thesis: S3[k + 1]
then A18: b - (f . k) >= (b - a) / (2 |^ (k + 1)) by XREAL_1:19;
A19: (f . k) - a >= (b - a) / (2 |^ (k + 1)) by A17, XREAL_1:11;
now__::_thesis:_(_a_<=_(f_._(k_+_1))_-_((b_-_a)_/_(2_|^_((k_+_1)_+_1)))_&_(f_._(k_+_1))_+_((b_-_a)_/_(2_|^_((k_+_1)_+_1)))_<=_b_)
percases ( f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) or f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ) by A13;
supposeA20: f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) ; ::_thesis: ( a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) & (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b )
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then A21: (b - a) / (2 |^ (k + 1)) >= 0 ;
(f . (k + 1)) - a = ((f . k) - a) + ((b - a) / (2 |^ (k + 2))) by A20;
then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A19, A21, XREAL_1:31;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:11; ::_thesis: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b
b - (f . (k + 1)) = (b - (f . k)) - ((b - a) / (2 |^ (k + 2))) by A20;
then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A18, A16, XREAL_1:9;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:19; ::_thesis: verum
end;
supposeA22: f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ; ::_thesis: ( a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) & (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b )
then (f . (k + 1)) - a = ((f . k) - a) - ((b - a) / (2 |^ (k + 2))) ;
then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A19, A16, XREAL_1:9;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:11; ::_thesis: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then A23: (b - a) / (2 |^ (k + 1)) >= 0 ;
b - (f . (k + 1)) = (b - (f . k)) + ((b - a) / (2 |^ (k + 2))) by A22;
then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A18, A23, XREAL_1:31;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:19; ::_thesis: verum
end;
end;
end;
hence S3[k + 1] ; ::_thesis: verum
end;
A24: (f . 0) - ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) - ((b - a) / 2) by A10, NEWTON:5
.= a ;
then A25: S3[ 0 ] by A12;
A26: for k being Element of NAT holds S3[k] from NAT_1:sch_1(A25, A14);
A27: rng f c= [.a,b.]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [.a,b.] )
assume y in rng f ; ::_thesis: y in [.a,b.]
then consider x being set such that
A28: x in dom f and
A29: y = f . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A28, FUNCT_2:def_1;
A30: ( 2 |^ (n + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
(f . n) + ((b - a) / (2 |^ (n + 1))) <= b by A26;
then A31: f . n <= b by A30, XREAL_1:40;
a <= (f . n) - ((b - a) / (2 |^ (n + 1))) by A26;
then a <= f . n by A30, XREAL_1:51;
then y in { y1 where y1 is Real : ( a <= y1 & y1 <= b ) } by A29, A31;
hence y in [.a,b.] by RCOMP_1:def_1; ::_thesis: verum
end;
A32: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A33: S2[k] ; ::_thesis: S2[k + 1]
given G being Subset-Family of (Closed-Interval-MSpace (a,b)) such that A34: G c= F and
A35: [.((f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1)))),((f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1)))).] c= union G and
A36: G is finite ; ::_thesis: contradiction
A37: (b - a) / (2 |^ (k + (1 + 1))) = (b - a) / (2 |^ ((k + 1) + 1))
.= (b - a) / ((2 |^ (k + 1)) * 2) by NEWTON:6
.= ((b - a) / (2 |^ (k + 1))) / 2 by XCMPLX_1:78 ;
now__::_thesis:_contradiction
percases ( ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st
( G c= F & [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G & G is finite ) or for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds
( not G c= F or not [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G or not G is finite ) ) ;
supposeA38: ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st
( G c= F & [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G & G is finite ) ; ::_thesis: contradiction
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then ( (f . k) - ((b - a) / (2 |^ (k + 1))) <= f . k & f . k <= (f . k) + ((b - a) / (2 |^ (k + 1))) ) by XREAL_1:31, XREAL_1:43;
then A39: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] = [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] \/ [.(f . k),((f . k) + ((b - a) / (2 |^ (k + 1)))).] by XXREAL_1:165;
A40: (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38
.= f . k ;
consider G1 being Subset-Family of (Closed-Interval-MSpace (a,b)) such that
A41: G1 c= F and
A42: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G1 and
A43: G1 is finite by A38;
reconsider G3 = G1 \/ G as Subset-Family of (Closed-Interval-MSpace (a,b)) ;
(f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38
.= ((f . k) + (((b - a) / (2 |^ (k + 1))) / 2)) + (((b - a) / (2 |^ (k + 1))) / 2) by A37
.= (f . k) + ((b - a) / (2 |^ (k + 1))) ;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= (union G1) \/ (union G) by A35, A42, A40, A39, XBOOLE_1:13;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= union G3 by ZFMISC_1:78;
hence contradiction by A33, A34, A36, A41, A43, XBOOLE_1:8; ::_thesis: verum
end;
supposeA44: for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds
( not G c= F or not [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G or not G is finite ) ; ::_thesis: contradiction
then A45: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11
.= f . k ;
(f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A44
.= ((f . k) - (((b - a) / (2 |^ (k + 1))) / 2)) - (((b - a) / (2 |^ (k + 1))) / 2) by A37
.= (f . k) - ((b - a) / (2 |^ (k + 1))) ;
hence contradiction by A34, A35, A36, A44, A45; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
A46: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10;
A47: S2[ 0 ]
proof
given G being Subset-Family of (Closed-Interval-MSpace (a,b)) such that A48: G c= F and
A49: [.((f . 0) - ((b - a) / (2 |^ (0 + 1)))),((f . 0) + ((b - a) / (2 |^ (0 + 1)))).] c= union G and
A50: G is finite ; ::_thesis: contradiction
the carrier of (Closed-Interval-MSpace (a,b)) c= union G by A1, A24, A12, A49, TOPMETR:10;
then G is Cover of (Closed-Interval-MSpace (a,b)) by SETFAM_1:def_11;
hence contradiction by A6, A48, A50; ::_thesis: verum
end;
reconsider f = f as Real_Sequence ;
[.a,b.] is compact by RCOMP_1:6;
then consider s being Real_Sequence such that
A51: s is subsequence of f and
A52: s is convergent and
A53: lim s in [.a,b.] by A27, RCOMP_1:def_3;
reconsider ls = lim s as Point of (Closed-Interval-MSpace (a,b)) by A1, A53, TOPMETR:10;
consider Nseq being V40() sequence of NAT such that
A54: s = f * Nseq by A51, VALUED_0:def_17;
the carrier of (Closed-Interval-MSpace (a,b)) c= union F by A5, SETFAM_1:def_11;
then consider Z being set such that
A55: lim s in Z and
A56: Z in F by A53, A46, TARSKI:def_4;
consider p being Point of (Closed-Interval-MSpace (a,b)), r0 being Real such that
A57: Z = Ball (p,r0) by A4, A56, TOPMETR:def_4;
set G = {(Ball (p,r0))};
{(Ball (p,r0))} c= bool the carrier of (Closed-Interval-MSpace (a,b))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(Ball (p,r0))} or a in bool the carrier of (Closed-Interval-MSpace (a,b)) )
assume a in {(Ball (p,r0))} ; ::_thesis: a in bool the carrier of (Closed-Interval-MSpace (a,b))
then a = Ball (p,r0) by TARSKI:def_1;
hence a in bool the carrier of (Closed-Interval-MSpace (a,b)) ; ::_thesis: verum
end;
then reconsider G = {(Ball (p,r0))} as Subset-Family of (Closed-Interval-MSpace (a,b)) ;
A58: G c= F by A56, A57, ZFMISC_1:31;
reconsider Ns = Nseq as Real_Sequence by RELSET_1:7;
not Ns is bounded_above
proof
let r be real number ; :: according to SEQ_2:def_3 ::_thesis: ex b1 being Element of NAT st r <= Ns . b1
consider n being Element of NAT such that
A59: n > r by SEQ_4:3;
rng Nseq c= NAT by VALUED_0:def_6;
then n <= Ns . n by Th2;
hence ex b1 being Element of NAT st r <= Ns . b1 by A59, XXREAL_0:2; ::_thesis: verum
end;
then A60: 2 to_power Ns is divergent_to+infty by Th3, LIMFUNC1:31;
then A61: (2 to_power Ns) " is convergent by LIMFUNC1:34;
consider r1 being Real such that
A62: r1 > 0 and
A63: Ball (ls,r1) c= Ball (p,r0) by A55, A57, PCOMPS_1:27;
A64: r1 / 2 > 0 by A62, XREAL_1:139;
then consider n being Element of NAT such that
A65: for m being Element of NAT st m >= n holds
abs ((s . m) - (lim s)) < r1 / 2 by A52, SEQ_2:def_7;
A66: for m being Element of NAT
for q being Point of (Closed-Interval-MSpace (a,b)) st s . m = q & m >= n holds
dist (ls,q) < r1 / 2
proof
let m be Element of NAT ; ::_thesis: for q being Point of (Closed-Interval-MSpace (a,b)) st s . m = q & m >= n holds
dist (ls,q) < r1 / 2
let q be Point of (Closed-Interval-MSpace (a,b)); ::_thesis: ( s . m = q & m >= n implies dist (ls,q) < r1 / 2 )
assume that
A67: s . m = q and
A68: m >= n ; ::_thesis: dist (ls,q) < r1 / 2
abs ((s . m) - (lim s)) < r1 / 2 by A65, A68;
then A69: abs (- ((s . m) - (lim s))) < r1 / 2 by COMPLEX1:52;
dist (ls,q) = the distance of (Closed-Interval-MSpace (a,b)) . ((lim s),(s . m)) by A67, METRIC_1:def_1
.= the distance of RealSpace . (ls,q) by A67, TOPMETR:def_1
.= abs ((lim s) - (s . m)) by A67, METRIC_1:def_12, METRIC_1:def_13 ;
hence dist (ls,q) < r1 / 2 by A69; ::_thesis: verum
end;
A70: for m being Element of NAT st m >= n holds
(f * Nseq) . m in Ball (ls,(r1 / 2))
proof
let m be Element of NAT ; ::_thesis: ( m >= n implies (f * Nseq) . m in Ball (ls,(r1 / 2)) )
assume A71: m >= n ; ::_thesis: (f * Nseq) . m in Ball (ls,(r1 / 2))
( dom f = NAT & s . m = f . (Nseq . m) ) by A54, FUNCT_2:15, FUNCT_2:def_1;
then s . m in rng f by FUNCT_1:def_3;
then reconsider q = s . m as Point of (Closed-Interval-MSpace (a,b)) by A1, A27, TOPMETR:10;
dist (ls,q) < r1 / 2 by A66, A71;
hence (f * Nseq) . m in Ball (ls,(r1 / 2)) by A54, METRIC_1:11; ::_thesis: verum
end;
lim ((2 to_power Ns) ") = 0 by A60, LIMFUNC1:34;
then A72: lim ((b - a) (#) ((2 to_power Ns) ")) = (b - a) * 0 by A61, SEQ_2:8
.= 0 ;
(b - a) (#) ((2 to_power Ns) ") is convergent by A61, SEQ_2:7;
then consider i being Element of NAT such that
A73: for m being Element of NAT st i <= m holds
abs ((((b - a) (#) ((2 to_power Ns) ")) . m) - 0) < r1 / 2 by A64, A72, SEQ_2:def_7;
set l = (i + 1) + n;
A74: (i + 1) + n = (n + 1) + i ;
[.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] c= Ball (ls,r1)
proof
abs ((((b - a) (#) ((2 to_power Ns) ")) . ((i + 1) + n)) - 0) < r1 / 2 by A73, A74, NAT_1:11;
then abs ((b - a) * (((2 to_power Ns) ") . ((i + 1) + n))) < r1 / 2 by SEQ_1:9;
then abs ((b - a) * (((2 to_power Ns) . ((i + 1) + n)) ")) < r1 / 2 by VALUED_1:10;
then abs ((b - a) * ((2 to_power (Ns . ((i + 1) + n))) ")) < r1 / 2 by Def1;
then A75: abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ")) < r1 / 2 by POWER:41;
( 2 |^ ((Nseq . ((i + 1) + n)) + 1) = 2 * (2 |^ (Nseq . ((i + 1) + n))) & 2 |^ (Nseq . ((i + 1) + n)) > 0 ) by NEWTON:6, NEWTON:83;
then 1 / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) < (2 |^ (Nseq . ((i + 1) + n))) " by XREAL_1:88, XREAL_1:155;
then A76: (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") < (b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ") by A2, XREAL_1:68;
( 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) = (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by ABSVALUE:def_1;
then abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) < abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ")) by A76, ABSVALUE:5;
then A77: abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) < r1 / 2 by A75, XXREAL_0:2;
( 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48;
then A78: (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") < r1 / 2 by A77, ABSVALUE:def_1;
A79: s . ((i + 1) + n) in Ball (ls,(r1 / 2)) by A54, A70, NAT_1:11;
then reconsider sl = s . ((i + 1) + n) as Point of (Closed-Interval-MSpace (a,b)) ;
dist (ls,sl) < r1 / 2 by A79, METRIC_1:11;
then A80: abs ((lim s) - (s . ((i + 1) + n))) < r1 / 2 by Th1;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] or z in Ball (ls,r1) )
A81: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10;
assume z in [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] ; ::_thesis: z in Ball (ls,r1)
then z in { m where m is Real : ( (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) <= m & m <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) ) } by RCOMP_1:def_1;
then consider x being Real such that
A82: x = z and
A83: (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) <= x and
A84: x <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) ;
(f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) >= a by A26;
then (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) >= a by A54, FUNCT_2:15;
then A85: x >= a by A83, XXREAL_0:2;
(f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) <= b by A26;
then (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) <= b by A54, FUNCT_2:15;
then x <= b by A84, XXREAL_0:2;
then x in { m where m is Real : ( a <= m & m <= b ) } by A85;
then reconsider x9 = x as Point of (Closed-Interval-MSpace (a,b)) by A81, RCOMP_1:def_1;
abs ((lim s) - x) = abs (((lim s) - (s . ((i + 1) + n))) + ((s . ((i + 1) + n)) - x)) ;
then A86: abs ((lim s) - x) <= (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) by COMPLEX1:56;
x - (s . ((i + 1) + n)) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by A84, XREAL_1:20;
then A87: - (x - (s . ((i + 1) + n))) >= - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) by XREAL_1:24;
s . ((i + 1) + n) <= ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) + x by A83, XREAL_1:20;
then (s . ((i + 1) + n)) - x <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by XREAL_1:20;
then abs ((s . ((i + 1) + n)) - x) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by A87, ABSVALUE:5;
then abs ((s . ((i + 1) + n)) - x) < r1 / 2 by A78, XXREAL_0:2;
then (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) < (r1 / 2) + (r1 / 2) by A80, XREAL_1:8;
then abs ((lim s) - x) < (r1 / 2) + (r1 / 2) by A86, XXREAL_0:2;
then dist (ls,x9) < r1 by Th1;
hence z in Ball (ls,r1) by A82, METRIC_1:11; ::_thesis: verum
end;
then [.((s . ((i + 1) + n)) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] c= Ball (p,r0) by A63, XBOOLE_1:1;
then [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball (p,r0) by A54, FUNCT_2:15;
then [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball (p,r0) by A54, FUNCT_2:15;
then A88: [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= union G by ZFMISC_1:25;
for k being Element of NAT holds S2[k] from NAT_1:sch_1(A47, A32);
hence contradiction by A58, A88; ::_thesis: verum
end;
end;
end;
hence Closed-Interval-TSpace (a,b) is compact ; ::_thesis: verum
end;