:: by Konrad Raczkowski and Pawe{\l} Sadowski

::

:: Received June 18, 1990

:: Copyright (c) 1990 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

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

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

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

].g,s.[ is Subset of REAL

proof end;

compatibility for b

( b

proof 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

proof end;

theorem :: RCOMP_1:9

proof end;

theorem :: RCOMP_1:10

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

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

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

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

proof end;

theorem Th23: :: RCOMP_1:23

proof end;

theorem :: RCOMP_1:24

proof end;

theorem Th25: :: RCOMP_1:25

proof end;

registration

let p, q be real number ;

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

coherence

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

b_{1} is open
by Th25;

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

coherence

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

b_{1} is closed
by Th23;

end;
cluster ].p,q.[ -> open Subset of REAL;

coherence

for b

b

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

coherence

for b

b

theorem Th26: :: RCOMP_1:26

proof end;

registration

cluster compact -> closed Element of K21(REAL);

coherence

for b_{1} being Subset of REAL st b_{1} is compact holds

b_{1} is closed
by Th26;

end;
coherence

for b

b

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

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

proof end;

theorem :: RCOMP_1:29

proof end;

theorem Th30: :: RCOMP_1:30

proof end;

theorem Th31: :: RCOMP_1:31

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 )

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

[.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 b_{1} being Subset of REAL st b_{1} is open

end;
existence

ex b

proof 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 b_{1} being Subset of REAL ex g being real number st

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

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

( 0 < g & b

proof end;

:: deftheorem RCOMP_1:def 6 :

canceled;

:: deftheorem Def7 defines Neighbourhood RCOMP_1:def 7 :

for r being real number

for b

( b

( 0 < g & b

registration

let r be real number ;

cluster -> open Neighbourhood of r;

coherence

for b_{1} being Neighbourhood of r holds b_{1} is open

end;
cluster -> open Neighbourhood of r;

coherence

for b

proof end;

theorem :: RCOMP_1:34

canceled;

theorem :: RCOMP_1:35

canceled;

theorem :: RCOMP_1:36

canceled;

theorem :: RCOMP_1:37

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 )

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

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 )

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

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

proof end;

theorem Th44: :: RCOMP_1:44

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

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

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 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 b

( b

proof 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

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 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 b

( b

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