:: Topological Properties of Subsets in Real Numbers
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SEQ_1, ORDINAL2, NAT_1, XXREAL_1, REAL_1,
XXREAL_0, TARSKI, ARYTM_3, ARYTM_1, COMPLEX1, RELAT_1, VALUED_0, SEQ_2,
XXREAL_2, FUNCT_1, CARD_1, XBOOLE_0, SEQ_4, RCOMP_1, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, SEQ_1,
SEQ_2, COMSEQ_2, VALUED_0, SEQ_4, XXREAL_0, XXREAL_1, XXREAL_2, RECDEF_1;
constructors FUNCOP_1, REAL_1, NAT_1, XXREAL_1, COMPLEX1, PARTFUN1, SEQ_2,
SEQM_3, SEQ_4, RECDEF_1, XXREAL_2, MEMBERED, RELSET_1, RVSUM_1, BINOP_2,
COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0,
XXREAL_2, FUNCT_2, SEQ_1, SEQ_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, SEQ_2;
equalities XBOOLE_0, SUBSET_1, XXREAL_1;
expansions TARSKI, SEQ_2, XBOOLE_0;
theorems TARSKI, SUBSET_1, NAT_1, FUNCT_1, FUNCT_2, SEQ_2, SEQM_3, SEQ_4,
ABSVALUE, RELAT_1, XREAL_0, XBOOLE_0, XCMPLX_0, XCMPLX_1, XREAL_1,
COMPLEX1, XXREAL_0, NUMBERS, XXREAL_1, VALUED_0, XXREAL_2, ORDINAL1,
SEQ_1;
schemes SUBSET_1, FUNCT_2, SEQ_1;
begin
reserve n,n1,m,k for Nat;
reserve x,y for set;
reserve s,g,g1,g2,r,p,p2,q,t for Real;
reserve s1,s2,s3 for Real_Sequence;
reserve Nseq for increasing sequence of NAT;
reserve X for Subset of REAL;
definition
let g,s be Real;
redefine func [. g,s .] -> Subset of REAL equals :: redefines [. (XXREAL_1, definition)
{r: g<=r & r<=s };
coherence
proof
now
let x be object;
assume x in [. g,s .];
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;
end;
hence thesis by TARSKI:def 3;
end;
compatibility
proof
set Y = {r: g<=r & r<=s };
let X be Subset of REAL;
A2: [. g,s .] c= Y
proof
let x be object;
assume x in [. g,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 thesis by A3,A4;
end;
Y c= [. g,s .]
proof
let x be object;
assume x in Y;
then consider r such that
A5: x = r & g <= r & r<=s;
r in REAL by XREAL_0:def 1;
hence thesis by A5,NUMBERS:31;
end;
hence thesis by A2;
end;
end;
definition
let g,s be ExtReal;
redefine func ]. g,s .[ -> Subset of REAL equals :: redefines ]. (XXREAL_1, definition)
{r : g<r & r<s };
coherence
proof
now
let x be object;
assume x in ]. g,s .[;
then ex r being Element of ExtREAL st x = r & g < r & r<s;
hence x in REAL by XXREAL_0:48;
end;
hence thesis by TARSKI:def 3;
end;
compatibility
proof
set Y = {r: g<r & r<s };
let X be Subset of REAL;
A1: Y c= ]. g,s .[
proof
let x be object;
assume x in Y;
then consider r such that
A2: x = r & g < r & r<s;
r in REAL by XREAL_0:def 1;
hence thesis by A2,NUMBERS:31;
end;
]. g,s .[ c= Y
proof
let x be object;
assume x in ]. g,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 thesis by A3,A4;
end;
hence thesis by A1;
end;
end;
theorem Th1:
r in ].p-g,p+g.[ iff |.r-p.|<g
proof
thus r in ].p-g,p+g.[ implies |.r-p.|<g
proof
assume r in ].p-g,p+g.[;
then
A1: ex s 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 thesis by A2,SEQ_2:1;
end;
assume
A3: |.r-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_1:20;
hence thesis by A4;
end;
theorem
r in [.p,g.] iff |.p+g-2*r.|<=g-p
proof
thus r in [.p,g.] implies |.p+g-2*r.|<=g-p
proof
assume r in [.p,g.];
then
A1: ex s 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 thesis by A2,ABSVALUE:5;
end;
assume
A3: |.p+g-2*r.|<=g-p;
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;
end;
theorem
r in ].p,g.[ iff |.p+g-2*r.|<g-p
proof
thus r in ].p,g.[ implies |.p+g-2*r.|<g-p
proof
assume r in ].p,g.[;
then
A1: ex s 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 thesis by A2,SEQ_2:1;
end;
assume
A3: |.p+g-2*r.|<g-p;
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 thesis by A4;
end;
definition
let X;
attr X is compact means
for s1 st rng s1 c= X ex s2 st s2 is
subsequence of s1 & s2 is convergent & lim s2 in X;
end;
definition
let X;
attr X is closed means
for s1 st rng s1 c= X & s1 is convergent holds lim s1 in X;
end;
definition
let X;
attr X is open means
:Def5:
X` is closed;
end;
theorem Th4:
for s1 st rng s1 c= [.s,g.] holds s1 is bounded
proof
let s1 such that
A1: rng s1 c= [.s,g.];
thus s1 is bounded_above
proof
take r = g + 1;
A2: for t st t in rng s1 holds t < r
proof
let t;
assume t in rng s1;
then t in [.s,g.] by A1;
then
A3: ex p st t = p & s <= p & p<=g;
g < r by XREAL_1:29;
hence thesis by A3,XXREAL_0:2;
end;
let n;
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:def 3;
hence thesis by A2;
end;
take r = s - 1;
A4: r + 1 = s - (1-1);
A5: for t st t in rng s1 holds r < t
proof
let t;
assume t in rng s1;
then t in [.s,g.] by A1;
then
A6: ex p st t = p & s <= p & p<=g;
r < s by A4,XREAL_1:29;
hence thesis by A6,XXREAL_0:2;
end;
let n;
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:def 3;
hence thesis by A5;
end;
theorem Th5:
[.s,g.] is closed
proof
for s1 st rng s1 c= [.s,g.] & s1 is convergent holds lim s1 in [.s,g.]
proof
let s1;
assume that
A1: rng s1 c= [.s,g.] and
A2: s1 is convergent;
A3: s <= lim s1
proof
set s2 = seq_const s;
A4: now
let n;
n in NAT by ORDINAL1:def 12;
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 st s1.n = p & s <= p & p<=g;
hence s2.n<=s1.n by SEQ_1:57;
end;
s2.0 = s by SEQ_1:57;
then lim s2 = s by SEQ_4:25;
hence thesis by A2,A4,SEQ_2:18;
end;
lim s1 <= g
proof
set s2 = seq_const g;
A5: now
let n;
n in NAT by ORDINAL1:def 12;
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 st s1.n = p & s <= p & p<=g;
hence s1.n<=s2.n by SEQ_1:57;
end;
s2.0 = g by SEQ_1:57;
then lim s2 = g by SEQ_4:25;
hence thesis by A2,A5,SEQ_2:18;
end;
hence thesis by A3;
end;
hence thesis;
end;
theorem
[.s,g.] is compact
proof
for s1 st rng s1 c= [.s,g.] ex s2 st s2 is subsequence of s1 & s2 is
convergent & lim s2 in [.s,g.]
proof
let s1;
A1: [.s,g.] is closed by Th5;
assume
A2: (rng s1) c= [.s,g.];
then consider s2 be Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent by Th4,SEQ_4:40;
take s2;
ex Nseq 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;
hence thesis by A3,A4,A1;
end;
hence thesis;
end;
theorem Th7:
].p,q.[ is open
proof
defpred P[Real] means $1<=p or q<=$1;
consider X such that
A1: for r be Element of REAL holds r in X iff P[r] from SUBSET_1:sch 3;
now
let s1 such that
A2: (rng s1) c= X and
A3: s1 is convergent;
A4: lim s1 in REAL by XREAL_0:def 1;
lim s1<=p or q<=lim s1
proof
assume
A5: not thesis;
then 0<lim s1 - p by XREAL_1:50;
then consider n1 such that
A6: for m st n1<=m holds |.s1.m-lim s1.|<lim s1-p by A3,SEQ_2:def 7;
0<q - lim s1 by A5,XREAL_1:50;
then consider n such that
A7: for m st n<=m holds |.s1.m-lim s1.|<q-lim s1 by A3,SEQ_2:def 7;
consider k such that
A8: max(n,n1)<k by SEQ_4:3;
n1<=max(n,n1) by XXREAL_0:25;
then n1<=k by A8,XXREAL_0:2;
then
A9: |.s1.k-lim s1.|<lim s1 - p by A6;
-|.s1.k-lim s1.| <= s1.k-lim s1 by ABSVALUE:4;
then -(s1.k-lim s1) <= -(-|.s1.k-lim s1.|) by XREAL_1:24;
then -(s1.k-lim s1)<lim s1 - p by A9,XXREAL_0:2;
then -(lim s1 - p)< -(-(s1.k-lim s1)) by XREAL_1:24;
then p - lim s1 < s1.k-lim s1;
then
A10: p < s1.k by XREAL_1:9;
n<=max(n,n1) by XXREAL_0:25;
then n<=k by A8,XXREAL_0:2;
then
s1.k-lim s1 <= |.s1.k-lim s1.| & |.s1.k-lim s1.|<q-lim s1 by A7,
ABSVALUE:4;
then s1.k-lim s1 < q-lim s1 by XXREAL_0:2;
then
A11: s1.k < q by XREAL_1:9;
A12: k in NAT by ORDINAL1:def 12;
A13: s1.k in REAL by XREAL_0:def 1;
dom s1 = NAT by FUNCT_2:def 1;
then s1.k in rng s1 by FUNCT_1:def 3,A12;
hence contradiction by A1,A2,A11,A10,A13;
end;
hence lim s1 in X by A1,A4;
end;
then
A14: X is closed;
now
let r;
A15: r in REAL by XREAL_0:def 1;
assume r in ].p,q.[`;
then not r in ].p,q.[ by XBOOLE_0:def 5;
then r<=p or q<=r;
hence r in X by A1,A15;
end;
then
A16: ].p,q.[` c= X;
now
let r;
assume r in X;
then not ex s st s=r & p<s & s<q by A1;
then r in REAL & not r in ].p,q.[ by XREAL_0:def 1;
hence r in ].p,q.[` by XBOOLE_0:def 5;
end;
then X c= ].p,q.[`;
then ].p,q.[` = X by A16;
hence thesis by A14;
end;
registration
let p, q be Real;
cluster ].p,q.[ -> open for Subset of REAL;
coherence by Th7;
cluster [.p,q.] -> closed for Subset of REAL;
coherence by Th5;
end;
theorem Th8:
X is compact implies X is closed
proof
assume
A1: X is compact;
assume not X is closed;
then consider s1 such that
A2: rng s1 c= X and
A3: s1 is convergent & not lim s1 in X;
ex s2 st s2 is subsequence of s1 & s2 is convergent & (lim s2) in X by A1,A2;
hence contradiction by A3,SEQ_4:17;
end;
registration
cluster compact -> closed for Subset of REAL;
coherence by Th8;
end;
theorem Th9:
(for p st p in X ex r,n st 0<r & (for m st n<m holds r<|.s1.m-p.|))
implies for s2 st s2 is subsequence of s1 holds not (s2 is convergent &
lim s2 in X)
proof
assume that
A1: for p st p in X ex r,n st 0<r & for m st n<m holds r<|.s1.m-p.| and
A2: not for s2 st s2 is subsequence of s1 holds not (s2 is convergent &
lim s2 in X);
consider s2 such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent and
A5: lim s2 in X by A2;
consider r,n such that
A6: 0<r and
A7: for m st n<m holds r<|.s1.m - lim s2.| by A1,A5;
consider n1 such that
A8: for m st n1<=m holds |.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;
reconsider k = n + 1 + n1 as Element of NAT by ORDINAL1:def 12;
|.(s1*NS).k-(lim s2).|<r by A8,A9,NAT_1:11;
then
A10: |.s1.(NS.k)-(lim s2).|<r by FUNCT_2:15;
n + 1 <= k by NAT_1:11;
then
A11: n < k by NAT_1:13;
k<=NS.k by SEQM_3:14;
then n<NS.k by A11,XXREAL_0:2;
hence contradiction by A7,A10;
end;
theorem Th10:
X is compact implies X is real-bounded
proof
assume
A1: X is compact;
assume
A2: not X is real-bounded;
per cases by A2;
suppose
A3: not X is bounded_above;
defpred P[Element of NAT,Element of REAL] means ex q st q =$2 & q in X &
$1<q;
A4: for n being Element of NAT ex p being Element of REAL st P[n,p]
proof
let n be Element of NAT;
n is not UpperBound of X by A3,XXREAL_2:def 10;
then consider t being ExtReal such that
A5: t in X & n<t by XXREAL_2:def 1;
take t;
thus thesis by A5;
end;
consider f being sequence of REAL such that
A6: for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A4);
A7: now
let n;
n in NAT by ORDINAL1:def 12;
then ex q st q=f.n & q in X & n<q by A6;
hence f.n in X & n<f.n;
end;
A8: for p st p in X ex r,n st 0<r & for m st n<m holds r<|.f.m-p.|
proof
let p such that
p in X;
consider q such that
A9: q = 1;
take r = q;
consider k such that
A10: p+1<k by SEQ_4:3;
take n = k;
thus 0 < r by A9;
let m;
assume n<m;
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 thesis by A9,ABSVALUE:def 1;
end;
rng f c= X
proof
let x be object;
assume x in rng f;
then consider y being object such that
A11: y in dom f and
A12: x = f.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A11,FUNCT_2:def 1;
f.y in X by A7;
hence thesis by A12;
end;
then
ex s2 st s2 is subsequence of f & s2 is convergent & lim s2 in X by A1;
hence contradiction by A8,Th9;
end;
suppose
A13: not X is bounded_below;
defpred P[Element of NAT,Element of REAL] means ex q st q=$2 & q in X &
q<-$1;
A14: for n being Element of NAT ex p being Element of REAL st P[n,p]
proof
let n be Element of NAT;
-n is not LowerBound of X by A13,XXREAL_2:def 9;
then consider t being ExtReal such that
A15: t in X & t<-n by XXREAL_2:def 2;
take t;
thus thesis by A15;
end;
consider f being sequence of REAL such that
A16: for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(
A14);
A17: now
let n;
n in NAT by ORDINAL1:def 12;
then ex q st q=f.n & q in X & q<-n by A16;
hence f.n in X & f.n<-n;
end;
A18: for p st p in X ex r,n st 0<r & for m st n<m holds r<|.f.m-p.|
proof
let p such that
p in X;
consider q such that
A19: q = 1;
take r = q;
consider k such that
A20: |.p-1.| <k by SEQ_4:3;
take n = k;
thus 0 < r by A19;
let m;
assume n<m;
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 < |.-(f.m-p).| by A19,ABSVALUE:def 1;
hence thesis by COMPLEX1:52;
end;
rng f c= X
proof
let x be object;
assume x in rng f;
then consider y being object such that
A22: y in dom f and
A23: x = f.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A22,FUNCT_2:def 1;
f.y in X by A17;
hence thesis by A23;
end;
then
ex s2 st s2 is subsequence of f & s2 is convergent & lim s2 in X by A1;
hence contradiction by A18,Th9;
end;
end;
theorem
X is real-bounded closed implies X is compact
proof
assume that
A1: X is real-bounded and
A2: X is closed;
now
let s1 such that
A3: rng s1 c= X;
A4: s1 is bounded_below
proof
consider p such that
A5: p is LowerBound of X by A1,XXREAL_2:def 9;
A6: for q st q in X holds p<=q by A5,XXREAL_2:def 2;
take r = p - 1;
A7: r + 1 = p - (1-1);
A8: for t st t in rng s1 holds r < t
proof
let t;
assume t in rng s1;
then
A9: p<=t by A3,A6;
r < p by A7,XREAL_1:29;
hence thesis by A9,XXREAL_0:2;
end;
for n holds r < s1.n
proof
let n;
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:def 3;
hence thesis by A8;
end;
hence thesis;
end;
s1 is bounded_above
proof
consider p such that
A10: p is UpperBound of X by A1,XXREAL_2:def 10;
A11: for q st q in X holds q<=p by A10,XXREAL_2:def 1;
take r = p+1;
A12: for t st t in rng s1 holds t < r
proof
let t;
assume t in rng s1;
then
A13: t<=p by A3,A11;
p < r by XREAL_1:29;
hence thesis by A13,XXREAL_0:2;
end;
for n holds s1.n < r
proof
let n;
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:def 3;
hence thesis by A12;
end;
hence thesis;
end;
then s1 is bounded by A4;
then consider s2 be Real_Sequence such that
A14: s2 is subsequence of s1 and
A15: s2 is convergent by SEQ_4:40;
ex Nseq 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;
then lim s2 in X by A2,A15;
hence ex s2 st s2 is subsequence of s1 & s2 is convergent & lim s2 in X by
A14,A15;
end;
hence thesis;
end;
theorem Th12:
for X st X<>{} & X is closed & X is bounded_above holds upper_bound X in X
proof
let X such that
A1: X<>{} and
A2: X is closed and
A3: X is bounded_above and
A4: not upper_bound X in X;
set s1=upper_bound X;
defpred P[Element of NAT,Element of REAL] means ex q st q=$2 & q in X & s1 -
q < 1/($1+1);
A5: for n being Element of NAT ex p being Element of REAL st P[n,p]
proof
let n be Element of NAT;
0<(n+1)";
then 0<1/(n+1) by XCMPLX_1:215;
then consider t such that
A6: t in X and
A7: s1 -1/(n+1) <t by A1,A3,SEQ_4:def 1;
take t;
s1 < t + 1/(n+1) by A7,XREAL_1:19;
then s1 -t < 1/(n+1) by XREAL_1:19;
hence thesis by A6;
end;
consider f being sequence of REAL such that
A8: for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A5);
A9: now
let n;
n in NAT by ORDINAL1:def 12;
then ex q st q = f.n & q in X & s1 -q < 1/(n+1) by A8;
hence f.n in X & s1 - f.n<1/(n+1);
end;
A10: rng f c= X
proof
let x be object;
assume x in rng f;
then consider y being object such that
A11: y in dom f and
A12: x = f.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A11,FUNCT_2:def 1;
f.y in X by A9;
hence thesis by A12;
end;
A13: now
let s;
assume
A14: 0<s;
consider n such that
A15: s"<n by SEQ_4:3;
take k=n;
let m;
assume k<=m;
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 <= s1 by A3,SEQ_4:def 1;
then
A17: 0 <= s1-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 s1 - f.m<s by A9,XXREAL_0:2;
then |.-(f.m - s1).|<s by A17,ABSVALUE:def 1;
hence |.f.m - s1.|<s by COMPLEX1:52;
end;
then
A18: f is convergent;
then lim f=s1 by A13,SEQ_2:def 7;
hence contradiction by A2,A4,A18,A10;
end;
theorem Th13:
for X st X<>{} & X is closed & X is bounded_below holds lower_bound X in X
proof
let X such that
A1: X<>{} and
A2: X is closed and
A3: X is bounded_below and
A4: not lower_bound X in X;
set i1=lower_bound X;
defpred P[Element of NAT,Element of REAL] means ex q st q=$2 & q in X & q-i1
< 1/($1+1);
A5: for n being Element of NAT ex p being Element of REAL st P[n,p]
proof
let n be Element of NAT;
0<(n+1)";
then 0<1/(n+1) by XCMPLX_1:215;
then consider t such that
A6: t in X and
A7: t<i1 + 1/(n+1) by A1,A3,SEQ_4:def 2;
take t;
t-i1 < 1/(n+1) by A7,XREAL_1:19;
hence thesis by A6;
end;
consider f being sequence of REAL such that
A8: for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A5);
A9: now
let n;
n in NAT by ORDINAL1:def 12;
then ex q st q = f.n & q in X & q-i1 < 1/(n+1) by A8;
hence f.n in X & f.n-i1<1/(n+1);
end;
A10: rng f c= X
proof
let x be object;
assume x in rng f;
then consider y being object such that
A11: y in dom f and
A12: x = f.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A11,FUNCT_2:def 1;
f.y in X by A9;
hence thesis by A12;
end;
A13: now
let s;
assume
A14: 0<s;
consider n such that
A15: s"<n by SEQ_4:3;
take k=n;
let m;
assume k<=m;
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 i1<=f.m by A3,SEQ_4:def 2;
then
A17: 0 <= f.m-i1 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-i1<s by A9,XXREAL_0:2;
hence |.f.m-i1.|<s by A17,ABSVALUE:def 1;
end;
then
A18: f is convergent;
then lim f=i1 by A13,SEQ_2:def 7;
hence contradiction by A2,A4,A18,A10;
end;
theorem
for X st X<>{} & X is compact holds upper_bound X in X & lower_bound X in X
proof
let X such that
A1: X<>{} and
A2: X is compact;
X is real-bounded closed by A2,Th10;
hence thesis by A1,Th12,Th13;
end;
theorem
X is compact & (for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c= X)
implies ex p,g st X = [.p,g.]
proof
assume that
A1: X is compact and
A2: for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c= X;
per cases;
suppose
A3: X={};
take 1;
take 0;
thus thesis by A3,XXREAL_1:29;
end;
suppose
A4: X<>{};
take p=lower_bound X, g=upper_bound X;
A5: X is real-bounded closed by A1,Th10;
now
let r be Element of REAL;
assume r in X;
then r<=g & p<=r by A5,SEQ_4:def 1,def 2;
hence r in [.p,g.];
end;
then
A6: X c= [.p,g.];
upper_bound X in X & lower_bound X in X by A4,A5,Th12,Th13;
then [.p,g.] c= X by A2;
hence thesis by A6;
end;
end;
registration
cluster open for Subset of REAL;
existence
proof
take ].0,1.[;
thus thesis;
end;
end;
definition
let r be Real;
mode Neighbourhood of r -> Subset of REAL means
:Def6:
ex g st 0<g & it = ]. r-g,r+g.[;
existence
proof
take ].r-1,r+1.[;
thus thesis;
end;
end;
registration
let r be Real;
cluster -> open for Neighbourhood of r;
coherence
proof
let A be Neighbourhood of r;
ex g st 0<g & A = ].r-g,r+g.[ by Def6;
hence thesis;
end;
end;
theorem
for N being Neighbourhood of r holds r in N
proof
let N be Neighbourhood of r;
( ex g st 0<g & N = ].r-g,r+g.[)& |.r-r.| = 0 by Def6,ABSVALUE:2;
hence thesis by Th1;
end;
theorem
for r for N1,N2 being Neighbourhood of r ex N being Neighbourhood of r
st N c= N1 & N c= N2
proof
let r;
let N1,N2 be Neighbourhood of r;
consider g1 such that
A1: 0<g1 and
A2: ].r-g1,r+g1.[ = N1 by Def6;
consider g2 such that
A3: 0<g2 and
A4: ].r-g2,r+g2.[ = N2 by Def6;
set g = min(g1,g2);
0<g by A1,A3,XXREAL_0:15;
then reconsider N = ].r-g,r+g.[ as Neighbourhood of r by Def6;
take N;
A5: g<=g1 by XXREAL_0:17;
then
A6: r+g<=r+g1 by XREAL_1:7;
-g1<=-g by A5,XREAL_1:24;
then
A7: r+-g1<=r+-g by XREAL_1:7;
A8: g<=g2 by XXREAL_0:17;
then -g2<=-g by XREAL_1:24;
then
A9: r+-g2<=r+-g by XREAL_1:7;
A10: r+g<=r+g2 by A8,XREAL_1:7;
now
per cases;
suppose
A11: g1<=g2;
A12: now
let y be object;
assume
A13: y in ].r-g,r+g.[;
then reconsider x1=y as Real;
ex p2 st y = p2 & r-g<p2 & p2<r+g by A13;
then x1<r+g2 & r-g2<x1 by A10,A9,XXREAL_0:2;
hence y in ].r-g2,r+g2.[;
end;
g1=g by A11,XXREAL_0:def 9;
hence ].r-g,r+g.[ c= N1 & ].r-g,r+g.[ c= N2 by A2,A4,A12;
end;
suppose
A14: g2<=g1;
A15: now
let y be object;
assume
A16: y in ].r-g,r+g.[;
then reconsider x1=y as Real;
ex p2 st y = p2 & r-g<p2 & p2<r+g by A16;
then x1<r+g1 & r-g1<x1 by A6,A7,XXREAL_0:2;
hence y in ].r-g1,r+g1.[;
end;
g2=g by A14,XXREAL_0:def 9;
hence ].r-g,r+g.[ c= N1 & ].r-g,r+g.[ c= N2 by A2,A4,A15;
end;
end;
hence thesis;
end;
theorem Th18:
for X being open Subset of REAL, r st r in X ex N being
Neighbourhood of r st N c= X
proof
let X be open Subset of REAL, r;
assume that
A1: r in X and
A2: for N be Neighbourhood of r holds not N c= X;
defpred P[Nat,Real] means $2 in ].r - 1/($1+1),r + 1/($1+1
) .[ & $2 in X`;
A3: now
let N be Neighbourhood of r;
consider g such that
0<g and
A4: N = ].r-g,r+g.[ by Def6;
not N c= X by A2;
then consider x being object such that
A5: x in N and
A6: not x in X;
consider s such that
A7: x=s and
r-g<s and
s<r+g by A5,A4;
reconsider s as Element of REAL by XREAL_0:def 1;
take s;
thus s in N by A5,A7;
thus s in X` by A6,A7,XBOOLE_0:def 5;
end;
A8: for n being Element of NAT ex s being Element of REAL st P[n,s]
proof
let n be Element of NAT;
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 be Element of REAL st s in N & s in X` by A3;
hence thesis;
end;
consider s3 such that
A9: for n being Element of NAT holds P[n,s3.n] from FUNCT_2:sch 3(A8);
deffunc G(Nat)= r + 1/($1+1);
deffunc F(Nat)= r - 1/($1+1);
consider s1 be Real_Sequence such that
A10: for n holds s1.n = F(n) from SEQ_1:sch 1;
consider s2 be Real_Sequence such that
A11: for n holds s2.n = G(n) from SEQ_1:sch 1;
A12: for n holds s1.n <= s3.n & s3.n <= s2.n
proof
let n;
n in NAT by ORDINAL1:def 12;
then s3.n in].r - 1/(n+1),r + 1/(n+1) .[ by A9;
then
A13: ex s st s = s3.n & r - 1/(n+1) <s & s<r + 1/(n+1);
hence s1.n <= s3.n by A10;
thus thesis by A11,A13;
end;
A14: rng s3 c= X`
proof
let x be object;
assume x in rng s3;
then consider y being object such that
A15: y in dom s3 and
A16: s3.y=x by FUNCT_1:def 3;
reconsider y as Element of NAT by A15,FUNCT_2:def 1;
s3.y in X` by A9;
hence thesis by A16;
end;
A17: X` is closed by Def5;
A18: now
let s;
assume
A19: 0<s;
consider n such that
A20: s"<n by SEQ_4:3;
take n;
let m;
assume n<=m;
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;
|.s2.m - r.| = |.r + 1/(m+1) - r.| by A11
.= 1/(m+1) by ABSVALUE:def 1;
hence |.s2.m - r.| <s by A22,A21,XXREAL_0:2;
end;
then
A23: s2 is convergent;
then
A24: lim s2 = r by A18,SEQ_2:def 7;
A25: now
let s;
assume
A26: 0<s;
consider n such that
A27: s"<n by SEQ_4:3;
take n;
let m;
assume n<=m;
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;
|.s1.m - r.| = |.r - 1/(m+1) - r.| by A10
.= |.- 1/(m+1).|
.= |.1/(m+1).| by COMPLEX1:52
.= 1/(m+1) by ABSVALUE:def 1;
hence |.s1.m - r.| <s by A29,A28,XXREAL_0:2;
end;
then
A30: s1 is convergent;
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,20;
then r in X` by A14,A17;
hence contradiction by A1,XBOOLE_0:def 5;
end;
theorem
for X being open Subset of REAL, r st r in X ex g st 0<g & ].r-g,r+g.[ c= X
proof
let X be open Subset of REAL, r;
assume r in X;
then consider N be Neighbourhood of r such that
A1: N c= X by Th18;
consider g such that
A2: 0<g & N = ].r-g,r+g.[ by Def6;
take g;
thus thesis by A1,A2;
end;
theorem
(for r being Element of REAL st r in X
ex N be Neighbourhood of r st N c= X) implies X
is open
proof
assume that
A1: for r being Element of REAL st r in X
ex N be Neighbourhood of r st N c= X and
A2: not X is open;
not X` is closed by A2;
then consider s1 such that
A3: rng s1 c= X` and
A4: s1 is convergent and
A5: not lim s1 in X`;
reconsider ls = lim s1 as Element of REAL by XREAL_0:def 1;
consider N be Neighbourhood of ls such that
A6: N c= X by A1,A5,SUBSET_1:29;
consider g such that
A7: 0<g and
A8: ]. (lim s1) - g, (lim s1) + g .[ = N by Def6;
consider n such that
A9: for m st n<=m holds |.s1.m - (lim s1).|<g by A4,A7,SEQ_2:def 7;
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then
A10: s1.n in rng s1 by FUNCT_1:def 3;
A11: |.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: (lim s1) - g < s & s <(lim s1) + g} by A12;
hence contradiction by A3,A6,A8,A10,XBOOLE_0:def 5;
end;
theorem Th21:
X is open bounded_above implies not upper_bound X in X
proof
assume that
A1: X is open and
A2: X is bounded_above;
assume upper_bound X in X;
then consider N being Neighbourhood of upper_bound X such that
A3: N c= X by A1,Th18;
consider t 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,215;
A7: upper_bound X + t/2 +t/2 > upper_bound X + t/2 by A4,XREAL_1:29,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: upper_bound X-t<s & s<
upper_bound X+t} by A7;
hence contradiction by A2,A3,A5,A6,SEQ_4:def 1;
end;
theorem Th22:
X is open bounded_below implies not lower_bound X in X
proof
assume that
A1: X is open and
A2: X is bounded_below;
assume lower_bound X in X;
then consider N being Neighbourhood of lower_bound X such that
A3: N c= X by A1,Th18;
consider t 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,215;
A7: lower_bound X - t/2 - t/2 < lower_bound X - t/2 by A4,XREAL_1:44,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: lower_bound X-t<s & s<
lower_bound X+t} by A7;
hence contradiction by A2,A3,A5,A6,SEQ_4:def 2;
end;
theorem
X is open real-bounded & (for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c=
X) implies ex p,g st X = ].p,g.[
proof
assume that
A1: X is open and
A2: X is real-bounded and
A3: for g1,g2 st g1 in X & g2 in X holds [.g1,g2.] c= X;
per cases;
suppose
A4: X={};
take 1;
take 0;
thus thesis by A4,XXREAL_1:28;
end;
suppose
A5: X<>{};
take p=lower_bound X, g=upper_bound X;
now
let r be Element of REAL;
thus r in X implies r in ].p,g.[
proof
assume
A6: r in X;
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 thesis by A7;
end;
assume r in ].p,g.[;
then
A8: ex s st s=r & p<s & s<g;
then g-r>0 by XREAL_1:50;
then consider g2 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 such that
A10: g1 in X & g1<p+(r-p) by A2,A5,SEQ_4:def 2;
reconsider g1, g2 as Real;
r in {s: g1<=s & s<=g2} & [.g1,g2.] c= X by A3,A9,A10;
hence r in X;
end;
hence thesis by SUBSET_1:3;
end;
end;
:: From RCOMP_2, AG 19.12.2008
definition
let g be Real,s be ExtReal;
redefine func [. g,s .[ -> Subset of REAL equals :: redefines [. (XXREAL_1, definition)
{ r : g<=r & r<s };
coherence
proof
now
let e be object;
assume e in [. g,s .[;
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;
end;
hence thesis by TARSKI:def 3;
end;
compatibility
proof
set Y = {r: g<=r & r<s };
let X be Subset of REAL;
A2: [. g,s .[ c= Y
proof
let e be object;
assume e in [. g,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 thesis by A3,A4;
end;
Y c= [. g,s .[
proof
let e be object;
assume e in Y;
then consider r such that
A5: e = r & g <= r & r<s;
r in REAL by XREAL_0:def 1;
hence thesis by A5,NUMBERS:31;
end;
hence thesis by A2;
end;
end;
definition
let g be ExtReal,s be Real;
redefine func ]. g,s .] -> Subset of REAL equals :: redefines ]. (XXREAL_1, definition)
{ r: g<r & r<=s };
coherence
proof
now
let e be object;
assume e in ]. g,s .];
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;
end;
hence thesis by TARSKI:def 3;
end;
compatibility
proof
set Y = {r: g<r & r<=s };
let X be Subset of REAL;
A2: ]. g,s .] c= Y
proof
let e be object;
assume e in ]. g,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 thesis by A3,A4;
end;
Y c= ]. g,s .]
proof
let e be object;
assume e in Y;
then consider r such that
A5: e = r & g < r & r<=s;
r in REAL by XREAL_0:def 1;
hence thesis by A5,NUMBERS:31;
end;
hence thesis by A2;
end;
end;