:: JCT_MISC semantic presentation
begin
scheme :: JCT_MISC:sch 1
NonEmpty{ F1() -> non empty set , F2( set ) -> set } :
not { F2(a) where a is Element of F1() : verum } is empty
proof
consider a0 being set such that
A1: a0 in F1() by XBOOLE_0:def_1;
F2(a0) in { F2(a) where a is Element of F1() : verum } by A1;
hence not { F2(a) where a is Element of F1() : verum } is empty ; ::_thesis: verum
end;
theorem Th1: :: JCT_MISC:1
for r, s, a, b being real number st r in [.a,b.] & s in [.a,b.] holds
(r + s) / 2 in [.a,b.]
proof
let r, s be real number ; ::_thesis: for a, b being real number st r in [.a,b.] & s in [.a,b.] holds
(r + s) / 2 in [.a,b.]
let a, b be real number ; ::_thesis: ( r in [.a,b.] & s in [.a,b.] implies (r + s) / 2 in [.a,b.] )
assume that
A1: r in [.a,b.] and
A2: s in [.a,b.] ; ::_thesis: (r + s) / 2 in [.a,b.]
reconsider a = a, b = b, r = r, s = s as Real by XREAL_0:def_1;
A3: s <= b by A2, XXREAL_1:1;
r <= b by A1, XXREAL_1:1;
then r + s <= b + b by A3, XREAL_1:7;
then A4: (r + s) / 2 <= (b + b) / 2 by XREAL_1:72;
A5: a <= s by A2, XXREAL_1:1;
a <= r by A1, XXREAL_1:1;
then a + a <= r + s by A5, XREAL_1:7;
then (a + a) / 2 <= (r + s) / 2 by XREAL_1:72;
hence (r + s) / 2 in [.a,b.] by A4; ::_thesis: verum
end;
theorem Th2: :: JCT_MISC:2
for r0, s0, r, s being real number holds abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s))
proof
let r0, s0, r, s be real number ; ::_thesis: abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s))
(r0 - s0) - (r - s) = (r0 - r) - (s0 - s) ;
then A1: abs ((r0 - s0) - (r - s)) <= (abs (r0 - r)) + (abs (s0 - s)) by COMPLEX1:57;
abs ((abs (r0 - s0)) - (abs (r - s))) <= abs ((r0 - s0) - (r - s)) by COMPLEX1:64;
hence abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s)) by A1, XXREAL_0:2; ::_thesis: verum
end;
theorem Th3: :: JCT_MISC:3
for t, r, s being real number st t in ].r,s.[ holds
abs t < max ((abs r),(abs s))
proof
let t, r, s be real number ; ::_thesis: ( t in ].r,s.[ implies abs t < max ((abs r),(abs s)) )
assume A1: t in ].r,s.[ ; ::_thesis: abs t < max ((abs r),(abs s))
reconsider r = r, t = t, s = s as Real by XREAL_0:def_1;
A2: r < t by A1, XXREAL_1:4;
A3: t < s by A1, XXREAL_1:4;
percases ( t >= 0 or t < 0 ) ;
supposeA4: t >= 0 ; ::_thesis: abs t < max ((abs r),(abs s))
then t = abs t by ABSVALUE:def_1;
then abs t < abs s by A3, A4, ABSVALUE:def_1;
hence abs t < max ((abs r),(abs s)) by XXREAL_0:30; ::_thesis: verum
end;
supposeA5: t < 0 ; ::_thesis: abs t < max ((abs r),(abs s))
then A6: - t = abs t by ABSVALUE:def_1;
- r = abs r by A2, A5, ABSVALUE:def_1;
then abs t < abs r by A2, A6, XREAL_1:24;
hence abs t < max ((abs r),(abs s)) by XXREAL_0:30; ::_thesis: verum
end;
end;
end;
scheme :: JCT_MISC:sch 2
DoubleChoice{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set , set ] } :
ex a being Function of F1(),F2() ex b being Function of F1(),F3() st
for i being Element of F1() holds P1[i,a . i,b . i]
provided
A1: for i being Element of F1() ex ai being Element of F2() ex bi being Element of F3() st P1[i,ai,bi]
proof
defpred S1[ set , set ] means P1[$1,$2 `1 ,$2 `2 ];
A2: for e being Element of F1() ex u being Element of [:F2(),F3():] st S1[e,u]
proof
let e be Element of F1(); ::_thesis: ex u being Element of [:F2(),F3():] st S1[e,u]
consider ai being Element of F2(), bi being Element of F3() such that
A3: P1[e,ai,bi] by A1;
take [ai,bi] ; ::_thesis: ( [ai,bi] is Element of [:F2(),F3():] & S1[e,[ai,bi]] )
thus [ai,bi] is Element of [:F2(),F3():] by ZFMISC_1:87; ::_thesis: S1[e,[ai,bi]]
thus S1[e,[ai,bi]] by A3; ::_thesis: verum
end;
consider f being Function of F1(),[:F2(),F3():] such that
A4: for e being Element of F1() holds S1[e,f . e] from FUNCT_2:sch_3(A2);
take pr1 f ; ::_thesis: ex b being Function of F1(),F3() st
for i being Element of F1() holds P1[i,(pr1 f) . i,b . i]
take pr2 f ; ::_thesis: for i being Element of F1() holds P1[i,(pr1 f) . i,(pr2 f) . i]
let i be Element of F1(); ::_thesis: P1[i,(pr1 f) . i,(pr2 f) . i]
A5: (f . i) `2 = (pr2 f) . i by FUNCT_2:def_6;
(f . i) `1 = (pr1 f) . i by FUNCT_2:def_5;
hence P1[i,(pr1 f) . i,(pr2 f) . i] by A4, A5; ::_thesis: verum
end;
theorem Th4: :: JCT_MISC:4
for S, T being non empty TopSpace
for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds
G is open
proof
let S, T be non empty TopSpace; ::_thesis: for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds
G is open
let G be Subset of [:S,T:]; ::_thesis: ( ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) implies G is open )
assume A1: for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ; ::_thesis: G is open
set A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } ;
{ [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } c= bool the carrier of [:S,T:]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } or e in bool the carrier of [:S,T:] )
assume e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } ; ::_thesis: e in bool the carrier of [:S,T:]
then ex GS being Subset of S ex GT being Subset of T st
( e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) ;
hence e in bool the carrier of [:S,T:] ; ::_thesis: verum
end;
then reconsider A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } as Subset-Family of [:S,T:] ;
reconsider A = A as Subset-Family of [:S,T:] ;
for x being set holds
( x in G iff ex Y being set st
( x in Y & Y in A ) )
proof
let x be set ; ::_thesis: ( x in G iff ex Y being set st
( x in Y & Y in A ) )
thus ( x in G implies ex Y being set st
( x in Y & Y in A ) ) ::_thesis: ( ex Y being set st
( x in Y & Y in A ) implies x in G )
proof
assume x in G ; ::_thesis: ex Y being set st
( x in Y & Y in A )
then consider GS being Subset of S, GT being Subset of T such that
A2: GS is open and
A3: GT is open and
A4: x in [:GS,GT:] and
A5: [:GS,GT:] c= G by A1;
take [:GS,GT:] ; ::_thesis: ( x in [:GS,GT:] & [:GS,GT:] in A )
thus ( x in [:GS,GT:] & [:GS,GT:] in A ) by A2, A3, A4, A5; ::_thesis: verum
end;
given Y being set such that A6: x in Y and
A7: Y in A ; ::_thesis: x in G
ex GS being Subset of S ex GT being Subset of T st
( Y = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) by A7;
hence x in G by A6; ::_thesis: verum
end;
then A8: G = union A by TARSKI:def_4;
for e being set st e in A holds
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
proof
let e be set ; ::_thesis: ( e in A implies ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume e in A ; ::_thesis: ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then ex GS being Subset of S ex GT being Subset of T st
( e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) ;
hence ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; ::_thesis: verum
end;
hence G is open by A8, BORSUK_1:5; ::_thesis: verum
end;
begin
theorem Th5: :: JCT_MISC:5
for A, B being compact Subset of REAL holds A /\ B is compact
proof
let A, B be compact Subset of REAL; ::_thesis: A /\ B is compact
let s1 be Real_Sequence; :: according to RCOMP_1:def_3 ::_thesis: ( not proj2 s1 c= A /\ B or ex b1 being Element of bool [:NAT,REAL:] st
( b1 is subsequence of s1 & b1 is convergent & lim b1 in A /\ B ) )
assume A1: rng s1 c= A /\ B ; ::_thesis: ex b1 being Element of bool [:NAT,REAL:] st
( b1 is subsequence of s1 & b1 is convergent & lim b1 in A /\ B )
A2: A /\ B c= B by XBOOLE_1:17;
A /\ B c= A by XBOOLE_1:17;
then rng s1 c= A by A1, XBOOLE_1:1;
then consider s2 being Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent and
A5: lim s2 in A by RCOMP_1:def_3;
rng s2 c= rng s1 by A3, VALUED_0:21;
then rng s2 c= A /\ B by A1, XBOOLE_1:1;
then rng s2 c= B by A2, XBOOLE_1:1;
then consider s3 being Real_Sequence such that
A6: s3 is subsequence of s2 and
A7: s3 is convergent and
A8: lim s3 in B by RCOMP_1:def_3;
take s3 ; ::_thesis: ( s3 is subsequence of s1 & s3 is convergent & lim s3 in A /\ B )
thus s3 is subsequence of s1 by A3, A6, VALUED_0:20; ::_thesis: ( s3 is convergent & lim s3 in A /\ B )
thus s3 is convergent by A7; ::_thesis: lim s3 in A /\ B
lim s3 = lim s2 by A4, A6, SEQ_4:17;
hence lim s3 in A /\ B by A5, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: JCT_MISC:6
for T being non empty TopSpace
for f being continuous RealMap of T
for A being Subset of T st A is connected holds
f .: A is interval
proof
let T be non empty TopSpace; ::_thesis: for f being continuous RealMap of T
for A being Subset of T st A is connected holds
f .: A is interval
let f be continuous RealMap of T; ::_thesis: for A being Subset of T st A is connected holds
f .: A is interval
let A be Subset of T; ::_thesis: ( A is connected implies f .: A is interval )
assume A1: A is connected ; ::_thesis: f .: A is interval
let r, s be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: ( not r in f .: A or not s in f .: A or [.r,s.] c= f .: A )
A2: A c= f " (f .: A) by FUNCT_2:42;
assume A3: r in f .: A ; ::_thesis: ( not s in f .: A or [.r,s.] c= f .: A )
then consider p being Point of T such that
A4: p in A and
A5: r = f . p by FUNCT_2:65;
assume A6: s in f .: A ; ::_thesis: [.r,s.] c= f .: A
then consider q being Point of T such that
A7: q in A and
A8: s = f . q by FUNCT_2:65;
assume A9: not [.r,s.] c= f .: A ; ::_thesis: contradiction
reconsider r = r, s = s as Real by A3, A6;
consider t being Real such that
A10: t in [.r,s.] and
A11: not t in f .: A by A9, SUBSET_1:2;
reconsider r = r, s = s, t = t as Real ;
set P1 = f " (left_open_halfline t);
set Q1 = f " (right_open_halfline t);
set P = (f " (left_open_halfline t)) /\ A;
set Q = (f " (right_open_halfline t)) /\ A;
set X = (left_open_halfline t) \/ (right_open_halfline t);
A12: f " (right_open_halfline t) is open by PSCOMP_1:8;
t <= s by A10, XXREAL_1:1;
then A13: t < s by A6, A11, XXREAL_0:1;
right_open_halfline t = { r1 where r1 is Real : t < r1 } by XXREAL_1:230;
then s in right_open_halfline t by A13;
then q in f " (right_open_halfline t) by A8, FUNCT_2:38;
then A14: (f " (right_open_halfline t)) /\ A <> {} T by A7, XBOOLE_0:def_4;
(left_open_halfline t) /\ (right_open_halfline t) = ].t,t.[ by XXREAL_1:269
.= {} by XXREAL_1:28 ;
then left_open_halfline t misses right_open_halfline t by XBOOLE_0:def_7;
then f " (left_open_halfline t) misses f " (right_open_halfline t) by FUNCT_1:71;
then (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) = {} by XBOOLE_0:def_7;
then A15: (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) misses ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) by XBOOLE_1:65;
reconsider Y = {t} as Subset of REAL ;
Y ` = REAL \ [.t,t.] by XXREAL_1:17
.= (left_open_halfline t) \/ (right_open_halfline t) by XXREAL_1:385 ;
then A16: (f " Y) ` = f " ((left_open_halfline t) \/ (right_open_halfline t)) by FUNCT_2:100
.= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by RELAT_1:140 ;
f " {t} misses f " (f .: A) by A11, FUNCT_1:71, ZFMISC_1:50;
then f " {t} misses A by A2, XBOOLE_1:63;
then A c= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by A16, SUBSET_1:23;
then A17: A = A /\ ((f " (left_open_halfline t)) \/ (f " (right_open_halfline t))) by XBOOLE_1:28
.= ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) by XBOOLE_1:23 ;
A18: (f " (left_open_halfline t)) /\ A c= f " (left_open_halfline t) by XBOOLE_1:17;
r <= t by A10, XXREAL_1:1;
then A19: r < t by A3, A11, XXREAL_0:1;
left_open_halfline t = { r1 where r1 is Real : r1 < t } by XXREAL_1:229;
then r in left_open_halfline t by A19;
then p in f " (left_open_halfline t) by A5, FUNCT_2:38;
then A20: (f " (left_open_halfline t)) /\ A <> {} T by A4, XBOOLE_0:def_4;
A21: (f " (right_open_halfline t)) /\ A c= f " (right_open_halfline t) by XBOOLE_1:17;
f " (left_open_halfline t) is open by PSCOMP_1:8;
then (f " (left_open_halfline t)) /\ A,(f " (right_open_halfline t)) /\ A are_separated by A12, A18, A21, A15, TSEP_1:45;
hence contradiction by A1, A17, A20, A14, CONNSP_1:15; ::_thesis: verum
end;
definition
let A, B be Subset of REAL;
func dist (A,B) -> real number means :Def1: :: JCT_MISC:def 1
ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & it = lower_bound X );
existence
ex b1 being real number ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X )
proof
set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ;
{ (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL
then ex r, s being Element of REAL st
( e = abs (r - s) & r in A & s in B ) ;
hence e in REAL ; ::_thesis: verum
end;
then reconsider Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ;
take lower_bound Y0 ; ::_thesis: ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & lower_bound Y0 = lower_bound X )
thus ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & lower_bound Y0 = lower_bound X ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being real number st ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) & ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b2 = lower_bound X ) holds
b1 = b2 ;
commutativity
for b1 being real number
for A, B being Subset of REAL st ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) holds
ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & b1 = lower_bound X )
proof
let IT be real number ; ::_thesis: for A, B being Subset of REAL st ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & IT = lower_bound X ) holds
ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound X )
let A, B be Subset of REAL; ::_thesis: ( ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & IT = lower_bound X ) implies ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound X ) )
given X0 being Subset of REAL such that A1: X0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } and
A2: IT = lower_bound X0 ; ::_thesis: ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound X )
set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } ;
{ (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } c= REAL
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } ; ::_thesis: e in REAL
then ex r, s being Element of REAL st
( e = abs (r - s) & r in B & s in A ) ;
hence e in REAL ; ::_thesis: verum
end;
then reconsider Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } as Subset of REAL ;
take Y0 ; ::_thesis: ( Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound Y0 )
thus Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } ; ::_thesis: IT = lower_bound Y0
X0 = Y0
proof
thus X0 c= Y0 :: according to XBOOLE_0:def_10 ::_thesis: Y0 c= X0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X0 or x in Y0 )
assume x in X0 ; ::_thesis: x in Y0
then consider r, s being Element of REAL such that
A3: x = abs (r - s) and
A4: r in A and
A5: s in B by A1;
x = abs (s - r) by A3, UNIFORM1:11;
hence x in Y0 by A4, A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y0 or x in X0 )
assume x in Y0 ; ::_thesis: x in X0
then consider r, s being Element of REAL such that
A6: x = abs (r - s) and
A7: r in B and
A8: s in A ;
x = abs (s - r) by A6, UNIFORM1:11;
hence x in X0 by A1, A7, A8; ::_thesis: verum
end;
hence IT = lower_bound Y0 by A2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines dist JCT_MISC:def_1_:_
for A, B being Subset of REAL
for b3 being real number holds
( b3 = dist (A,B) iff ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b3 = lower_bound X ) );
theorem Th7: :: JCT_MISC:7
for A, B being Subset of REAL
for r, s being real number st r in A & s in B holds
abs (r - s) >= dist (A,B)
proof
let A, B be Subset of REAL; ::_thesis: for r, s being real number st r in A & s in B holds
abs (r - s) >= dist (A,B)
set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ;
let r, s be real number ; ::_thesis: ( r in A & s in B implies abs (r - s) >= dist (A,B) )
assume that
A1: r in A and
A2: s in B ; ::_thesis: abs (r - s) >= dist (A,B)
{ (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL
then ex r, s being Real st
( e = abs (r - s) & r in A & s in B ) ;
hence e in REAL ; ::_thesis: verum
end;
then reconsider Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ;
A3: Y0 is bounded_below
proof
take 0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of Y0
let r0 be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r0 in Y0 or 0 <= r0 )
assume r0 in Y0 ; ::_thesis: 0 <= r0
then ex r, s being Real st
( r0 = abs (r - s) & r in A & s in B ) ;
hence 0 <= r0 by COMPLEX1:46; ::_thesis: verum
end;
A4: dist (A,B) = lower_bound Y0 by Def1;
abs (r - s) in Y0 by A1, A2;
hence abs (r - s) >= dist (A,B) by A4, A3, SEQ_4:def_2; ::_thesis: verum
end;
theorem Th8: :: JCT_MISC:8
for A, B being Subset of REAL
for C, D being non empty Subset of REAL st C c= A & D c= B holds
dist (A,B) <= dist (C,D)
proof
let A, B be Subset of REAL; ::_thesis: for C, D being non empty Subset of REAL st C c= A & D c= B holds
dist (A,B) <= dist (C,D)
let C, D be non empty Subset of REAL; ::_thesis: ( C c= A & D c= B implies dist (A,B) <= dist (C,D) )
assume that
A1: C c= A and
A2: D c= B ; ::_thesis: dist (A,B) <= dist (C,D)
consider s0 being set such that
A3: s0 in D by XBOOLE_0:def_1;
set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } ;
consider r0 being set such that
A4: r0 in C by XBOOLE_0:def_1;
A5: { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } c= REAL
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } ; ::_thesis: e in REAL
then ex r, s being Real st
( e = abs (r - s) & r in C & s in D ) ;
hence e in REAL ; ::_thesis: verum
end;
reconsider r0 = r0, s0 = s0 as real number by A4, A3;
abs (r0 - s0) in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } by A4, A3;
then reconsider Y = { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } as non empty Subset of REAL by A5;
set X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ;
{ (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL
then ex r, s being Real st
( e = abs (r - s) & r in A & s in B ) ;
hence e in REAL ; ::_thesis: verum
end;
then reconsider X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ;
A6: Y c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X )
assume x in Y ; ::_thesis: x in X
then ex r, s being Real st
( x = abs (r - s) & r in C & s in D ) ;
hence x in X by A1, A2; ::_thesis: verum
end;
A7: X is bounded_below
proof
take 0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X
let r0 be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r0 in X or 0 <= r0 )
assume r0 in X ; ::_thesis: 0 <= r0
then ex r, s being Real st
( r0 = abs (r - s) & r in A & s in B ) ;
hence 0 <= r0 by COMPLEX1:46; ::_thesis: verum
end;
A8: dist (C,D) = lower_bound Y by Def1;
dist (A,B) = lower_bound X by Def1;
hence dist (A,B) <= dist (C,D) by A7, A8, A6, SEQ_4:47; ::_thesis: verum
end;
theorem Th9: :: JCT_MISC:9
for A, B being non empty compact Subset of REAL ex r, s being real number st
( r in A & s in B & dist (A,B) = abs (r - s) )
proof
defpred S1[ set , set ] means ex r, s being Real st
( $1 = [r,s] & $2 = abs (r - s) );
let A, B be non empty compact Subset of REAL; ::_thesis: ex r, s being real number st
( r in A & s in B & dist (A,B) = abs (r - s) )
reconsider At = A, Bt = B as non empty compact Subset of R^1 by JORDAN5A:25, TOPMETR:17;
A1: the carrier of (R^1 | Bt) = Bt by PRE_TOPC:8;
reconsider AB = [:(R^1 | At),(R^1 | Bt):] as non empty compact TopSpace ;
A2: the carrier of (R^1 | At) = At by PRE_TOPC:8;
A3: now__::_thesis:_for_x_being_Element_of_AB_ex_t_being_Element_of_REAL_st_S1[x,t]
let x be Element of AB; ::_thesis: ex t being Element of REAL st S1[x,t]
x in the carrier of AB ;
then x in [:A,B:] by A2, A1, BORSUK_1:def_2;
then consider r, s being set such that
A4: r in REAL and
A5: s in REAL and
A6: x = [r,s] by ZFMISC_1:84;
reconsider r = r, s = s as Real by A4, A5;
take t = abs (r - s); ::_thesis: S1[x,t]
thus S1[x,t] by A6; ::_thesis: verum
end;
consider f being RealMap of AB such that
A7: for x being Element of AB holds S1[x,f . x] from FUNCT_2:sch_3(A3);
for Y being Subset of REAL st Y is open holds
f " Y is open
proof
let Y be Subset of REAL; ::_thesis: ( Y is open implies f " Y is open )
assume A8: Y is open ; ::_thesis: f " Y is open
for x being Point of AB st x in f " Y holds
ex YS being Subset of (R^1 | At) ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )
proof
let x be Point of AB; ::_thesis: ( x in f " Y implies ex YS being Subset of (R^1 | At) ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y ) )
consider r, s being Real such that
A9: x = [r,s] and
A10: f . x = abs (r - s) by A7;
assume x in f " Y ; ::_thesis: ex YS being Subset of (R^1 | At) ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )
then f . x in Y by FUNCT_1:def_7;
then consider N being Neighbourhood of f . x such that
A11: N c= Y by A8, RCOMP_1:18;
consider g being real number such that
A12: 0 < g and
A13: N = ].((f . x) - g),((f . x) + g).[ by RCOMP_1:def_6;
reconsider a = r - (g / 2), b = r + (g / 2), c = s - (g / 2), d = s + (g / 2) as Real ;
reconsider S = ].a,b.[, T = ].c,d.[ as Subset of R^1 by TOPMETR:17;
reconsider YT = T /\ B as Subset of (R^1 | Bt) by A1, XBOOLE_1:17;
reconsider YS = S /\ A as Subset of (R^1 | At) by A2, XBOOLE_1:17;
A14: s in T by A12, TOPREAL6:15, XREAL_1:215;
take YS ; ::_thesis: ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )
take YT ; ::_thesis: ( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )
A15: T is open by JORDAN6:35;
S is open by JORDAN6:35;
hence ( YS is open & YT is open ) by A2, A1, A15, TSP_1:def_1; ::_thesis: ( x in [:YS,YT:] & [:YS,YT:] c= f " Y )
A16: r in S by A12, TOPREAL6:15, XREAL_1:215;
x in the carrier of AB ;
then A17: x in [:A,B:] by A2, A1, BORSUK_1:def_2;
then s in B by A9, ZFMISC_1:87;
then A18: s in YT by A14, XBOOLE_0:def_4;
f .: [:YS,YT:] c= N
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in f .: [:YS,YT:] or e in N )
assume e in f .: [:YS,YT:] ; ::_thesis: e in N
then consider y being Element of AB such that
A19: y in [:YS,YT:] and
A20: e = f . y by FUNCT_2:65;
consider r1, s1 being Real such that
A21: y = [r1,s1] and
A22: f . y = abs (r1 - s1) by A7;
A23: abs ((abs (r1 - s1)) - (abs (r - s))) <= (abs (r1 - r)) + (abs (s1 - s)) by Th2;
s1 in YT by A19, A21, ZFMISC_1:87;
then s1 in ].(s - (g / 2)),(s + (g / 2)).[ by XBOOLE_0:def_4;
then A24: abs (s1 - s) < g / 2 by RCOMP_1:1;
r1 in YS by A19, A21, ZFMISC_1:87;
then r1 in ].(r - (g / 2)),(r + (g / 2)).[ by XBOOLE_0:def_4;
then A25: abs (r1 - r) < g / 2 by RCOMP_1:1;
g = (g / 2) + (g / 2) ;
then (abs (r1 - r)) + (abs (s1 - s)) < g by A25, A24, XREAL_1:8;
then abs ((abs (r1 - s1)) - (abs (r - s))) < g by A23, XXREAL_0:2;
hence e in N by A13, A10, A20, A22, RCOMP_1:1; ::_thesis: verum
end;
then A26: f .: [:YS,YT:] c= Y by A11, XBOOLE_1:1;
r in A by A9, A17, ZFMISC_1:87;
then r in YS by A16, XBOOLE_0:def_4;
hence x in [:YS,YT:] by A9, A18, ZFMISC_1:87; ::_thesis: [:YS,YT:] c= f " Y
dom f = the carrier of AB by FUNCT_2:def_1;
hence [:YS,YT:] c= f " Y by A26, FUNCT_1:93; ::_thesis: verum
end;
hence f " Y is open by Th4; ::_thesis: verum
end;
then reconsider f = f as continuous RealMap of AB by PSCOMP_1:8;
f .: the carrier of AB is with_min by MEASURE6:def_13;
then lower_bound (f .: the carrier of AB) in f .: the carrier of AB by MEASURE6:def_5;
then consider x being Element of AB such that
A27: x in the carrier of AB and
A28: lower_bound (f .: the carrier of AB) = f . x by FUNCT_2:65;
A29: x in [:A,B:] by A2, A1, A27, BORSUK_1:def_2;
then consider r1, s1 being set such that
A30: r1 in REAL and
A31: s1 in REAL and
A32: x = [r1,s1] by ZFMISC_1:84;
A33: f .: the carrier of AB = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= f .: the carrier of AB
let x be set ; ::_thesis: ( x in f .: the carrier of AB implies x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } )
assume x in f .: the carrier of AB ; ::_thesis: x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) }
then consider y being Element of AB such that
A34: y in the carrier of AB and
A35: x = f . y by FUNCT_2:65;
consider r1, s1 being Real such that
A36: y = [r1,s1] and
A37: f . y = abs (r1 - s1) by A7;
A38: [r1,s1] in [:A,B:] by A2, A1, A34, A36, BORSUK_1:def_2;
then A39: s1 in B by ZFMISC_1:87;
r1 in A by A38, ZFMISC_1:87;
hence x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } by A35, A37, A39; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or x in f .: the carrier of AB )
assume x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: x in f .: the carrier of AB
then consider r, s being Real such that
A40: x = abs (r - s) and
A41: r in A and
A42: s in B ;
[r,s] in [:A,B:] by A41, A42, ZFMISC_1:87;
then reconsider y = [r,s] as Element of AB by A2, A1, BORSUK_1:def_2;
consider r1, s1 being Real such that
A43: y = [r1,s1] and
A44: f . y = abs (r1 - s1) by A7;
A45: s1 = s by A43, XTUPLE_0:1;
r1 = r by A43, XTUPLE_0:1;
hence x in f .: the carrier of AB by A40, A44, A45, FUNCT_2:35; ::_thesis: verum
end;
reconsider r1 = r1, s1 = s1 as real number by A30, A31;
take r1 ; ::_thesis: ex s being real number st
( r1 in A & s in B & dist (A,B) = abs (r1 - s) )
take s1 ; ::_thesis: ( r1 in A & s1 in B & dist (A,B) = abs (r1 - s1) )
thus ( r1 in A & s1 in B ) by A29, A32, ZFMISC_1:87; ::_thesis: dist (A,B) = abs (r1 - s1)
consider r, s being Real such that
A46: x = [r,s] and
A47: f . x = abs (r - s) by A7;
A48: s1 = s by A32, A46, XTUPLE_0:1;
r1 = r by A32, A46, XTUPLE_0:1;
hence dist (A,B) = abs (r1 - s1) by A28, A33, A47, A48, Def1; ::_thesis: verum
end;
theorem Th10: :: JCT_MISC:10
for A, B being non empty compact Subset of REAL holds dist (A,B) >= 0
proof
let A, B be non empty compact Subset of REAL; ::_thesis: dist (A,B) >= 0
set X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ;
consider r0 being set such that
A1: r0 in A by XBOOLE_0:def_1;
A2: { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL
then ex r, s being Real st
( e = abs (r - s) & r in A & s in B ) ;
hence e in REAL ; ::_thesis: verum
end;
consider s0 being set such that
A3: s0 in B by XBOOLE_0:def_1;
reconsider r0 = r0, s0 = s0 as real number by A1, A3;
abs (r0 - s0) in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } by A1, A3;
then reconsider X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as non empty Subset of REAL by A2;
A4: for t being real number st t in X holds
t >= 0
proof
let t be real number ; ::_thesis: ( t in X implies t >= 0 )
assume t in X ; ::_thesis: t >= 0
then ex r, s being Real st
( t = abs (r - s) & r in A & s in B ) ;
hence t >= 0 by COMPLEX1:46; ::_thesis: verum
end;
dist (A,B) = lower_bound X by Def1;
hence dist (A,B) >= 0 by A4, SEQ_4:43; ::_thesis: verum
end;
theorem Th11: :: JCT_MISC:11
for A, B being non empty compact Subset of REAL st A misses B holds
dist (A,B) > 0
proof
let A, B be non empty compact Subset of REAL; ::_thesis: ( A misses B implies dist (A,B) > 0 )
assume A1: A misses B ; ::_thesis: dist (A,B) > 0
consider r0, s0 being real number such that
A2: r0 in A and
A3: s0 in B and
A4: dist (A,B) = abs (r0 - s0) by Th9;
reconsider r0 = r0, s0 = s0 as Real by XREAL_0:def_1;
assume dist (A,B) <= 0 ; ::_thesis: contradiction
then abs (r0 - s0) = 0 by A4, Th10;
then r0 = s0 by GOBOARD7:2;
hence contradiction by A1, A2, A3, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: JCT_MISC:12
for e, f being real number
for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds
for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) )
proof
let e, f be real number ; ::_thesis: for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds
for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) )
let A, B be compact Subset of REAL; ::_thesis: ( A misses B & A c= [.e,f.] & B c= [.e,f.] implies for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) ) )
assume that
A1: A misses B and
A2: A c= [.e,f.] and
A3: B c= [.e,f.] ; ::_thesis: for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) )
let S be Function of NAT,(bool REAL); ::_thesis: ( ( for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ) implies ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) ) )
assume A4: for i being Element of NAT holds
( S . i is interval & S . i meets A & S . i meets B ) ; ::_thesis: ex r being real number st
( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & r in S . k ) ) )
defpred S1[ set , Subset of REAL] means ( not $2 is empty & $2 is closed_interval & $2 meets A & $2 meets B & $2 c= S . $1 );
A5: for i being Element of NAT ex u being Subset of REAL st S1[i,u]
proof
let i be Element of NAT ; ::_thesis: ex u being Subset of REAL st S1[i,u]
A6: S . i is interval by A4;
S . i meets B by A4;
then consider y being set such that
A7: y in S . i and
A8: y in B by XBOOLE_0:3;
S . i meets A by A4;
then consider x being set such that
A9: x in S . i and
A10: x in A by XBOOLE_0:3;
reconsider y = y as Real by A8;
reconsider x = x as Real by A10;
percases ( x <= y or y <= x ) ;
supposeA11: x <= y ; ::_thesis: ex u being Subset of REAL st S1[i,u]
take [.x,y.] ; ::_thesis: S1[i,[.x,y.]]
thus ( not [.x,y.] is empty & [.x,y.] is closed_interval ) by A11, MEASURE5:14; ::_thesis: ( [.x,y.] meets A & [.x,y.] meets B & [.x,y.] c= S . i )
x in [.x,y.] by A11;
hence [.x,y.] meets A by A10, XBOOLE_0:3; ::_thesis: ( [.x,y.] meets B & [.x,y.] c= S . i )
y in [.x,y.] by A11;
hence [.x,y.] meets B by A8, XBOOLE_0:3; ::_thesis: [.x,y.] c= S . i
thus [.x,y.] c= S . i by A9, A7, A6, XXREAL_2:def_12; ::_thesis: verum
end;
supposeA12: y <= x ; ::_thesis: ex u being Subset of REAL st S1[i,u]
take [.y,x.] ; ::_thesis: S1[i,[.y,x.]]
thus ( not [.y,x.] is empty & [.y,x.] is closed_interval ) by A12, MEASURE5:14; ::_thesis: ( [.y,x.] meets A & [.y,x.] meets B & [.y,x.] c= S . i )
x in [.y,x.] by A12;
hence [.y,x.] meets A by A10, XBOOLE_0:3; ::_thesis: ( [.y,x.] meets B & [.y,x.] c= S . i )
y in [.y,x.] by A12;
hence [.y,x.] meets B by A8, XBOOLE_0:3; ::_thesis: [.y,x.] c= S . i
thus [.y,x.] c= S . i by A9, A7, A6, XXREAL_2:def_12; ::_thesis: verum
end;
end;
end;
consider T being Function of NAT,(bool REAL) such that
A13: for i being Element of NAT holds S1[i,T . i] from FUNCT_2:sch_3(A5);
T . 0 meets B by A13;
then A14: not B is empty by XBOOLE_1:65;
deffunc H1( Element of NAT ) -> Element of bool REAL = (T . $1) /\ B;
deffunc H2( Element of NAT ) -> Element of bool REAL = (T . $1) /\ A;
consider SA being Function of NAT,(bool REAL) such that
A15: for i being Element of NAT holds SA . i = H2(i) from FUNCT_2:sch_4();
consider SB being Function of NAT,(bool REAL) such that
A16: for i being Element of NAT holds SB . i = H1(i) from FUNCT_2:sch_4();
defpred S2[ Element of NAT , Real, Real] means ( $2 in SA . $1 & $3 in SB . $1 & dist ((SA . $1),(SB . $1)) = abs ($2 - $3) );
A17: for i being Element of NAT ex ai, bi being Real st S2[i,ai,bi]
proof
let i be Element of NAT ; ::_thesis: ex ai, bi being Real st S2[i,ai,bi]
reconsider Si = T . i as non empty closed_interval Subset of REAL by A13;
A18: T . i meets B by A13;
A19: SA . i = Si /\ A by A15;
A20: SB . i = Si /\ B by A16;
T . i meets A by A13;
then reconsider SAi = SA . i, SBi = SB . i as non empty compact Subset of REAL by A18, A19, A20, Th5, XBOOLE_0:def_7;
consider ai, bi being real number such that
A21: ai in SAi and
A22: bi in SBi and
A23: dist (SAi,SBi) = abs (ai - bi) by Th9;
reconsider ai = ai, bi = bi as Real by XREAL_0:def_1;
take ai ; ::_thesis: ex bi being Real st S2[i,ai,bi]
take bi ; ::_thesis: S2[i,ai,bi]
thus S2[i,ai,bi] by A21, A22, A23; ::_thesis: verum
end;
consider sa, sb being Real_Sequence such that
A24: for i being Element of NAT holds S2[i,sa . i,sb . i] from JCT_MISC:sch_2(A17);
rng sa c= [.e,f.]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng sa or u in [.e,f.] )
assume u in rng sa ; ::_thesis: u in [.e,f.]
then consider x being set such that
A25: x in dom sa and
A26: u = sa . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A25;
sa . n in SA . n by A24;
then u in (T . n) /\ A by A15, A26;
then u in A by XBOOLE_0:def_4;
hence u in [.e,f.] by A2; ::_thesis: verum
end;
then consider ga being Real_Sequence such that
A27: ga is subsequence of sa and
A28: ga is convergent and
A29: lim ga in [.e,f.] by RCOMP_1:def_3;
consider Nseq being increasing sequence of NAT such that
A30: ga = sa * Nseq by A27, VALUED_0:def_17;
set gb = sb * Nseq;
rng (sb * Nseq) c= [.e,f.]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng (sb * Nseq) or u in [.e,f.] )
assume u in rng (sb * Nseq) ; ::_thesis: u in [.e,f.]
then consider x being set such that
A31: x in dom (sb * Nseq) and
A32: u = (sb * Nseq) . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A31;
(sb * Nseq) . n = sb . (Nseq . n) by FUNCT_2:15;
then (sb * Nseq) . n in SB . (Nseq . n) by A24;
then u in (T . (Nseq . n)) /\ B by A16, A32;
then u in B by XBOOLE_0:def_4;
hence u in [.e,f.] by A3; ::_thesis: verum
end;
then consider fb being Real_Sequence such that
A33: fb is subsequence of sb * Nseq and
A34: fb is convergent and
A35: lim fb in [.e,f.] by RCOMP_1:def_3;
consider Nseq1 being increasing sequence of NAT such that
A36: fb = (sb * Nseq) * Nseq1 by A33, VALUED_0:def_17;
set fa = ga * Nseq1;
set r = ((lim (ga * Nseq1)) + (lim fb)) / 2;
set d0 = dist (A,B);
set ff = (1 / 2) (#) ((ga * Nseq1) + fb);
A37: ga * Nseq1 is convergent by A28, SEQ_4:16;
then A38: (ga * Nseq1) + fb is convergent by A34, SEQ_2:5;
then A39: (1 / 2) (#) ((ga * Nseq1) + fb) is convergent by SEQ_2:7;
T . 0 meets A by A13;
then not A is empty by XBOOLE_1:65;
then dist (A,B) > 0 by A1, A14, Th11;
then A40: (dist (A,B)) / 2 > 0 by XREAL_1:139;
((lim (ga * Nseq1)) + (lim fb)) / 2 = (1 / 2) * ((lim (ga * Nseq1)) + (lim fb))
.= (1 / 2) * (lim ((ga * Nseq1) + fb)) by A34, A37, SEQ_2:6
.= lim ((1 / 2) (#) ((ga * Nseq1) + fb)) by A38, SEQ_2:8 ;
then consider k0 being Element of NAT such that
A41: for i being Element of NAT st k0 <= i holds
abs ((((1 / 2) (#) ((ga * Nseq1) + fb)) . i) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist (A,B)) / 2 by A39, A40, SEQ_2:def_7;
take ((lim (ga * Nseq1)) + (lim fb)) / 2 ; ::_thesis: ( ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] & not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) )
lim (ga * Nseq1) = lim ga by A28, SEQ_4:17;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] by A29, A35, Th1; ::_thesis: ( not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B & ( for i being Element of NAT ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) )
now__::_thesis:_not_((lim_(ga_*_Nseq1))_+_(lim_fb))_/_2_in_A_\/_B
set i = Nseq . (Nseq1 . k0);
set di = dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))));
A42: 2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) = (abs 2) * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by ABSVALUE:def_1
.= abs (2 * ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:65
.= abs (((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) ;
A43: (ga * Nseq1) . k0 = ga . (Nseq1 . k0) by FUNCT_2:15
.= sa . (Nseq . (Nseq1 . k0)) by A30, FUNCT_2:15 ;
T . (Nseq . (Nseq1 . k0)) meets B by A13;
then (T . (Nseq . (Nseq1 . k0))) /\ B <> {} by XBOOLE_0:def_7;
then A44: not SB . (Nseq . (Nseq1 . k0)) is empty by A16;
A45: SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16;
then A46: SB . (Nseq . (Nseq1 . k0)) c= B by XBOOLE_1:17;
A47: SB . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A45, XBOOLE_1:17;
A48: SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15;
then A49: SA . (Nseq . (Nseq1 . k0)) c= A by XBOOLE_1:17;
T . (Nseq . (Nseq1 . k0)) meets A by A13;
then (T . (Nseq . (Nseq1 . k0))) /\ A <> {} by XBOOLE_0:def_7;
then A50: not SA . (Nseq . (Nseq1 . k0)) is empty by A15;
then A51: dist (A,B) <= dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A44, A49, A46, Th8;
(dist (A,B)) / 2 <= (dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2 by A50, A44, A49, A46, Th8, XREAL_1:72;
then A52: ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) + ((dist (A,B)) / 2) <= ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) + ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) by XREAL_1:6;
((1 / 2) (#) ((ga * Nseq1) + fb)) . k0 = (1 / 2) * (((ga * Nseq1) + fb) . k0) by SEQ_1:9
.= (((ga * Nseq1) + fb) . k0) / 2
.= (((ga * Nseq1) . k0) + (fb . k0)) / 2 by SEQ_1:7 ;
then A53: abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist (A,B)) / 2 by A41;
( not T . (Nseq . (Nseq1 . k0)) is empty & T . (Nseq . (Nseq1 . k0)) is closed_interval ) by A13;
then A54: ex a, b being Real st
( a <= b & T . (Nseq . (Nseq1 . k0)) = [.a,b.] ) by MEASURE5:14;
A55: sb . (Nseq . (Nseq1 . k0)) in SB . (Nseq . (Nseq1 . k0)) by A24;
A56: SA . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A48, XBOOLE_1:17;
A57: fb . k0 = (sb * Nseq) . (Nseq1 . k0) by A36, FUNCT_2:15
.= sb . (Nseq . (Nseq1 . k0)) by FUNCT_2:15 ;
2 * ((dist (A,B)) / 2) = dist (A,B) ;
then A58: 2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist (A,B) by A53, A43, A57, XREAL_1:68;
A59: sa . (Nseq . (Nseq1 . k0)) in SA . (Nseq . (Nseq1 . k0)) by A24;
then A60: dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) by A55, Th7;
A61: now__::_thesis:_((lim_(ga_*_Nseq1))_+_(lim_fb))_/_2_in_T_._(Nseq_._(Nseq1_._k0))
percases ( sa . (Nseq . (Nseq1 . k0)) <= sb . (Nseq . (Nseq1 . k0)) or sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ) ;
suppose sa . (Nseq . (Nseq1 . k0)) <= sb . (Nseq . (Nseq1 . k0)) ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0))
then (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) >= 0 by XREAL_1:48;
then dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A60, ABSVALUE:def_1;
then dist (A,B) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A51, XXREAL_0:2;
then abs (((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A58, A42, XXREAL_0:2;
then A62: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] by RCOMP_1:2;
[.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A54, A59, A55, A56, A47, XXREAL_2:def_12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A62; ::_thesis: verum
end;
supposeA63: sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0))
A64: abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) = abs ((sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0)))) by UNIFORM1:11;
(sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) >= 0 by A63, XREAL_1:48;
then dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A60, A64, ABSVALUE:def_1;
then dist (A,B) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A51, XXREAL_0:2;
then abs (((sb . (Nseq . (Nseq1 . k0))) + (sa . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A58, A42, XXREAL_0:2;
then A65: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] by RCOMP_1:2;
[.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A54, A59, A55, A56, A47, XXREAL_2:def_12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A65; ::_thesis: verum
end;
end;
end;
assume A66: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; ::_thesis: contradiction
percases ( ((lim (ga * Nseq1)) + (lim fb)) / 2 in B or ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ) by A66, XBOOLE_0:def_3;
supposeA67: ((lim (ga * Nseq1)) + (lim fb)) / 2 in B ; ::_thesis: contradiction
SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16;
then A68: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SB . (Nseq . (Nseq1 . k0)) by A61, A67, XBOOLE_0:def_4;
A69: abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2) = (abs (((ga * Nseq1) . k0) - (fb . k0))) / (abs 2) by COMPLEX1:67
.= (abs (((ga * Nseq1) . k0) - (fb . k0))) / 2 by ABSVALUE:def_1 ;
((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) = ((((ga * Nseq1) . k0) - (fb . k0)) / 2) + (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) ;
then A70: abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) <= (abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + (abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:56;
(abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + (abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < (abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + ((dist (A,B)) / 2) by A53, XREAL_1:6;
then abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs (((ga * Nseq1) . k0) - (fb . k0))) / 2) + ((dist (A,B)) / 2) by A70, A69, XXREAL_0:2;
then abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) + ((dist (A,B)) / 2) by A24, A43, A57;
then A71: abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A52, XXREAL_0:2;
(ga * Nseq1) . k0 in SA . (Nseq . (Nseq1 . k0)) by A24, A43;
hence contradiction by A68, A71, Th7; ::_thesis: verum
end;
supposeA72: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ; ::_thesis: contradiction
SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15;
then A73: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SA . (Nseq . (Nseq1 . k0)) by A61, A72, XBOOLE_0:def_4;
A74: abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2) = (abs ((fb . k0) - ((ga * Nseq1) . k0))) / (abs 2) by COMPLEX1:67
.= (abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2 by ABSVALUE:def_1 ;
(fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) = (((fb . k0) - ((ga * Nseq1) . k0)) / 2) + ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) ;
then A75: abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) <= (abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + (abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:56;
A76: abs ((fb . k0) - ((ga * Nseq1) . k0)) = abs (((ga * Nseq1) . k0) - (fb . k0)) by UNIFORM1:11
.= dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A24, A43, A57 ;
(abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + (abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < (abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + ((dist (A,B)) / 2) by A53, XREAL_1:6;
then abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2) + ((dist (A,B)) / 2) by A75, A74, XXREAL_0:2;
then A77: abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A52, A76, XXREAL_0:2;
fb . k0 in SB . (Nseq . (Nseq1 . k0)) by A24, A57;
hence contradiction by A73, A77, Th7; ::_thesis: verum
end;
end;
end;
hence not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; ::_thesis: for i being Element of NAT ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k )
let i be Element of NAT ; ::_thesis: ex k being Element of NAT st
( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k )
set k = max (k0,i);
take j = Nseq . (Nseq1 . (max (k0,i))); ::_thesis: ( i <= j & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j )
A78: fb . (max (k0,i)) = (sb * Nseq) . (Nseq1 . (max (k0,i))) by A36, FUNCT_2:15
.= sb . j by FUNCT_2:15 ;
A79: i <= max (k0,i) by XXREAL_0:25;
A80: sb . j in SB . j by A24;
T . j meets B by A13;
then (T . j) /\ B <> {} by XBOOLE_0:def_7;
then A81: not SB . j is empty by A16;
A82: dom Nseq = NAT by FUNCT_2:def_1;
T . j meets A by A13;
then (T . j) /\ A <> {} by XBOOLE_0:def_7;
then A83: not SA . j is empty by A15;
A84: i <= Nseq . i by SEQM_3:14;
A85: SA . j = (T . j) /\ A by A15;
then A86: SA . j c= T . j by XBOOLE_1:17;
((1 / 2) (#) ((ga * Nseq1) + fb)) . (max (k0,i)) = (1 / 2) * (((ga * Nseq1) + fb) . (max (k0,i))) by SEQ_1:9
.= (((ga * Nseq1) + fb) . (max (k0,i))) / 2
.= (((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2 by SEQ_1:7 ;
then A87: abs (((((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist (A,B)) / 2 by A41, XXREAL_0:25;
A88: 2 * ((dist (A,B)) / 2) = dist (A,B) ;
(ga * Nseq1) . (max (k0,i)) = ga . (Nseq1 . (max (k0,i))) by FUNCT_2:15
.= sa . j by A30, FUNCT_2:15 ;
then A89: 2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist (A,B) by A87, A78, A88, XREAL_1:68;
( not T . j is empty & T . j is closed_interval ) by A13;
then A90: ex a, b being Real st
( a <= b & T . j = [.a,b.] ) by MEASURE5:14;
A91: SB . j = (T . j) /\ B by A16;
then A92: SB . j c= B by XBOOLE_1:17;
A93: SB . j c= T . j by A91, XBOOLE_1:17;
dom Nseq1 = NAT by FUNCT_2:def_1;
then Nseq1 . i <= Nseq1 . (max (k0,i)) by A79, VALUED_0:def_15;
then A94: Nseq . (Nseq1 . i) <= j by A82, VALUED_0:def_15;
i <= Nseq1 . i by SEQM_3:14;
then Nseq . i <= Nseq . (Nseq1 . i) by A82, VALUED_0:def_15;
then i <= Nseq . (Nseq1 . i) by A84, XXREAL_0:2;
hence i <= j by A94, XXREAL_0:2; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j
set di = dist ((SA . j),(SB . j));
A95: 2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) = (abs 2) * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by ABSVALUE:def_1
.= abs (2 * ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:65
.= abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) ;
SA . j c= A by A85, XBOOLE_1:17;
then A96: dist (A,B) <= dist ((SA . j),(SB . j)) by A83, A81, A92, Th8;
A97: sa . j in SA . j by A24;
then A98: dist ((SA . j),(SB . j)) <= abs ((sb . j) - (sa . j)) by A80, Th7;
A99: now__::_thesis:_((lim_(ga_*_Nseq1))_+_(lim_fb))_/_2_in_T_._j
percases ( sa . j <= sb . j or sb . j <= sa . j ) ;
suppose sa . j <= sb . j ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j
then (sb . j) - (sa . j) >= 0 by XREAL_1:48;
then dist ((SA . j),(SB . j)) <= (sb . j) - (sa . j) by A98, ABSVALUE:def_1;
then dist (A,B) <= (sb . j) - (sa . j) by A96, XXREAL_0:2;
then abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sb . j) - (sa . j) by A89, A95, XXREAL_0:2;
then A100: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . j),(sb . j).] by RCOMP_1:2;
[.(sa . j),(sb . j).] c= T . j by A90, A97, A80, A86, A93, XXREAL_2:def_12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A100; ::_thesis: verum
end;
supposeA101: sb . j <= sa . j ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j
A102: abs ((sb . j) - (sa . j)) = abs ((sa . j) - (sb . j)) by UNIFORM1:11;
(sa . j) - (sb . j) >= 0 by A101, XREAL_1:48;
then dist ((SA . j),(SB . j)) <= (sa . j) - (sb . j) by A98, A102, ABSVALUE:def_1;
then dist (A,B) <= (sa . j) - (sb . j) by A96, XXREAL_0:2;
then abs (((sb . j) + (sa . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sa . j) - (sb . j) by A89, A95, XXREAL_0:2;
then A103: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . j),(sa . j).] by RCOMP_1:2;
[.(sb . j),(sa . j).] c= T . j by A90, A97, A80, A86, A93, XXREAL_2:def_12;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A103; ::_thesis: verum
end;
end;
end;
T . j c= S . j by A13;
hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j by A99; ::_thesis: verum
end;
theorem Th13: :: JCT_MISC:13
for S being closed Subset of (TOP-REAL 2) st S is bounded holds
proj2 .: S is closed
proof
let S be closed Subset of (TOP-REAL 2); ::_thesis: ( S is bounded implies proj2 .: S is closed )
assume S is bounded ; ::_thesis: proj2 .: S is closed
then Cl (proj2 .: S) = proj2 .: (Cl S) by TOPREAL6:84
.= proj2 .: S by PRE_TOPC:22 ;
hence proj2 .: S is closed ; ::_thesis: verum
end;
theorem Th14: :: JCT_MISC:14
for S being Subset of (TOP-REAL 2) st S is bounded holds
proj2 .: S is real-bounded
proof
let S be Subset of (TOP-REAL 2); ::_thesis: ( S is bounded implies proj2 .: S is real-bounded )
assume S is bounded ; ::_thesis: proj2 .: S is real-bounded
then reconsider C = S as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r being Real, x being Point of (Euclid 2) such that
A1: 0 < r and
A2: C c= Ball (x,r) by METRIC_6:def_3;
reconsider P = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:8;
reconsider p = x as Point of (TOP-REAL 2) by TOPREAL3:8;
set t = max ((abs ((p `2) - r)),(abs ((p `2) + r)));
now__::_thesis:_(_abs_((p_`2)_-_r)_<=_0_implies_not_abs_((p_`2)_+_r)_<=_0_)
assume that
A3: abs ((p `2) - r) <= 0 and
A4: abs ((p `2) + r) <= 0 ; ::_thesis: contradiction
abs ((p `2) - r) = 0 by A3, COMPLEX1:46;
then abs (r - (p `2)) = 0 by UNIFORM1:11;
then A5: r - (p `2) = 0 by ABSVALUE:2;
abs ((p `2) + r) = 0 by A4, COMPLEX1:46;
hence contradiction by A1, A5, ABSVALUE:2; ::_thesis: verum
end;
then A6: max ((abs ((p `2) - r)),(abs ((p `2) + r))) > 0 by XXREAL_0:30;
A7: proj2 .: P = ].((p `2) - r),((p `2) + r).[ by TOPREAL6:44;
for s being real number st s in proj2 .: S holds
abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r)))
proof
let s be real number ; ::_thesis: ( s in proj2 .: S implies abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r))) )
proj2 .: S c= proj2 .: P by A2, RELAT_1:123;
hence ( s in proj2 .: S implies abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r))) ) by A7, Th3; ::_thesis: verum
end;
hence proj2 .: S is real-bounded by A6, SEQ_4:4; ::_thesis: verum
end;
theorem :: JCT_MISC:15
for S being compact Subset of (TOP-REAL 2) holds proj2 .: S is compact
proof
let S be compact Subset of (TOP-REAL 2); ::_thesis: proj2 .: S is compact
proj2 .: S is closed by Th13;
hence proj2 .: S is compact by Th14, RCOMP_1:11; ::_thesis: verum
end;