:: Topological Properties of Subsets in Real Numbers
::
:: Copyright (c) 1990-2021 Association of Mizar Users

definition
let g, s be Real;
:: 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 holds [.g,s.] = { r where r is Real : ( g <= r & r <= s ) } ;

definition
let g, s be ExtReal;
:: 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 ExtReal holds ].g,s.[ = { r where r is Real : ( g < r & r < s ) } ;

theorem Th1: :: RCOMP_1:1
for g, r, p being Real holds
( r in ].(p - g),(p + g).[ iff |.(r - p).| < g )
proof end;

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

theorem :: RCOMP_1:3
for g, r, p being Real holds
( r in ].p,g.[ iff |.((p + g) - (2 * r)).| < g - p )
proof end;

definition
let X be Subset of REAL;
attr X is compact means :: 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 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 :: RCOMP_1:def 4
for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X;
end;

:: deftheorem 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 Th4: :: RCOMP_1:4
for s, g being Real
for s1 being Real_Sequence st rng s1 c= [.s,g.] holds
s1 is bounded
proof end;

theorem Th5: :: RCOMP_1:5
for s, g being Real holds [.s,g.] is closed
proof end;

theorem :: RCOMP_1:6
for s, g being Real holds [.s,g.] is compact
proof end;

theorem Th7: :: RCOMP_1:7
for p, q being Real holds ].p,q.[ is open
proof end;

registration
let p, q be Real;
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 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 st p in X holds
ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((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 Th10: :: RCOMP_1:10
for X being Subset of REAL st X is compact holds
X is real-bounded
proof end;

theorem :: RCOMP_1:11
for X being Subset of REAL st X is real-bounded & X is closed holds
X is compact
proof 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 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 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 end;

theorem :: RCOMP_1:15
for X being Subset of REAL st X is compact & ( for g1, g2 being Real st g1 in X & g2 in X holds
[.g1,g2.] c= X ) holds
ex p, g being Real st X = [.p,g.]
proof end;

registration
cluster V57() V58() V59() open for Element of K19(REAL);
existence
ex b1 being Subset of REAL st b1 is open
proof end;
end;

definition
let r be Real;
mode Neighbourhood of r -> Subset of REAL means :Def6: :: RCOMP_1:def 6
ex g being Real st
( 0 < g & it = ].(r - g),(r + g).[ );
existence
ex b1 being Subset of REAL ex g being Real st
( 0 < g & b1 = ].(r - g),(r + g).[ )
proof end;
end;

:: deftheorem Def6 defines Neighbourhood RCOMP_1:def 6 :
for r being Real
for b2 being Subset of REAL holds
( b2 is Neighbourhood of r iff ex g being Real st
( 0 < g & b2 = ].(r - g),(r + g).[ ) );

registration
let r be Real;
cluster -> open for Neighbourhood of r;
coherence
for b1 being Neighbourhood of r holds b1 is open
proof end;
end;

theorem :: RCOMP_1:16
for r being Real
for N being Neighbourhood of r holds r in N
proof end;

theorem :: RCOMP_1:17
for r being Real
for N1, N2 being Neighbourhood of r ex N being Neighbourhood of r st
( N c= N1 & N c= N2 )
proof end;

theorem Th18: :: RCOMP_1:18
for X being open Subset of REAL
for r being Real st r in X holds
ex N being Neighbourhood of r st N c= X
proof end;

theorem :: RCOMP_1:19
for X being open Subset of REAL
for r being Real st r in X holds
ex g being Real st
( 0 < g & ].(r - g),(r + g).[ c= X )
proof end;

theorem :: RCOMP_1:20
for X being Subset of REAL st ( for r being Element of REAL st r in X holds
ex N being Neighbourhood of r st N c= X ) holds
X is open
proof 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 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 end;

theorem :: RCOMP_1:23
for X being Subset of REAL st X is open & X is real-bounded & ( for g1, g2 being Real st g1 in X & g2 in X holds
[.g1,g2.] c= X ) holds
ex p, g being Real st X = ].p,g.[
proof end;

:: From RCOMP_2, AG 19.12.2008
definition
let g be Real;
let s be ExtReal;
:: 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 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 7 :
for g being Real
for s being ExtReal holds [.g,s.[ = { r where r is Real : ( g <= r & r < s ) } ;

definition
let g be ExtReal;
let s be Real;
:: 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 ExtReal
for s being Real holds ].g,s.] = { r where r is Real : ( g < r & r <= s ) } ;