:: RCOMP_1 semantic presentation
begin
definition
let g, s be real number ;
:: original: [.
redefine func[.g,s.] -> Subset of REAL equals :: RCOMP_1:def 1
{ r where r is Real : ( g <= r & r <= s ) } ;
coherence
[.g,s.] is Subset of REAL
proof
now__::_thesis:_for_x_being_set_st_x_in_[.g,s.]_holds_
x_in_REAL
let x be set ; ::_thesis: ( x in [.g,s.] implies x in REAL )
assume x in [.g,s.] ; ::_thesis: x in REAL
then A1: ex r being Element of ExtREAL st
( x = r & g <= r & r <= s ) ;
( g in REAL & s in REAL ) by XREAL_0:def_1;
hence x in REAL by A1, XXREAL_0:45; ::_thesis: verum
end;
hence [.g,s.] is Subset of REAL by TARSKI:def_3; ::_thesis: verum
end;
compatibility
for b1 being Subset of REAL holds
( b1 = [.g,s.] iff b1 = { r where r is Real : ( g <= r & r <= s ) } )
proof
set Y = { r where r is Real : ( g <= r & r <= s ) } ;
let X be Subset of REAL; ::_thesis: ( X = [.g,s.] iff X = { r where r is Real : ( g <= r & r <= s ) } )
A2: [.g,s.] c= { r where r is Real : ( g <= r & r <= s ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.g,s.] or x in { r where r is Real : ( g <= r & r <= s ) } )
assume x in [.g,s.] ; ::_thesis: x in { r where r is Real : ( g <= r & r <= s ) }
then consider r being Element of ExtREAL such that
A3: x = r and
A4: ( g <= r & r <= s ) ;
( g in REAL & s in REAL ) by XREAL_0:def_1;
then r in REAL by A4, XXREAL_0:45;
hence x in { r where r is Real : ( g <= r & r <= s ) } by A3, A4; ::_thesis: verum
end;
{ r where r is Real : ( g <= r & r <= s ) } c= [.g,s.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Real : ( g <= r & r <= s ) } or x in [.g,s.] )
assume x in { r where r is Real : ( g <= r & r <= s ) } ; ::_thesis: x in [.g,s.]
then consider r being Element of REAL such that
A5: ( x = r & g <= r & r <= s ) ;
r in REAL ;
hence x in [.g,s.] by A5, NUMBERS:31; ::_thesis: verum
end;
hence ( X = [.g,s.] iff X = { r where r is Real : ( g <= r & r <= s ) } ) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines [. RCOMP_1:def_1_:_
for g, s being real number holds [.g,s.] = { r where r is Real : ( g <= r & r <= s ) } ;
definition
let g, s be ext-real number ;
:: original: ].
redefine func].g,s.[ -> Subset of REAL equals :: RCOMP_1:def 2
{ r where r is Real : ( g < r & r < s ) } ;
coherence
].g,s.[ is Subset of REAL
proof
now__::_thesis:_for_x_being_set_st_x_in_].g,s.[_holds_
x_in_REAL
let x be set ; ::_thesis: ( x in ].g,s.[ implies x in REAL )
assume x in ].g,s.[ ; ::_thesis: x in REAL
then ex r being Element of ExtREAL st
( x = r & g < r & r < s ) ;
hence x in REAL by XXREAL_0:48; ::_thesis: verum
end;
hence ].g,s.[ is Subset of REAL by TARSKI:def_3; ::_thesis: verum
end;
compatibility
for b1 being Subset of REAL holds
( b1 = ].g,s.[ iff b1 = { r where r is Real : ( g < r & r < s ) } )
proof
set Y = { r where r is Real : ( g < r & r < s ) } ;
let X be Subset of REAL; ::_thesis: ( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } )
A1: { r where r is Real : ( g < r & r < s ) } c= ].g,s.[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Real : ( g < r & r < s ) } or x in ].g,s.[ )
assume x in { r where r is Real : ( g < r & r < s ) } ; ::_thesis: x in ].g,s.[
then consider r being Element of REAL such that
A2: ( x = r & g < r & r < s ) ;
r in REAL ;
hence x in ].g,s.[ by A2, NUMBERS:31; ::_thesis: verum
end;
].g,s.[ c= { r where r is Real : ( g < r & r < s ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].g,s.[ or x in { r where r is Real : ( g < r & r < s ) } )
assume x in ].g,s.[ ; ::_thesis: x in { r where r is Real : ( g < r & r < s ) }
then consider r being Element of ExtREAL such that
A3: x = r and
A4: ( g < r & r < s ) ;
r in REAL by A4, XXREAL_0:48;
hence x in { r where r is Real : ( g < r & r < s ) } by A3, A4; ::_thesis: verum
end;
hence ( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } ) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines ]. RCOMP_1:def_2_:_
for g, s being ext-real number holds ].g,s.[ = { r where r is Real : ( g < r & r < s ) } ;
theorem Th1: :: RCOMP_1:1
for r, p, g being real number holds
( r in ].(p - g),(p + g).[ iff abs (r - p) < g )
proof
let r, p, g be real number ; ::_thesis: ( r in ].(p - g),(p + g).[ iff abs (r - p) < g )
thus ( r in ].(p - g),(p + g).[ implies abs (r - p) < g ) ::_thesis: ( abs (r - p) < g implies r in ].(p - g),(p + g).[ )
proof
assume r in ].(p - g),(p + g).[ ; ::_thesis: abs (r - p) < g
then A1: ex s being Real st
( r = s & p - g < s & s < p + g ) ;
then p + (- g) < r ;
then A2: - g < r - p by XREAL_1:20;
r - p < g by A1, XREAL_1:19;
hence abs (r - p) < g by A2, SEQ_2:1; ::_thesis: verum
end;
assume A3: abs (r - p) < g ; ::_thesis: r in ].(p - g),(p + g).[
then r - p < g by SEQ_2:1;
then A4: r < p + g by XREAL_1:19;
- g < r - p by A3, SEQ_2:1;
then ( r is Real & p + (- g) < r ) by XREAL_0:def_1, XREAL_1:20;
hence r in ].(p - g),(p + g).[ by A4; ::_thesis: verum
end;
theorem :: RCOMP_1:2
for r, p, g being real number holds
( r in [.p,g.] iff abs ((p + g) - (2 * r)) <= g - p )
proof
let r, p, g be real number ; ::_thesis: ( r in [.p,g.] iff abs ((p + g) - (2 * r)) <= g - p )
thus ( r in [.p,g.] implies abs ((p + g) - (2 * r)) <= g - p ) ::_thesis: ( abs ((p + g) - (2 * r)) <= g - p implies r in [.p,g.] )
proof
assume r in [.p,g.] ; ::_thesis: abs ((p + g) - (2 * r)) <= g - p
then A1: ex s being Real st
( s = r & p <= s & s <= g ) ;
then 2 * r <= 2 * g by XREAL_1:64;
then - (2 * r) >= - (2 * g) by XREAL_1:24;
then (p + g) + (- (2 * r)) >= (p + g) + (- (2 * g)) by XREAL_1:7;
then A2: (p + g) - (2 * r) >= - (g - p) ;
2 * p <= 2 * r by A1, XREAL_1:64;
then - (2 * p) >= - (2 * r) by XREAL_1:24;
then (p + g) + (- (2 * p)) >= (p + g) + (- (2 * r)) by XREAL_1:7;
hence abs ((p + g) - (2 * r)) <= g - p by A2, ABSVALUE:5; ::_thesis: verum
end;
assume A3: abs ((p + g) - (2 * r)) <= g - p ; ::_thesis: r in [.p,g.]
then (p + g) - (2 * r) >= - (g - p) by ABSVALUE:5;
then p + g >= (p - g) + (2 * r) by XREAL_1:19;
then (p + g) - (p - g) >= 2 * r by XREAL_1:19;
then A4: (1 / 2) * (2 * g) >= (1 / 2) * (2 * r) by XREAL_1:64;
g - p >= (p + g) - (2 * r) by A3, ABSVALUE:5;
then (2 * r) + (g - p) >= p + g by XREAL_1:20;
then 2 * r >= (p + g) - (g - p) by XREAL_1:20;
then (1 / 2) * (2 * r) >= (1 / 2) * (2 * p) by XREAL_1:64;
hence r in [.p,g.] by A4; ::_thesis: verum
end;
theorem :: RCOMP_1:3
for r, p, g being real number holds
( r in ].p,g.[ iff abs ((p + g) - (2 * r)) < g - p )
proof
let r, p, g be real number ; ::_thesis: ( r in ].p,g.[ iff abs ((p + g) - (2 * r)) < g - p )
thus ( r in ].p,g.[ implies abs ((p + g) - (2 * r)) < g - p ) ::_thesis: ( abs ((p + g) - (2 * r)) < g - p implies r in ].p,g.[ )
proof
assume r in ].p,g.[ ; ::_thesis: abs ((p + g) - (2 * r)) < g - p
then A1: ex s being Real st
( s = r & p < s & s < g ) ;
then 2 * r < 2 * g by XREAL_1:68;
then - (2 * r) > - (2 * g) by XREAL_1:24;
then (p + g) + (- (2 * r)) > (p + g) + (- (2 * g)) by XREAL_1:6;
then A2: (p + g) - (2 * r) > - (g - p) ;
2 * p < 2 * r by A1, XREAL_1:68;
then - (2 * p) > - (2 * r) by XREAL_1:24;
then (p + g) + (- (2 * p)) > (p + g) + (- (2 * r)) by XREAL_1:6;
hence abs ((p + g) - (2 * r)) < g - p by A2, SEQ_2:1; ::_thesis: verum
end;
assume A3: abs ((p + g) - (2 * r)) < g - p ; ::_thesis: r in ].p,g.[
then (p + g) - (2 * r) > - (g - p) by SEQ_2:1;
then p + g > (p - g) + (2 * r) by XREAL_1:20;
then (p + g) - (p - g) > 2 * r by XREAL_1:20;
then A4: (1 / 2) * (2 * g) > (1 / 2) * (2 * r) by XREAL_1:68;
g - p > (p + g) - (2 * r) by A3, SEQ_2:1;
then (2 * r) + (g - p) > p + g by XREAL_1:19;
then 2 * r > (p + g) - (g - p) by XREAL_1:19;
then (1 / 2) * (2 * r) > (1 / 2) * (2 * p) by XREAL_1:68;
hence r in ].p,g.[ by A4; ::_thesis: verum
end;
definition
let X be Subset of REAL;
attrX is compact means :Def3: :: RCOMP_1:def 3
for s1 being Real_Sequence st rng s1 c= X holds
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X );
end;
:: deftheorem Def3 defines compact RCOMP_1:def_3_:_
for X being Subset of REAL holds
( X is compact iff for s1 being Real_Sequence st rng s1 c= X holds
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );
definition
let X be Subset of REAL;
attrX is closed means :Def4: :: RCOMP_1:def 4
for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X;
end;
:: deftheorem Def4 defines closed RCOMP_1:def_4_:_
for X being Subset of REAL holds
( X is closed iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X );
definition
let X be Subset of REAL;
attrX is open means :Def5: :: RCOMP_1:def 5
X ` is closed ;
end;
:: deftheorem Def5 defines open RCOMP_1:def_5_:_
for X being Subset of REAL holds
( X is open iff X ` is closed );
theorem Th4: :: RCOMP_1:4
for s, g being real number
for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
s1 is bounded
proof
let s, g be real number ; ::_thesis: for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
s1 is bounded
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [.s,g.] implies s1 is bounded )
assume A1: rng s1 c= [.s,g.] ; ::_thesis: s1 is bounded
thus s1 is bounded_above :: according to SEQ_2:def_8 ::_thesis: s1 is bounded_below
proof
take r = g + 1; :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not r <= s1 . b1
A2: for t being real number st t in rng s1 holds
t < r
proof
let t be real number ; ::_thesis: ( t in rng s1 implies t < r )
assume t in rng s1 ; ::_thesis: t < r
then t in [.s,g.] by A1;
then A3: ex p being Real st
( t = p & s <= p & p <= g ) ;
g < r by XREAL_1:29;
hence t < r by A3, XXREAL_0:2; ::_thesis: verum
end;
for n being Element of NAT holds s1 . n < r
proof
let n be Element of NAT ; ::_thesis: s1 . n < r
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then s1 . n in rng s1 by FUNCT_1:def_3;
hence s1 . n < r by A2; ::_thesis: verum
end;
hence for b1 being Element of NAT holds not r <= s1 . b1 ; ::_thesis: verum
end;
thus s1 is bounded_below ::_thesis: verum
proof
take r = s - 1; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not s1 . b1 <= r
A4: r + 1 = s - (1 - 1) ;
A5: for t being real number st t in rng s1 holds
r < t
proof
let t be real number ; ::_thesis: ( t in rng s1 implies r < t )
assume t in rng s1 ; ::_thesis: r < t
then t in [.s,g.] by A1;
then A6: ex p being Real st
( t = p & s <= p & p <= g ) ;
r < s by A4, XREAL_1:29;
hence r < t by A6, XXREAL_0:2; ::_thesis: verum
end;
for n being Element of NAT holds r < s1 . n
proof
let n be Element of NAT ; ::_thesis: r < s1 . n
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then s1 . n in rng s1 by FUNCT_1:def_3;
hence r < s1 . n by A5; ::_thesis: verum
end;
hence for b1 being Element of NAT holds not s1 . b1 <= r ; ::_thesis: verum
end;
end;
theorem Th5: :: RCOMP_1:5
for s, g being real number holds [.s,g.] is closed
proof
let s, g be real number ; ::_thesis: [.s,g.] is closed
for s1 being Real_Sequence st rng s1 c= [.s,g.] & s1 is convergent holds
lim s1 in [.s,g.]
proof
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [.s,g.] & s1 is convergent implies lim s1 in [.s,g.] )
assume that
A1: rng s1 c= [.s,g.] and
A2: s1 is convergent ; ::_thesis: lim s1 in [.s,g.]
A3: s <= lim s1
proof
s in REAL by XREAL_0:def_1;
then reconsider s2 = NAT --> s as Real_Sequence by FUNCOP_1:45;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_s2_._n_<=_s1_._n
let n be Element of NAT ; ::_thesis: s2 . n <= s1 . n
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then s1 . n in rng s1 by FUNCT_1:def_3;
then s1 . n in [.s,g.] by A1;
then ex p being Real st
( s1 . n = p & s <= p & p <= g ) ;
hence s2 . n <= s1 . n by FUNCOP_1:7; ::_thesis: verum
end;
s2 . 0 = s by FUNCOP_1:7;
then lim s2 = s by SEQ_4:25;
hence s <= lim s1 by A2, A4, SEQ_2:18; ::_thesis: verum
end;
lim s1 <= g
proof
g in REAL by XREAL_0:def_1;
then reconsider s2 = NAT --> g as Real_Sequence by FUNCOP_1:45;
A5: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<=_s2_._n
let n be Element of NAT ; ::_thesis: s1 . n <= s2 . n
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then s1 . n in rng s1 by FUNCT_1:def_3;
then s1 . n in [.s,g.] by A1;
then ex p being Real st
( s1 . n = p & s <= p & p <= g ) ;
hence s1 . n <= s2 . n by FUNCOP_1:7; ::_thesis: verum
end;
s2 . 0 = g by FUNCOP_1:7;
then lim s2 = g by SEQ_4:25;
hence lim s1 <= g by A2, A5, SEQ_2:18; ::_thesis: verum
end;
hence lim s1 in [.s,g.] by A3; ::_thesis: verum
end;
hence [.s,g.] is closed by Def4; ::_thesis: verum
end;
theorem :: RCOMP_1:6
for s, g being real number holds [.s,g.] is compact
proof
let s, g be real number ; ::_thesis: [.s,g.] is compact
for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] )
proof
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [.s,g.] implies ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) )
A1: [.s,g.] is closed by Th5;
assume A2: rng s1 c= [.s,g.] ; ::_thesis: ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] )
then consider s2 being Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent by Th4, SEQ_4:40;
take s2 ; ::_thesis: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] )
ex Nseq being increasing sequence of NAT st s2 = s1 * Nseq by A3, VALUED_0:def_17;
then rng s2 c= rng s1 by RELAT_1:26;
then rng s2 c= [.s,g.] by A2, XBOOLE_1:1;
hence ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) by A3, A4, A1, Def4; ::_thesis: verum
end;
hence [.s,g.] is compact by Def3; ::_thesis: verum
end;
theorem Th7: :: RCOMP_1:7
for p, q being real number holds ].p,q.[ is open
proof
let p, q be real number ; ::_thesis: ].p,q.[ is open
defpred S1[ Real] means ( $1 <= p or q <= $1 );
consider X being Subset of REAL such that
A1: for r being Real holds
( r in X iff S1[r] ) from SUBSET_1:sch_3();
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_holds_
lim_s1_in_X
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent implies lim s1 in X )
assume that
A2: rng s1 c= X and
A3: s1 is convergent ; ::_thesis: lim s1 in X
( lim s1 <= p or q <= lim s1 )
proof
assume A4: ( not lim s1 <= p & not q <= lim s1 ) ; ::_thesis: contradiction
then 0 < (lim s1) - p by XREAL_1:50;
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
abs ((s1 . m) - (lim s1)) < (lim s1) - p by A3, SEQ_2:def_7;
0 < q - (lim s1) by A4, XREAL_1:50;
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < q - (lim s1) by A3, SEQ_2:def_7;
consider k being Element of NAT such that
A7: max (n,n1) < k by SEQ_4:3;
n1 <= max (n,n1) by XXREAL_0:25;
then n1 <= k by A7, XXREAL_0:2;
then A8: abs ((s1 . k) - (lim s1)) < (lim s1) - p by A5;
- (abs ((s1 . k) - (lim s1))) <= (s1 . k) - (lim s1) by ABSVALUE:4;
then - ((s1 . k) - (lim s1)) <= - (- (abs ((s1 . k) - (lim s1)))) by XREAL_1:24;
then - ((s1 . k) - (lim s1)) < (lim s1) - p by A8, XXREAL_0:2;
then - ((lim s1) - p) < - (- ((s1 . k) - (lim s1))) by XREAL_1:24;
then p - (lim s1) < (s1 . k) - (lim s1) ;
then A9: p < s1 . k by XREAL_1:9;
n <= max (n,n1) by XXREAL_0:25;
then n <= k by A7, XXREAL_0:2;
then ( (s1 . k) - (lim s1) <= abs ((s1 . k) - (lim s1)) & abs ((s1 . k) - (lim s1)) < q - (lim s1) ) by A6, ABSVALUE:4;
then (s1 . k) - (lim s1) < q - (lim s1) by XXREAL_0:2;
then A10: s1 . k < q by XREAL_1:9;
dom s1 = NAT by FUNCT_2:def_1;
then s1 . k in rng s1 by FUNCT_1:def_3;
hence contradiction by A1, A2, A10, A9; ::_thesis: verum
end;
hence lim s1 in X by A1; ::_thesis: verum
end;
then A11: X is closed by Def4;
now__::_thesis:_for_r_being_real_number_st_r_in_].p,q.[_`_holds_
r_in_X
let r be real number ; ::_thesis: ( r in ].p,q.[ ` implies r in X )
A12: r is Real by XREAL_0:def_1;
assume r in ].p,q.[ ` ; ::_thesis: r in X
then not r in ].p,q.[ by XBOOLE_0:def_5;
then ( r <= p or q <= r ) by A12;
hence r in X by A1, A12; ::_thesis: verum
end;
then A13: ].p,q.[ ` c= X by MEMBERED:def_9;
now__::_thesis:_for_r_being_real_number_st_r_in_X_holds_
r_in_].p,q.[_`
let r be real number ; ::_thesis: ( r in X implies r in ].p,q.[ ` )
assume r in X ; ::_thesis: r in ].p,q.[ `
then for s being Real holds
( not s = r or not p < s or not s < q ) by A1;
then ( r is Real & not r in ].p,q.[ ) by XREAL_0:def_1;
hence r in ].p,q.[ ` by XBOOLE_0:def_5; ::_thesis: verum
end;
then X c= ].p,q.[ ` by MEMBERED:def_9;
then ].p,q.[ ` = X by A13, XBOOLE_0:def_10;
hence ].p,q.[ is open by A11, Def5; ::_thesis: verum
end;
registration
let p, q be real number ;
cluster].p,q.[ -> open for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = ].p,q.[ holds
b1 is open by Th7;
cluster[.p,q.] -> closed for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = [.p,q.] holds
b1 is closed by Th5;
end;
theorem Th8: :: RCOMP_1:8
for X being Subset of REAL st X is compact holds
X is closed
proof
let X be Subset of REAL; ::_thesis: ( X is compact implies X is closed )
assume A1: X is compact ; ::_thesis: X is closed
assume not X is closed ; ::_thesis: contradiction
then consider s1 being Real_Sequence such that
A2: rng s1 c= X and
A3: ( s1 is convergent & not lim s1 in X ) by Def4;
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A1, A2, Def3;
hence contradiction by A3, SEQ_4:17; ::_thesis: verum
end;
registration
cluster compact -> closed for Element of K19(REAL);
coherence
for b1 being Subset of REAL st b1 is compact holds
b1 is closed by Th8;
end;
theorem Th9: :: RCOMP_1:9
for s1 being Real_Sequence
for X being Subset of REAL st ( for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - p) ) ) ) holds
for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds
not lim s2 in X
proof
let s1 be Real_Sequence; ::_thesis: for X being Subset of REAL st ( for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - p) ) ) ) holds
for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds
not lim s2 in X
let X be Subset of REAL; ::_thesis: ( ( for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - p) ) ) ) implies for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds
not lim s2 in X )
assume that
A1: for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - p) ) ) and
A2: ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ; ::_thesis: contradiction
consider s2 being Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent and
A5: lim s2 in X by A2;
consider r being real number , n being Element of NAT such that
A6: 0 < r and
A7: for m being Element of NAT st n < m holds
r < abs ((s1 . m) - (lim s2)) by A1, A5;
consider n1 being Element of NAT such that
A8: for m being Element of NAT st n1 <= m holds
abs ((s2 . m) - (lim s2)) < r by A4, A6, SEQ_2:def_7;
consider NS being increasing sequence of NAT such that
A9: s2 = s1 * NS by A3, VALUED_0:def_17;
set k = (n + 1) + n1;
abs (((s1 * NS) . ((n + 1) + n1)) - (lim s2)) < r by A8, A9, NAT_1:11;
then A10: abs ((s1 . (NS . ((n + 1) + n1))) - (lim s2)) < r by FUNCT_2:15;
n + 1 <= (n + 1) + n1 by NAT_1:11;
then A11: n < (n + 1) + n1 by NAT_1:13;
(n + 1) + n1 <= NS . ((n + 1) + n1) by SEQM_3:14;
then n < NS . ((n + 1) + n1) by A11, XXREAL_0:2;
hence contradiction by A7, A10; ::_thesis: verum
end;
theorem Th10: :: RCOMP_1:10
for X being Subset of REAL st X is compact holds
X is real-bounded
proof
let X be Subset of REAL; ::_thesis: ( X is compact implies X is real-bounded )
assume A1: X is compact ; ::_thesis: X is real-bounded
assume A2: not X is real-bounded ; ::_thesis: contradiction
percases ( not X is bounded_above or not X is bounded_below ) by A2;
supposeA3: not X is bounded_above ; ::_thesis: contradiction
defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st
( q = $2 & q in X & $1 < q );
A4: for n being Element of NAT ex p being Element of REAL st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p]
n is not UpperBound of X by A3, XXREAL_2:def_10;
then consider t being ext-real number such that
A5: ( t in X & n < t ) by XXREAL_2:def_1;
take t ; ::_thesis: ( t is Element of REAL & S1[n,t] )
thus ( t is Element of REAL & S1[n,t] ) by A5; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A6: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A4);
A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_f_._n_in_X_&_n_<_f_._n_)
let n be Element of NAT ; ::_thesis: ( f . n in X & n < f . n )
ex q being real number st
( q = f . n & q in X & n < q ) by A6;
hence ( f . n in X & n < f . n ) ; ::_thesis: verum
end;
A8: for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
proof
let p be real number ; ::_thesis: ( p in X implies ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) ) )
assume p in X ; ::_thesis: ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider q being real number such that
A9: q = 1 ;
take r = q; ::_thesis: ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider k being Element of NAT such that
A10: p + 1 < k by SEQ_4:3;
take n = k; ::_thesis: ( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
thus 0 < r by A9; ::_thesis: for m being Element of NAT st n < m holds
r < abs ((f . m) - p)
let m be Element of NAT ; ::_thesis: ( n < m implies r < abs ((f . m) - p) )
assume n < m ; ::_thesis: r < abs ((f . m) - p)
then p + 1 < m by A10, XXREAL_0:2;
then p + 1 < f . m by A7, XXREAL_0:2;
then 1 < (f . m) - p by XREAL_1:20;
hence r < abs ((f . m) - p) by A9, ABSVALUE:def_1; ::_thesis: verum
end;
rng f c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X )
assume x in rng f ; ::_thesis: x in X
then consider y being set such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A11, FUNCT_2:def_1;
f . y in X by A7;
hence x in X by A12; ::_thesis: verum
end;
then ex s2 being Real_Sequence st
( s2 is subsequence of f & s2 is convergent & lim s2 in X ) by A1, Def3;
hence contradiction by A8, Th9; ::_thesis: verum
end;
supposeA13: not X is bounded_below ; ::_thesis: contradiction
defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st
( q = $2 & q in X & q < - $1 );
A14: for n being Element of NAT ex p being Element of REAL st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p]
- n is not LowerBound of X by A13, XXREAL_2:def_9;
then consider t being ext-real number such that
A15: ( t in X & t < - n ) by XXREAL_2:def_2;
take t ; ::_thesis: ( t is Element of REAL & S1[n,t] )
thus ( t is Element of REAL & S1[n,t] ) by A15; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A16: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A14);
A17: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_f_._n_in_X_&_f_._n_<_-_n_)
let n be Element of NAT ; ::_thesis: ( f . n in X & f . n < - n )
ex q being real number st
( q = f . n & q in X & q < - n ) by A16;
hence ( f . n in X & f . n < - n ) ; ::_thesis: verum
end;
A18: for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
proof
let p be real number ; ::_thesis: ( p in X implies ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) ) )
assume p in X ; ::_thesis: ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider q being real number such that
A19: q = 1 ;
take r = q; ::_thesis: ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
consider k being Element of NAT such that
A20: abs (p - 1) < k by SEQ_4:3;
take n = k; ::_thesis: ( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((f . m) - p) ) )
thus 0 < r by A19; ::_thesis: for m being Element of NAT st n < m holds
r < abs ((f . m) - p)
let m be Element of NAT ; ::_thesis: ( n < m implies r < abs ((f . m) - p) )
assume n < m ; ::_thesis: r < abs ((f . m) - p)
then A21: - m < - n by XREAL_1:24;
- k < p - 1 by A20, SEQ_2:1;
then - m < p - 1 by A21, XXREAL_0:2;
then f . m < p - 1 by A17, XXREAL_0:2;
then (f . m) + 1 < p by XREAL_1:20;
then 1 < p - (f . m) by XREAL_1:20;
then r < abs (- ((f . m) - p)) by A19, ABSVALUE:def_1;
hence r < abs ((f . m) - p) by COMPLEX1:52; ::_thesis: verum
end;
rng f c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X )
assume x in rng f ; ::_thesis: x in X
then consider y being set such that
A22: y in dom f and
A23: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A22, FUNCT_2:def_1;
f . y in X by A17;
hence x in X by A23; ::_thesis: verum
end;
then ex s2 being Real_Sequence st
( s2 is subsequence of f & s2 is convergent & lim s2 in X ) by A1, Def3;
hence contradiction by A18, Th9; ::_thesis: verum
end;
end;
end;
theorem :: RCOMP_1:11
for X being Subset of REAL st X is real-bounded & X is closed holds
X is compact
proof
let X be Subset of REAL; ::_thesis: ( X is real-bounded & X is closed implies X is compact )
assume that
A1: X is real-bounded and
A2: X is closed ; ::_thesis: X is compact
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_holds_
ex_s2_being_Real_Sequence_st_
(_s2_is_subsequence_of_s1_&_s2_is_convergent_&_lim_s2_in_X_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X implies ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) )
assume A3: rng s1 c= X ; ::_thesis: ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X )
A4: s1 is bounded_below
proof
consider p being real number such that
A5: p is LowerBound of X by A1, XXREAL_2:def_9;
A6: for q being real number st q in X holds
p <= q by A5, XXREAL_2:def_2;
take r = p - 1; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not s1 . b1 <= r
A7: r + 1 = p - (1 - 1) ;
A8: for t being real number st t in rng s1 holds
r < t
proof
let t be real number ; ::_thesis: ( t in rng s1 implies r < t )
assume t in rng s1 ; ::_thesis: r < t
then A9: p <= t by A3, A6;
r < p by A7, XREAL_1:29;
hence r < t by A9, XXREAL_0:2; ::_thesis: verum
end;
for n being Element of NAT holds r < s1 . n
proof
let n be Element of NAT ; ::_thesis: r < s1 . n
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then s1 . n in rng s1 by FUNCT_1:def_3;
hence r < s1 . n by A8; ::_thesis: verum
end;
hence for b1 being Element of NAT holds not s1 . b1 <= r ; ::_thesis: verum
end;
s1 is bounded_above
proof
consider p being real number such that
A10: p is UpperBound of X by A1, XXREAL_2:def_10;
A11: for q being real number st q in X holds
q <= p by A10, XXREAL_2:def_1;
take r = p + 1; :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not r <= s1 . b1
A12: for t being real number st t in rng s1 holds
t < r
proof
let t be real number ; ::_thesis: ( t in rng s1 implies t < r )
assume t in rng s1 ; ::_thesis: t < r
then A13: t <= p by A3, A11;
p < r by XREAL_1:29;
hence t < r by A13, XXREAL_0:2; ::_thesis: verum
end;
for n being Element of NAT holds s1 . n < r
proof
let n be Element of NAT ; ::_thesis: s1 . n < r
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then s1 . n in rng s1 by FUNCT_1:def_3;
hence s1 . n < r by A12; ::_thesis: verum
end;
hence for b1 being Element of NAT holds not r <= s1 . b1 ; ::_thesis: verum
end;
then s1 is bounded by A4, SEQ_2:def_8;
then consider s2 being Real_Sequence such that
A14: s2 is subsequence of s1 and
A15: s2 is convergent by SEQ_4:40;
ex Nseq being increasing sequence of NAT st s2 = s1 * Nseq by A14, VALUED_0:def_17;
then rng s2 c= rng s1 by RELAT_1:26;
then rng s2 c= X by A3, XBOOLE_1:1;
then lim s2 in X by A2, A15, Def4;
hence ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A14, A15; ::_thesis: verum
end;
hence X is compact by Def3; ::_thesis: verum
end;
theorem Th12: :: RCOMP_1:12
for X being Subset of REAL st X <> {} & X is closed & X is bounded_above holds
upper_bound X in X
proof
let X be Subset of REAL; ::_thesis: ( X <> {} & X is closed & X is bounded_above implies upper_bound X in X )
assume that
A1: X <> {} and
A2: X is closed and
A3: X is bounded_above and
A4: not upper_bound X in X ; ::_thesis: contradiction
set s1 = upper_bound X;
defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st
( q = $2 & q in X & (upper_bound X) - q < 1 / ($1 + 1) );
A5: for n being Element of NAT ex p being Element of REAL st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p]
0 < (n + 1) " ;
then 0 < 1 / (n + 1) by XCMPLX_1:215;
then consider t being real number such that
A6: t in X and
A7: (upper_bound X) - (1 / (n + 1)) < t by A1, A3, SEQ_4:def_1;
take t ; ::_thesis: ( t is Element of REAL & S1[n,t] )
upper_bound X < t + (1 / (n + 1)) by A7, XREAL_1:19;
then (upper_bound X) - t < 1 / (n + 1) by XREAL_1:19;
hence ( t is Element of REAL & S1[n,t] ) by A6; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A8: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A5);
A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_f_._n_in_X_&_(upper_bound_X)_-_(f_._n)_<_1_/_(n_+_1)_)
let n be Element of NAT ; ::_thesis: ( f . n in X & (upper_bound X) - (f . n) < 1 / (n + 1) )
ex q being real number st
( q = f . n & q in X & (upper_bound X) - q < 1 / (n + 1) ) by A8;
hence ( f . n in X & (upper_bound X) - (f . n) < 1 / (n + 1) ) ; ::_thesis: verum
end;
A10: rng f c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X )
assume x in rng f ; ::_thesis: x in X
then consider y being set such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A11, FUNCT_2:def_1;
f . y in X by A9;
hence x in X by A12; ::_thesis: verum
end;
A13: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((f_._m)_-_(upper_bound_X))_<_s
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((f . m) - (upper_bound X)) < s )
assume A14: 0 < s ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((f . m) - (upper_bound X)) < s
consider n being Element of NAT such that
A15: s " < n by SEQ_4:3;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
abs ((f . m) - (upper_bound X)) < s
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((f . m) - (upper_bound X)) < s )
assume k <= m ; ::_thesis: abs ((f . m) - (upper_bound X)) < s
then k + 1 <= m + 1 by XREAL_1:6;
then A16: 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
f . m in X by A9;
then f . m <= upper_bound X by A3, SEQ_4:def_1;
then A17: 0 <= (upper_bound X) - (f . m) by XREAL_1:48;
(s ") + 0 < n + 1 by A15, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A14, XREAL_1:76;
then 1 / (n + 1) < s by XCMPLX_1:216;
then 1 / (m + 1) < s by A16, XXREAL_0:2;
then (upper_bound X) - (f . m) < s by A9, XXREAL_0:2;
then abs (- ((f . m) - (upper_bound X))) < s by A17, ABSVALUE:def_1;
hence abs ((f . m) - (upper_bound X)) < s by COMPLEX1:52; ::_thesis: verum
end;
then A18: f is convergent by SEQ_2:def_6;
then lim f = upper_bound X by A13, SEQ_2:def_7;
hence contradiction by A2, A4, A18, A10, Def4; ::_thesis: verum
end;
theorem Th13: :: RCOMP_1:13
for X being Subset of REAL st X <> {} & X is closed & X is bounded_below holds
lower_bound X in X
proof
let X be Subset of REAL; ::_thesis: ( X <> {} & X is closed & X is bounded_below implies lower_bound X in X )
assume that
A1: X <> {} and
A2: X is closed and
A3: X is bounded_below and
A4: not lower_bound X in X ; ::_thesis: contradiction
set i1 = lower_bound X;
defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st
( q = $2 & q in X & q - (lower_bound X) < 1 / ($1 + 1) );
A5: for n being Element of NAT ex p being Element of REAL st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p]
0 < (n + 1) " ;
then 0 < 1 / (n + 1) by XCMPLX_1:215;
then consider t being real number such that
A6: t in X and
A7: t < (lower_bound X) + (1 / (n + 1)) by A1, A3, SEQ_4:def_2;
take t ; ::_thesis: ( t is Element of REAL & S1[n,t] )
t - (lower_bound X) < 1 / (n + 1) by A7, XREAL_1:19;
hence ( t is Element of REAL & S1[n,t] ) by A6; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A8: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A5);
A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_f_._n_in_X_&_(f_._n)_-_(lower_bound_X)_<_1_/_(n_+_1)_)
let n be Element of NAT ; ::_thesis: ( f . n in X & (f . n) - (lower_bound X) < 1 / (n + 1) )
ex q being real number st
( q = f . n & q in X & q - (lower_bound X) < 1 / (n + 1) ) by A8;
hence ( f . n in X & (f . n) - (lower_bound X) < 1 / (n + 1) ) ; ::_thesis: verum
end;
A10: rng f c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X )
assume x in rng f ; ::_thesis: x in X
then consider y being set such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A11, FUNCT_2:def_1;
f . y in X by A9;
hence x in X by A12; ::_thesis: verum
end;
A13: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((f_._m)_-_(lower_bound_X))_<_s
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((f . m) - (lower_bound X)) < s )
assume A14: 0 < s ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((f . m) - (lower_bound X)) < s
consider n being Element of NAT such that
A15: s " < n by SEQ_4:3;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
abs ((f . m) - (lower_bound X)) < s
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((f . m) - (lower_bound X)) < s )
assume k <= m ; ::_thesis: abs ((f . m) - (lower_bound X)) < s
then k + 1 <= m + 1 by XREAL_1:6;
then A16: 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
f . m in X by A9;
then lower_bound X <= f . m by A3, SEQ_4:def_2;
then A17: 0 <= (f . m) - (lower_bound X) by XREAL_1:48;
(s ") + 0 < n + 1 by A15, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A14, XREAL_1:76;
then 1 / (n + 1) < s by XCMPLX_1:216;
then 1 / (m + 1) < s by A16, XXREAL_0:2;
then (f . m) - (lower_bound X) < s by A9, XXREAL_0:2;
hence abs ((f . m) - (lower_bound X)) < s by A17, ABSVALUE:def_1; ::_thesis: verum
end;
then A18: f is convergent by SEQ_2:def_6;
then lim f = lower_bound X by A13, SEQ_2:def_7;
hence contradiction by A2, A4, A18, A10, Def4; ::_thesis: verum
end;
theorem :: RCOMP_1:14
for X being Subset of REAL st X <> {} & X is compact holds
( upper_bound X in X & lower_bound X in X )
proof
let X be Subset of REAL; ::_thesis: ( X <> {} & X is compact implies ( upper_bound X in X & lower_bound X in X ) )
assume that
A1: X <> {} and
A2: X is compact ; ::_thesis: ( upper_bound X in X & lower_bound X in X )
( X is real-bounded & X is closed ) by A2, Th10;
hence ( upper_bound X in X & lower_bound X in X ) by A1, Th12, Th13; ::_thesis: verum
end;
theorem :: RCOMP_1:15
for X being Subset of REAL st X is compact & ( for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ) holds
ex p, g being real number st X = [.p,g.]
proof
let X be Subset of REAL; ::_thesis: ( X is compact & ( for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ) implies ex p, g being real number st X = [.p,g.] )
assume that
A1: X is compact and
A2: for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ; ::_thesis: ex p, g being real number st X = [.p,g.]
percases ( X = {} or X <> {} ) ;
supposeA3: X = {} ; ::_thesis: ex p, g being real number st X = [.p,g.]
take 1 ; ::_thesis: ex g being real number st X = [.1,g.]
take 0 ; ::_thesis: X = [.1,0.]
thus X = [.1,0.] by A3, XXREAL_1:29; ::_thesis: verum
end;
supposeA4: X <> {} ; ::_thesis: ex p, g being real number st X = [.p,g.]
take p = lower_bound X; ::_thesis: ex g being real number st X = [.p,g.]
take g = upper_bound X; ::_thesis: X = [.p,g.]
A5: ( X is real-bounded & X is closed ) by A1, Th10;
now__::_thesis:_for_r_being_Real_st_r_in_X_holds_
r_in_[.p,g.]
let r be Real; ::_thesis: ( r in X implies r in [.p,g.] )
assume r in X ; ::_thesis: r in [.p,g.]
then ( r <= g & p <= r ) by A5, SEQ_4:def_1, SEQ_4:def_2;
hence r in [.p,g.] ; ::_thesis: verum
end;
then A6: X c= [.p,g.] by SUBSET_1:2;
( upper_bound X in X & lower_bound X in X ) by A4, A5, Th12, Th13;
then [.p,g.] c= X by A2;
hence X = [.p,g.] by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
registration
clusterV50() V51() V52() open for Element of K19(REAL);
existence
ex b1 being Subset of REAL st b1 is open
proof
take ].0,1.[ ; ::_thesis: ].0,1.[ is open
thus ].0,1.[ is open ; ::_thesis: verum
end;
end;
definition
let r be real number ;
mode Neighbourhood of r -> Subset of REAL means :Def6: :: RCOMP_1:def 6
ex g being real number st
( 0 < g & it = ].(r - g),(r + g).[ );
existence
ex b1 being Subset of REAL ex g being real number st
( 0 < g & b1 = ].(r - g),(r + g).[ )
proof
take ].(r - 1),(r + 1).[ ; ::_thesis: ex g being real number st
( 0 < g & ].(r - 1),(r + 1).[ = ].(r - g),(r + g).[ )
thus ex g being real number st
( 0 < g & ].(r - 1),(r + 1).[ = ].(r - g),(r + g).[ ) ; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Neighbourhood RCOMP_1:def_6_:_
for r being real number
for b2 being Subset of REAL holds
( b2 is Neighbourhood of r iff ex g being real number st
( 0 < g & b2 = ].(r - g),(r + g).[ ) );
registration
let r be real number ;
cluster -> open for Neighbourhood of r;
coherence
for b1 being Neighbourhood of r holds b1 is open
proof
let A be Neighbourhood of r; ::_thesis: A is open
ex g being real number st
( 0 < g & A = ].(r - g),(r + g).[ ) by Def6;
hence A is open ; ::_thesis: verum
end;
end;
theorem :: RCOMP_1:16
for r being real number
for N being Neighbourhood of r holds r in N
proof
let r be real number ; ::_thesis: for N being Neighbourhood of r holds r in N
let N be Neighbourhood of r; ::_thesis: r in N
( ex g being real number st
( 0 < g & N = ].(r - g),(r + g).[ ) & abs (r - r) = 0 ) by Def6, ABSVALUE:2;
hence r in N by Th1; ::_thesis: verum
end;
theorem :: RCOMP_1:17
for r being real number
for N1, N2 being Neighbourhood of r ex N being Neighbourhood of r st
( N c= N1 & N c= N2 )
proof
let r be real number ; ::_thesis: for N1, N2 being Neighbourhood of r ex N being Neighbourhood of r st
( N c= N1 & N c= N2 )
let N1, N2 be Neighbourhood of r; ::_thesis: ex N being Neighbourhood of r st
( N c= N1 & N c= N2 )
consider g1 being real number such that
A1: 0 < g1 and
A2: ].(r - g1),(r + g1).[ = N1 by Def6;
consider g2 being real number such that
A3: 0 < g2 and
A4: ].(r - g2),(r + g2).[ = N2 by Def6;
set g = min (g1,g2);
0 < min (g1,g2) by A1, A3, XXREAL_0:15;
then reconsider N = ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ as Neighbourhood of r by Def6;
take N ; ::_thesis: ( N c= N1 & N c= N2 )
A5: min (g1,g2) <= g1 by XXREAL_0:17;
then A6: r + (min (g1,g2)) <= r + g1 by XREAL_1:7;
- g1 <= - (min (g1,g2)) by A5, XREAL_1:24;
then A7: r + (- g1) <= r + (- (min (g1,g2))) by XREAL_1:7;
A8: min (g1,g2) <= g2 by XXREAL_0:17;
then - g2 <= - (min (g1,g2)) by XREAL_1:24;
then A9: r + (- g2) <= r + (- (min (g1,g2))) by XREAL_1:7;
A10: r + (min (g1,g2)) <= r + g2 by A8, XREAL_1:7;
now__::_thesis:_(_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_c=_N1_&_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_c=_N2_)
percases ( g1 <= g2 or g2 <= g1 ) ;
supposeA11: g1 <= g2 ; ::_thesis: ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 )
A12: now__::_thesis:_for_y_being_set_st_y_in_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_holds_
y_in_].(r_-_g2),(r_+_g2).[
let y be set ; ::_thesis: ( y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ implies y in ].(r - g2),(r + g2).[ )
assume A13: y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ ; ::_thesis: y in ].(r - g2),(r + g2).[
then reconsider x1 = y as Real ;
ex p2 being Real st
( y = p2 & r - (min (g1,g2)) < p2 & p2 < r + (min (g1,g2)) ) by A13;
then ( x1 < r + g2 & r - g2 < x1 ) by A10, A9, XXREAL_0:2;
hence y in ].(r - g2),(r + g2).[ ; ::_thesis: verum
end;
g1 = min (g1,g2) by A11, XXREAL_0:def_9;
hence ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) by A2, A4, A12, TARSKI:def_3; ::_thesis: verum
end;
supposeA14: g2 <= g1 ; ::_thesis: ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 )
A15: now__::_thesis:_for_y_being_set_st_y_in_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_holds_
y_in_].(r_-_g1),(r_+_g1).[
let y be set ; ::_thesis: ( y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ implies y in ].(r - g1),(r + g1).[ )
assume A16: y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ ; ::_thesis: y in ].(r - g1),(r + g1).[
then reconsider x1 = y as Real ;
ex p2 being Real st
( y = p2 & r - (min (g1,g2)) < p2 & p2 < r + (min (g1,g2)) ) by A16;
then ( x1 < r + g1 & r - g1 < x1 ) by A6, A7, XXREAL_0:2;
hence y in ].(r - g1),(r + g1).[ ; ::_thesis: verum
end;
g2 = min (g1,g2) by A14, XXREAL_0:def_9;
hence ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) by A2, A4, A15, TARSKI:def_3; ::_thesis: verum
end;
end;
end;
hence ( N c= N1 & N c= N2 ) ; ::_thesis: verum
end;
theorem Th18: :: RCOMP_1:18
for X being open Subset of REAL
for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X
proof
let X be open Subset of REAL; ::_thesis: for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X
let r be real number ; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X )
assume that
A1: r in X and
A2: for N being Neighbourhood of r holds not N c= X ; ::_thesis: contradiction
defpred S1[ Element of NAT , real number ] means ( $2 in ].(r - (1 / ($1 + 1))),(r + (1 / ($1 + 1))).[ & $2 in X ` );
A3: now__::_thesis:_for_N_being_Neighbourhood_of_r_ex_s_being_Real_st_
(_s_in_N_&_s_in_X_`_)
let N be Neighbourhood of r; ::_thesis: ex s being Real st
( s in N & s in X ` )
consider g being real number such that
0 < g and
A4: N = ].(r - g),(r + g).[ by Def6;
not N c= X by A2;
then consider x being set such that
A5: x in N and
A6: not x in X by TARSKI:def_3;
consider s being Real such that
A7: x = s and
r - g < s and
s < r + g by A5, A4;
take s = s; ::_thesis: ( s in N & s in X ` )
thus s in N by A5, A7; ::_thesis: s in X `
thus s in X ` by A6, A7, XBOOLE_0:def_5; ::_thesis: verum
end;
A8: for n being Element of NAT ex s being Real st S1[n,s]
proof
let n be Element of NAT ; ::_thesis: ex s being Real st S1[n,s]
0 < 1 * ((n + 1) ") ;
then 0 < 1 / (n + 1) by XCMPLX_0:def_9;
then reconsider N = ].(r - (1 / (n + 1))),(r + (1 / (n + 1))).[ as Neighbourhood of r by Def6;
ex s being Real st
( s in N & s in X ` ) by A3;
hence ex s being Real st S1[n,s] ; ::_thesis: verum
end;
consider s3 being Real_Sequence such that
A9: for n being Element of NAT holds S1[n,s3 . n] from FUNCT_2:sch_3(A8);
deffunc H1( Element of NAT ) -> Element of REAL = r + (1 / ($1 + 1));
deffunc H2( Element of NAT ) -> Element of REAL = r - (1 / ($1 + 1));
consider s1 being Real_Sequence such that
A10: for n being Element of NAT holds s1 . n = H2(n) from SEQ_1:sch_1();
consider s2 being Real_Sequence such that
A11: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1();
A12: for n being Element of NAT holds
( s1 . n <= s3 . n & s3 . n <= s2 . n )
proof
let n be Element of NAT ; ::_thesis: ( s1 . n <= s3 . n & s3 . n <= s2 . n )
s3 . n in ].(r - (1 / (n + 1))),(r + (1 / (n + 1))).[ by A9;
then A13: ex s being Real st
( s = s3 . n & r - (1 / (n + 1)) < s & s < r + (1 / (n + 1)) ) ;
hence s1 . n <= s3 . n by A10; ::_thesis: s3 . n <= s2 . n
thus s3 . n <= s2 . n by A11, A13; ::_thesis: verum
end;
A14: rng s3 c= X `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s3 or x in X ` )
assume x in rng s3 ; ::_thesis: x in X `
then consider y being set such that
A15: y in dom s3 and
A16: s3 . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A15, FUNCT_2:def_1;
s3 . y in X ` by A9;
hence x in X ` by A16; ::_thesis: verum
end;
A17: X ` is closed by Def5;
A18: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((s2_._m)_-_r)_<_s
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s2 . m) - r) < s )
assume A19: 0 < s ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s2 . m) - r) < s
consider n being Element of NAT such that
A20: s " < n by SEQ_4:3;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs ((s2 . m) - r) < s
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((s2 . m) - r) < s )
assume n <= m ; ::_thesis: abs ((s2 . m) - r) < s
then n + 1 <= m + 1 by XREAL_1:6;
then A21: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
(s ") + 0 < n + 1 by A20, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A19, XREAL_1:76;
then A22: 1 / (n + 1) < s by XCMPLX_1:216;
abs ((s2 . m) - r) = abs ((r + (1 / (m + 1))) - r) by A11
.= 1 / (m + 1) by ABSVALUE:def_1 ;
hence abs ((s2 . m) - r) < s by A22, A21, XXREAL_0:2; ::_thesis: verum
end;
then A23: s2 is convergent by SEQ_2:def_6;
then A24: lim s2 = r by A18, SEQ_2:def_7;
A25: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((s1_._m)_-_r)_<_s
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s1 . m) - r) < s )
assume A26: 0 < s ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s1 . m) - r) < s
consider n being Element of NAT such that
A27: s " < n by SEQ_4:3;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs ((s1 . m) - r) < s
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((s1 . m) - r) < s )
assume n <= m ; ::_thesis: abs ((s1 . m) - r) < s
then n + 1 <= m + 1 by XREAL_1:6;
then A28: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
(s ") + 0 < n + 1 by A27, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A26, XREAL_1:76;
then A29: 1 / (n + 1) < s by XCMPLX_1:216;
abs ((s1 . m) - r) = abs ((r - (1 / (m + 1))) - r) by A10
.= abs (- (1 / (m + 1)))
.= abs (1 / (m + 1)) by COMPLEX1:52
.= 1 / (m + 1) by ABSVALUE:def_1 ;
hence abs ((s1 . m) - r) < s by A29, A28, XXREAL_0:2; ::_thesis: verum
end;
then A30: s1 is convergent by SEQ_2:def_6;
then lim s1 = r by A25, SEQ_2:def_7;
then ( s3 is convergent & lim s3 = r ) by A30, A23, A24, A12, SEQ_2:19, SEQ_2:20;
then r in X ` by A14, A17, Def4;
hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: RCOMP_1:19
for X being open Subset of REAL
for r being real number st r in X holds
ex g being real number st
( 0 < g & ].(r - g),(r + g).[ c= X )
proof
let X be open Subset of REAL; ::_thesis: for r being real number st r in X holds
ex g being real number st
( 0 < g & ].(r - g),(r + g).[ c= X )
let r be real number ; ::_thesis: ( r in X implies ex g being real number st
( 0 < g & ].(r - g),(r + g).[ c= X ) )
assume r in X ; ::_thesis: ex g being real number st
( 0 < g & ].(r - g),(r + g).[ c= X )
then consider N being Neighbourhood of r such that
A1: N c= X by Th18;
consider g being real number such that
A2: ( 0 < g & N = ].(r - g),(r + g).[ ) by Def6;
take g ; ::_thesis: ( 0 < g & ].(r - g),(r + g).[ c= X )
thus ( 0 < g & ].(r - g),(r + g).[ c= X ) by A1, A2; ::_thesis: verum
end;
theorem :: RCOMP_1:20
for X being Subset of REAL st ( for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X ) holds
X is open
proof
let X be Subset of REAL; ::_thesis: ( ( for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X ) implies X is open )
assume that
A1: for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X and
A2: not X is open ; ::_thesis: contradiction
not X ` is closed by A2, Def5;
then consider s1 being Real_Sequence such that
A3: rng s1 c= X ` and
A4: s1 is convergent and
A5: not lim s1 in X ` by Def4;
consider N being Neighbourhood of lim s1 such that
A6: N c= X by A1, A5, SUBSET_1:29;
consider g being real number such that
A7: 0 < g and
A8: ].((lim s1) - g),((lim s1) + g).[ = N by Def6;
consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < g by A4, A7, SEQ_2:def_7;
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then A10: s1 . n in rng s1 by FUNCT_1:def_3;
A11: abs ((s1 . n) - (lim s1)) < g by A9;
then (s1 . n) - (lim s1) < g by SEQ_2:1;
then A12: s1 . n < (lim s1) + g by XREAL_1:19;
- g < (s1 . n) - (lim s1) by A11, SEQ_2:1;
then (lim s1) + (- g) < (lim s1) + ((s1 . n) - (lim s1)) by XREAL_1:6;
then s1 . n in { s where s is Real : ( (lim s1) - g < s & s < (lim s1) + g ) } by A12;
hence contradiction by A3, A6, A8, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th21: :: RCOMP_1:21
for X being Subset of REAL st X is open & X is bounded_above holds
not upper_bound X in X
proof
let X be Subset of REAL; ::_thesis: ( X is open & X is bounded_above implies not upper_bound X in X )
assume that
A1: X is open and
A2: X is bounded_above ; ::_thesis: not upper_bound X in X
assume upper_bound X in X ; ::_thesis: contradiction
then consider N being Neighbourhood of upper_bound X such that
A3: N c= X by A1, Th18;
consider t being real number such that
A4: t > 0 and
A5: N = ].((upper_bound X) - t),((upper_bound X) + t).[ by Def6;
A6: (upper_bound X) + (t / 2) > upper_bound X by A4, XREAL_1:29, XREAL_1:215;
A7: ((upper_bound X) + (t / 2)) + (t / 2) > (upper_bound X) + (t / 2) by A4, XREAL_1:29, XREAL_1:215;
(upper_bound X) - t < upper_bound X by A4, XREAL_1:44;
then (upper_bound X) - t < (upper_bound X) + (t / 2) by A6, XXREAL_0:2;
then (upper_bound X) + (t / 2) in { s where s is Real : ( (upper_bound X) - t < s & s < (upper_bound X) + t ) } by A7;
hence contradiction by A2, A3, A5, A6, SEQ_4:def_1; ::_thesis: verum
end;
theorem Th22: :: RCOMP_1:22
for X being Subset of REAL st X is open & X is bounded_below holds
not lower_bound X in X
proof
let X be Subset of REAL; ::_thesis: ( X is open & X is bounded_below implies not lower_bound X in X )
assume that
A1: X is open and
A2: X is bounded_below ; ::_thesis: not lower_bound X in X
assume lower_bound X in X ; ::_thesis: contradiction
then consider N being Neighbourhood of lower_bound X such that
A3: N c= X by A1, Th18;
consider t being real number such that
A4: t > 0 and
A5: N = ].((lower_bound X) - t),((lower_bound X) + t).[ by Def6;
A6: (lower_bound X) - (t / 2) < lower_bound X by A4, XREAL_1:44, XREAL_1:215;
A7: ((lower_bound X) - (t / 2)) - (t / 2) < (lower_bound X) - (t / 2) by A4, XREAL_1:44, XREAL_1:215;
lower_bound X < (lower_bound X) + t by A4, XREAL_1:29;
then (lower_bound X) - (t / 2) < (lower_bound X) + t by A6, XXREAL_0:2;
then (lower_bound X) - (t / 2) in { s where s is Real : ( (lower_bound X) - t < s & s < (lower_bound X) + t ) } by A7;
hence contradiction by A2, A3, A5, A6, SEQ_4:def_2; ::_thesis: verum
end;
theorem :: RCOMP_1:23
for X being Subset of REAL st X is open & X is real-bounded & ( for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ) holds
ex p, g being real number st X = ].p,g.[
proof
let X be Subset of REAL; ::_thesis: ( X is open & X is real-bounded & ( for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ) implies ex p, g being real number st X = ].p,g.[ )
assume that
A1: X is open and
A2: X is real-bounded and
A3: for g1, g2 being real number st g1 in X & g2 in X holds
[.g1,g2.] c= X ; ::_thesis: ex p, g being real number st X = ].p,g.[
percases ( X = {} or X <> {} ) ;
supposeA4: X = {} ; ::_thesis: ex p, g being real number st X = ].p,g.[
take 1 ; ::_thesis: ex g being real number st X = ].1,g.[
take 0 ; ::_thesis: X = ].1,0.[
thus X = ].1,0.[ by A4, XXREAL_1:28; ::_thesis: verum
end;
supposeA5: X <> {} ; ::_thesis: ex p, g being real number st X = ].p,g.[
take p = lower_bound X; ::_thesis: ex g being real number st X = ].p,g.[
take g = upper_bound X; ::_thesis: X = ].p,g.[
now__::_thesis:_for_r_being_Real_holds_
(_(_r_in_X_implies_r_in_].p,g.[_)_&_(_r_in_].p,g.[_implies_r_in_X_)_)
let r be Real; ::_thesis: ( ( r in X implies r in ].p,g.[ ) & ( r in ].p,g.[ implies r in X ) )
thus ( r in X implies r in ].p,g.[ ) ::_thesis: ( r in ].p,g.[ implies r in X )
proof
assume A6: r in X ; ::_thesis: r in ].p,g.[
then ( p <> r & p <= r ) by A1, A2, Th22, SEQ_4:def_2;
then A7: p < r by XXREAL_0:1;
( g <> r & r <= g ) by A1, A2, A6, Th21, SEQ_4:def_1;
then r < g by XXREAL_0:1;
hence r in ].p,g.[ by A7; ::_thesis: verum
end;
assume r in ].p,g.[ ; ::_thesis: r in X
then A8: ex s being Real st
( s = r & p < s & s < g ) ;
then g - r > 0 by XREAL_1:50;
then consider g2 being real number such that
A9: ( g2 in X & g - (g - r) < g2 ) by A2, A5, SEQ_4:def_1;
r - p > 0 by A8, XREAL_1:50;
then consider g1 being real number such that
A10: ( g1 in X & g1 < p + (r - p) ) by A2, A5, SEQ_4:def_2;
reconsider g1 = g1, g2 = g2 as Real by XREAL_0:def_1;
( r in { s where s is Real : ( g1 <= s & s <= g2 ) } & [.g1,g2.] c= X ) by A3, A9, A10;
hence r in X ; ::_thesis: verum
end;
hence X = ].p,g.[ by SUBSET_1:3; ::_thesis: verum
end;
end;
end;
definition
let g be real number ;
let s be ext-real number ;
:: original: [.
redefine func[.g,s.[ -> Subset of REAL equals :: RCOMP_1:def 7
{ r where r is Real : ( g <= r & r < s ) } ;
coherence
[.g,s.[ is Subset of REAL
proof
now__::_thesis:_for_e_being_set_st_e_in_[.g,s.[_holds_
e_in_REAL
let e be set ; ::_thesis: ( e in [.g,s.[ implies e in REAL )
assume e in [.g,s.[ ; ::_thesis: e in REAL
then A1: ex r being Element of ExtREAL st
( e = r & g <= r & r < s ) ;
g in REAL by XREAL_0:def_1;
hence e in REAL by A1, XXREAL_0:46; ::_thesis: verum
end;
hence [.g,s.[ is Subset of REAL by TARSKI:def_3; ::_thesis: verum
end;
compatibility
for b1 being Subset of REAL holds
( b1 = [.g,s.[ iff b1 = { r where r is Real : ( g <= r & r < s ) } )
proof
set Y = { r where r is Real : ( g <= r & r < s ) } ;
let X be Subset of REAL; ::_thesis: ( X = [.g,s.[ iff X = { r where r is Real : ( g <= r & r < s ) } )
A2: [.g,s.[ c= { r where r is Real : ( g <= r & r < s ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in [.g,s.[ or e in { r where r is Real : ( g <= r & r < s ) } )
assume e in [.g,s.[ ; ::_thesis: e in { r where r is Real : ( g <= r & r < s ) }
then consider r being Element of ExtREAL such that
A3: e = r and
A4: ( g <= r & r < s ) ;
g in REAL by XREAL_0:def_1;
then r in REAL by A4, XXREAL_0:46;
hence e in { r where r is Real : ( g <= r & r < s ) } by A3, A4; ::_thesis: verum
end;
{ r where r is Real : ( g <= r & r < s ) } c= [.g,s.[
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { r where r is Real : ( g <= r & r < s ) } or e in [.g,s.[ )
assume e in { r where r is Real : ( g <= r & r < s ) } ; ::_thesis: e in [.g,s.[
then consider r being Element of REAL such that
A5: ( e = r & g <= r & r < s ) ;
r in REAL ;
hence e in [.g,s.[ by A5, NUMBERS:31; ::_thesis: verum
end;
hence ( X = [.g,s.[ iff X = { r where r is Real : ( g <= r & r < s ) } ) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines [. RCOMP_1:def_7_:_
for g being real number
for s being ext-real number holds [.g,s.[ = { r where r is Real : ( g <= r & r < s ) } ;
definition
let g be ext-real number ;
let s be real number ;
:: original: ].
redefine func].g,s.] -> Subset of REAL equals :: RCOMP_1:def 8
{ r where r is Real : ( g < r & r <= s ) } ;
coherence
].g,s.] is Subset of REAL
proof
now__::_thesis:_for_e_being_set_st_e_in_].g,s.]_holds_
e_in_REAL
let e be set ; ::_thesis: ( e in ].g,s.] implies e in REAL )
assume e in ].g,s.] ; ::_thesis: e in REAL
then A1: ex r being Element of ExtREAL st
( e = r & g < r & r <= s ) ;
s in REAL by XREAL_0:def_1;
hence e in REAL by A1, XXREAL_0:47; ::_thesis: verum
end;
hence ].g,s.] is Subset of REAL by TARSKI:def_3; ::_thesis: verum
end;
compatibility
for b1 being Subset of REAL holds
( b1 = ].g,s.] iff b1 = { r where r is Real : ( g < r & r <= s ) } )
proof
set Y = { r where r is Real : ( g < r & r <= s ) } ;
let X be Subset of REAL; ::_thesis: ( X = ].g,s.] iff X = { r where r is Real : ( g < r & r <= s ) } )
A2: ].g,s.] c= { r where r is Real : ( g < r & r <= s ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ].g,s.] or e in { r where r is Real : ( g < r & r <= s ) } )
assume e in ].g,s.] ; ::_thesis: e in { r where r is Real : ( g < r & r <= s ) }
then consider r being Element of ExtREAL such that
A3: e = r and
A4: ( g < r & r <= s ) ;
s in REAL by XREAL_0:def_1;
then r in REAL by A4, XXREAL_0:47;
hence e in { r where r is Real : ( g < r & r <= s ) } by A3, A4; ::_thesis: verum
end;
{ r where r is Real : ( g < r & r <= s ) } c= ].g,s.]
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { r where r is Real : ( g < r & r <= s ) } or e in ].g,s.] )
assume e in { r where r is Real : ( g < r & r <= s ) } ; ::_thesis: e in ].g,s.]
then consider r being Element of REAL such that
A5: ( e = r & g < r & r <= s ) ;
r in REAL ;
hence e in ].g,s.] by A5, NUMBERS:31; ::_thesis: verum
end;
hence ( X = ].g,s.] iff X = { r where r is Real : ( g < r & r <= s ) } ) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines ]. RCOMP_1:def_8_:_
for g being ext-real number
for s being real number holds ].g,s.] = { r where r is Real : ( g < r & r <= s ) } ;