:: Topological Properties of Subsets in Real Numbers
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


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 end;
compatibility
for b1 being Subset of REAL holds
( b1 = [.g,s.] iff b1 = { r where r is Real : ( g <= r & r <= s ) } )
proof 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 end;
compatibility
for b1 being Subset of REAL holds
( b1 = ].g,s.[ iff b1 = { r where r is Real : ( g < r & r < s ) } )
proof 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 :: RCOMP_1:1
canceled;

theorem :: RCOMP_1:2
canceled;

theorem :: RCOMP_1:3
canceled;

theorem :: RCOMP_1:4
canceled;

theorem :: RCOMP_1:5
canceled;

theorem :: RCOMP_1:6
canceled;

theorem :: RCOMP_1:7
canceled;

theorem Th8: :: RCOMP_1:8
for r, p, g being real number holds
( r in ].(p - g),(p + g).[ iff abs (r - p) < g )
proof end;

theorem :: RCOMP_1:9
for r, p, g being real number holds
( r in [.p,g.] iff abs ((p + g) - (2 * r)) <= g - p )
proof end;

theorem :: RCOMP_1:10
for r, p, g being real number holds
( r in ].p,g.[ iff abs ((p + g) - (2 * r)) < g - p )
proof end;

definition
let X be Subset of REAL;
attr X 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;
attr X 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;
attr X 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 :: RCOMP_1:11
canceled;

theorem :: RCOMP_1:12
canceled;

theorem :: RCOMP_1:13
canceled;

theorem :: RCOMP_1:14
canceled;

theorem :: RCOMP_1:15
canceled;

theorem :: RCOMP_1:16
canceled;

theorem :: RCOMP_1:17
canceled;

theorem :: RCOMP_1:18
canceled;

theorem :: RCOMP_1:19
canceled;

theorem :: RCOMP_1:20
canceled;

theorem :: RCOMP_1:21
canceled;

theorem Th22: :: RCOMP_1:22
for s, g being real number
for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
s1 is bounded
proof end;

theorem Th23: :: RCOMP_1:23
for s, g being real number holds [.s,g.] is closed
proof end;

theorem :: RCOMP_1:24
for s, g being real number holds [.s,g.] is compact
proof end;

theorem Th25: :: RCOMP_1:25
for p, q being real number holds ].p,q.[ is open
proof end;

registration
let p, q be real number ;
cluster ].p,q.[ -> open Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = ].p,q.[ holds
b1 is open by Th25;
cluster [.p,q.] -> closed Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = [.p,q.] holds
b1 is closed by Th23;
end;

theorem Th26: :: RCOMP_1:26
for X being Subset of REAL st X is compact holds
X is closed
proof end;

registration
cluster compact -> closed Element of K21(REAL);
coherence
for b1 being Subset of REAL st b1 is compact holds
b1 is closed by Th26;
end;

theorem Th27: :: RCOMP_1:27
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 end;

theorem Th28: :: RCOMP_1:28
for X being Subset of REAL st X is compact holds
X is bounded
proof end;

theorem :: RCOMP_1:29
for X being Subset of REAL st X is bounded & X is closed holds
X is compact
proof end;

theorem Th30: :: RCOMP_1:30
for X being Subset of REAL st X <> {} & X is closed & X is bounded_above holds
upper_bound X in X
proof end;

theorem Th31: :: RCOMP_1:31
for X being Subset of REAL st X <> {} & X is closed & X is bounded_below holds
lower_bound X in X
proof end;

theorem :: RCOMP_1:32
for X being Subset of REAL st X <> {} & X is compact holds
( upper_bound X in X & lower_bound X in X )
proof end;

theorem :: RCOMP_1:33
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 end;

registration
cluster V50() V51() V52() open Element of K21(REAL);
existence
ex b1 being Subset of REAL st b1 is open
proof end;
end;

definition
let r be real number ;
canceled;
mode Neighbourhood of r -> Subset of REAL means :Def7: :: RCOMP_1:def 7
 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 end;
end;

:: deftheorem RCOMP_1:def 6 :
canceled;

:: deftheorem Def7 defines Neighbourhood RCOMP_1:def 7 :
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 Neighbourhood of r;
coherence
for b1 being Neighbourhood of r holds b1 is open
proof end;
end;

theorem :: RCOMP_1:34
canceled;

theorem :: RCOMP_1:35
canceled;

theorem :: RCOMP_1:36
canceled;

theorem :: RCOMP_1:37
for r being real number
for N being Neighbourhood of r holds r in N
proof end;

theorem :: RCOMP_1:38
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 end;

theorem Th39: :: RCOMP_1:39
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 end;

theorem :: RCOMP_1:40
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 end;

theorem :: RCOMP_1:41
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 end;

theorem :: RCOMP_1:42
canceled;

theorem Th43: :: RCOMP_1:43
for X being Subset of REAL st X is open & X is bounded_above holds
not upper_bound X in X
proof end;

theorem Th44: :: RCOMP_1:44
for X being Subset of REAL st X is open & X is bounded_below holds
not lower_bound X in X
proof end;

theorem :: RCOMP_1:45
for X being Subset of REAL st X is open & X is 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 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 8
 { r where r is Real : ( g <= r & r < s ) } ;
coherence
[.g,s.[ is Subset of REAL
proof end;
compatibility
for b1 being Subset of REAL holds
( b1 = [.g,s.[ iff b1 = { r where r is Real : ( g <= r & r < s ) } )
proof end;
end;

:: deftheorem defines [. RCOMP_1:def 8 :
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 9
 { r where r is Real : ( g < r & r <= s ) } ;
coherence
].g,s.] is Subset of REAL
proof end;
compatibility
for b1 being Subset of REAL holds
( b1 = ].g,s.] iff b1 = { r where r is Real : ( g < r & r <= s ) } )
proof end;
end;

:: deftheorem defines ]. RCOMP_1:def 9 :
for g being ext-real number
for s being real number holds ].g,s.] = { r where r is Real : ( g < r & r <= s ) } ;