:: 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;

[.g,s.] is Subset of REAL

for b_{1} being Subset of REAL holds

( b_{1} = [.g,s.] iff b_{1} = { r where r is Real : ( g <= r & r <= s ) } )

end;
:: original: [.

redefine func [.g,s.] -> Subset of REAL equals :: RCOMP_1:def 1

{ r where r is Real : ( g <= r & r <= s ) } ;

coherence redefine func [.g,s.] -> Subset of REAL equals :: RCOMP_1:def 1

{ r where r is Real : ( g <= r & r <= s ) } ;

[.g,s.] is Subset of REAL

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines [. RCOMP_1:def 1 :

for g, s being Real holds [.g,s.] = { r where r is Real : ( g <= r & r <= s ) } ;

for g, s being Real holds [.g,s.] = { r where r is Real : ( g <= r & r <= s ) } ;

definition

let g, s be ExtReal;

].g,s.[ is Subset of REAL

for b_{1} being Subset of REAL holds

( b_{1} = ].g,s.[ iff b_{1} = { r where r is Real : ( g < r & r < s ) } )

end;
:: original: ].

redefine func ].g,s.[ -> Subset of REAL equals :: RCOMP_1:def 2

{ r where r is Real : ( g < r & r < s ) } ;

coherence redefine func ].g,s.[ -> Subset of REAL equals :: RCOMP_1:def 2

{ r where r is Real : ( g < r & r < s ) } ;

].g,s.[ is Subset of REAL

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines ]. RCOMP_1:def 2 :

for g, s being ExtReal holds ].g,s.[ = { r where r is Real : ( g < r & r < s ) } ;

for g, s being ExtReal holds ].g,s.[ = { r where r is Real : ( g < r & r < s ) } ;

definition

let X be Subset of REAL;

end;
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 );

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 );

:: 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 ) );

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;

end;
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;

for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds

lim s1 in X;

:: 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 );

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
end;

:: deftheorem Def5 defines open RCOMP_1:def 5 :

for X being Subset of REAL holds

( X is open iff X ` is closed );

for X being Subset of REAL holds

( X is open iff X ` is closed );

registration

let p, q be Real;

coherence

for b_{1} being Subset of REAL st b_{1} = ].p,q.[ holds

b_{1} is open
by Th7;

coherence

for b_{1} being Subset of REAL st b_{1} = [.p,q.] holds

b_{1} is closed
by Th5;

end;
coherence

for b

b

coherence

for b

b

registration
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

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 :: 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 )

( 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.]

[.g1,g2.] c= X ) holds

ex p, g being Real st X = [.p,g.]

proof end;

definition

let r be Real;

ex b_{1} being Subset of REAL ex g being Real st

( 0 < g & b_{1} = ].(r - g),(r + g).[ )

end;
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 g being Real st

( 0 < g & it = ].(r - g),(r + g).[ );

ex b

( 0 < g & b

proof end;

:: deftheorem Def6 defines Neighbourhood RCOMP_1:def 6 :

for r being Real

for b_{2} being Subset of REAL holds

( b_{2} is Neighbourhood of r iff ex g being Real st

( 0 < g & b_{2} = ].(r - g),(r + g).[ ) );

for r being Real

for b

( b

( 0 < g & b

registration
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 )

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

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 )

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

ex N being Neighbourhood of r st N c= X ) holds

X is open

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.[

[.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;

[.g,s.[ is Subset of REAL

for b_{1} being Subset of REAL holds

( b_{1} = [.g,s.[ iff b_{1} = { r where r is Real : ( g <= r & r < s ) } )

end;
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 redefine func [.g,s.[ -> Subset of REAL equals :: RCOMP_1:def 7

{ r where r is Real : ( g <= r & r < s ) } ;

[.g,s.[ is Subset of REAL

proof end;

compatibility for b

( b

proof 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 ) } ;

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;

].g,s.] is Subset of REAL

for b_{1} being Subset of REAL holds

( b_{1} = ].g,s.] iff b_{1} = { r where r is Real : ( g < r & r <= s ) } )

end;
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 redefine func ].g,s.] -> Subset of REAL equals :: RCOMP_1:def 8

{ r where r is Real : ( g < r & r <= s ) } ;

].g,s.] is Subset of REAL

proof end;

compatibility for b

( b

proof 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 ) } ;

for g being ExtReal

for s being Real holds ].g,s.] = { r where r is Real : ( g < r & r <= s ) } ;