:: Topological Properties of Subsets in Real Numbers
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: 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 b₁ being Subset of REAL holds
( b₁ = [.g,s.] iff b₁ = { 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 b₁ being Subset of REAL holds
( b₁ = ].g,s.[ iff b₁ = { 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 b₁ being Subset of REAL st b₁ = ].p,q.[ holds
b₁ is open by Th7;

cluster [.p,q.] -> closed for Subset of REAL;

coherence
for b₁ being Subset of REAL st b₁ = [.p,q.] holds
b₁ 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 b₁ being Subset of REAL st b₁ is compact holds
b₁ 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 b₁ being Subset of REAL st b₁ 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 b₁ being Subset of REAL ex g being Real st
( 0 < g & b₁ = ].(r - g),(r + g).[ )

proof end;

end;

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

registration

let r be Real;

cluster -> open for Neighbourhood of r;

coherence
for b₁ being Neighbourhood of r holds b₁ 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 b₁ being Subset of REAL holds
( b₁ = [.g,s.[ iff b₁ = { 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 b₁ being Subset of REAL holds
( b₁ = ].g,s.] iff b₁ = { 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 ) } ;