:: Topological Properties of Subsets in Real Numbers
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2016 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
{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
{r : g=-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.|-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) 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 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{} & 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) {} & 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{} & 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 open for Neighbourhood of r;
coherence
proof
let A be Neighbourhood of r;
ex g st 00 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-t0 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{};
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: pr & r<=g by A1,A2,A6,Th21,SEQ_4:def 1;
then r0 by XREAL_1:50;
then consider g2 such that
A9: g2 in X & g-(g-r)0 by A8,XREAL_1:50;
then consider g1 such that
A10: g1 in X & g1

Subset of REAL equals
{ r : g<=r & r Subset of REAL equals
{ r: g