:: RCOMP_1 semantic presentation

scheme :: RCOMP_1:sch 1
RealSeqChoice{ P₁[ set , set ] } :

ex s1 being Function of NAT , REAL st
for n being Nat holds P₁[n,s1 . n]

provided

A1: for n being Nat ex r being real number st P₁[n,r]

proof end;

theorem Th1: :: RCOMP_1:1

for X, Y being Subset of REAL st ( for r being real number st r in X holds
r in Y ) holds
X c= Y

proof end;

theorem :: RCOMP_1:2

canceled;

theorem Th3: :: RCOMP_1:3

for Y1, Y being Subset of REAL st Y1 c= Y & Y is bounded_below holds
Y1 is bounded_below

proof end;

theorem Th4: :: RCOMP_1:4

for Y1, Y being Subset of REAL st Y1 c= Y & Y is bounded_above holds
Y1 is bounded_above

proof end;

theorem :: RCOMP_1:5

for Y1, Y being Subset of REAL st Y1 c= Y & Y is bounded holds
Y1 is bounded

proof end;

definition

let g, s be real number ;
func [.g,s.] -> Subset of REAL equals :: RCOMP_1:def 1
{ r where r is Real : ( g <= r & r <= s ) } ;
coherence

proof end;

end;

:: deftheorem defines [. RCOMP_1:def 1 :

definition

let g, s be real number ;
func ].g,s.[ -> Subset of REAL equals :: RCOMP_1:def 2
{ r where r is Real : ( g < r & r < s ) } ;
coherence

proof end;

end;

:: deftheorem defines ]. RCOMP_1:def 2 :

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;

theorem :: RCOMP_1:11

for g, s being real number st g <= s holds
[.g,s.] = ].g,s.[ \/ {g,s}

proof end;

theorem Th12: :: RCOMP_1:12

for p, g being real number st p <= g holds
].g,p.[ = {}

proof end;

theorem Th13: :: RCOMP_1:13

for p, g being real number st p < g holds
[.g,p.] = {}

proof end;

theorem :: RCOMP_1:14

for p being real number holds [.p,p.] = {p}

proof end;

theorem :: RCOMP_1:15

for p, g being real number holds
( ( p < g implies ].p,g.[ <> {} ) & ( p <= g implies ( p in [.p,g.] & g in [.p,g.] ) ) & ].p,g.[ c= [.p,g.] )

proof end;

theorem :: RCOMP_1:16

for r, p, g, s being real number st r in [.p,g.] & s in [.p,g.] holds
[.r,s.] c= [.p,g.]

proof end;

theorem :: RCOMP_1:17

for r, p, g, s being real number st r in ].p,g.[ & s in ].p,g.[ holds
[.r,s.] c= ].p,g.[

proof end;

theorem :: RCOMP_1:18

for p, g being real number st p <= g holds
[.p,g.] = [.p,g.] \/ [.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 :

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 :

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 :

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 ;
coherence by Th25;
cluster [.p,q.] -> closed ;
coherence by Th23;

end;

theorem Th26: :: RCOMP_1:26

for X being Subset of REAL st X is compact holds
X is closed

proof 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 Nat st
( 0 < r & ( for m being 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 open Element of K40(REAL );
existence

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

proof end;

end;

:: deftheorem RCOMP_1:def 6 :

:: deftheorem Def7 defines Neighbourhood RCOMP_1:def 7 :

registration

let r be real number ;
cluster -> open Neighbourhood of r;
coherence

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

for X being Subset of REAL holds
( ( for r being real number st r in X holds
ex N being Neighbourhood of r st N c= X ) iff X is open ) by Th39, Th41;

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;

theorem :: RCOMP_1:46

for r, s being real number holds ].r,s.[ misses {r,s}

proof end;

theorem :: RCOMP_1:47

for a, b, c being real number holds
( c in ].a,b.[ iff ( a < c & c < b ) )

proof end;

theorem :: RCOMP_1:48

for a, b, c being real number holds
( c in [.a,b.] iff ( a <= c & c <= b ) )

proof end;