:: RCOMP_1 semantic presentation

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

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

provided

E1: for b₁ being Nat ex b₂ being real number st P₁[b₁,b₂]

proof end;

theorem Th1: :: RCOMP_1:1

for b₁, b₂ being Subset of REAL st ( for b₃ being real number st b₃ in b₁ holds
b₃ in b₂ ) holds
b₁ c= b₂

proof end;

theorem Th2: :: RCOMP_1:2

canceled;

theorem Th3: :: RCOMP_1:3

for b₁, b₂ being Subset of REAL st b₁ c= b₂ & b₂ is bounded_below holds
b₁ is bounded_below

proof end;

theorem Th4: :: RCOMP_1:4

for b₁, b₂ being Subset of REAL st b₁ c= b₂ & b₂ is bounded_above holds
b₁ is bounded_above

proof end;

theorem Th5: :: RCOMP_1:5

for b₁, b₂ being Subset of REAL st b₁ c= b₂ & b₂ is bounded holds
b₁ is bounded

proof end;

definition

let c₁, c₂ be real number ;
func [.c₁,c₂.] -> Subset of REAL equals :: RCOMP_1:def 1
{ b₁ where B is Real : ( a₁ <= b₁ & b₁ <= a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines [. RCOMP_1:def 1 :

definition

let c₁, c₂ be real number ;
func ].c₁,c₂.[ -> Subset of REAL equals :: RCOMP_1:def 2
{ b₁ where B is Real : ( a₁ < b₁ & b₁ < a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines ]. RCOMP_1:def 2 :

theorem Th6: :: RCOMP_1:6

canceled;

theorem Th7: :: RCOMP_1:7

canceled;

theorem Th8: :: RCOMP_1:8

for b₁, b₂, b₃ being real number holds
( b₁ in ].(b₂ - b₃),(b₂ + b₃).[ iff abs (b₁ - b₂) < b₃ )

proof end;

theorem Th9: :: RCOMP_1:9

for b₁, b₂, b₃ being real number holds
( b₁ in [.b₂,b₃.] iff abs ((b₂ + b₃) - (2 * b₁)) <= b₃ - b₂ )

proof end;

theorem Th10: :: RCOMP_1:10

for b₁, b₂, b₃ being real number holds
( b₁ in ].b₂,b₃.[ iff abs ((b₂ + b₃) - (2 * b₁)) < b₃ - b₂ )

proof end;

theorem Th11: :: RCOMP_1:11

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₁,b₂.] = ].b₁,b₂.[ \/ {b₁,b₂}

proof end;

theorem Th12: :: RCOMP_1:12

for b₁, b₂ being real number st b₁ <= b₂ holds
].b₂,b₁.[ = {}

proof end;

theorem Th13: :: RCOMP_1:13

for b₁, b₂ being real number st b₁ < b₂ holds
[.b₂,b₁.] = {}

proof end;

theorem Th14: :: RCOMP_1:14

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

proof end;

theorem Th15: :: RCOMP_1:15

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

proof end;

theorem Th16: :: RCOMP_1:16

for b₁, b₂, b₃, b₄ being real number st b₁ in [.b₂,b₃.] & b₄ in [.b₂,b₃.] holds
[.b₁,b₄.] c= [.b₂,b₃.]

proof end;

theorem Th17: :: RCOMP_1:17

for b₁, b₂, b₃, b₄ being real number st b₁ in ].b₂,b₃.[ & b₄ in ].b₂,b₃.[ holds
[.b₁,b₄.] c= ].b₂,b₃.[

proof end;

theorem Th18: :: RCOMP_1:18

for b₁, b₂ being real number st b₁ <= b₂ holds
[.b₁,b₂.] = [.b₁,b₂.] \/ [.b₂,b₁.]

proof end;

definition

let c₁ be Subset of REAL ;
attr a₁ is compact means :Def3: :: RCOMP_1:def 3
for b₁ being Real_Sequence st rng b₁ c= a₁ holds
ex b₂ being Real_Sequence st
( b₂ is subsequence of b₁ & b₂ is convergent & lim b₂ in a₁ );

end;

:: deftheorem Def3 defines compact RCOMP_1:def 3 :

definition

let c₁ be Subset of REAL ;
attr a₁ is closed means :Def4: :: RCOMP_1:def 4
for b₁ being Real_Sequence st rng b₁ c= a₁ & b₁ is convergent holds
lim b₁ in a₁;

end;

:: deftheorem Def4 defines closed RCOMP_1:def 4 :

definition

let c₁ be Subset of REAL ;
attr a₁ is open means :Def5: :: RCOMP_1:def 5
a₁ ` is closed;

end;

:: deftheorem Def5 defines open RCOMP_1:def 5 :

theorem Th19: :: RCOMP_1:19

canceled;

theorem Th20: :: RCOMP_1:20

canceled;

theorem Th21: :: RCOMP_1:21

canceled;

theorem Th22: :: RCOMP_1:22

for b₁, b₂ being real number
for b₃ being Real_Sequence st rng b₃ c= [.b₁,b₂.] holds
b₃ is bounded

proof end;

theorem Th23: :: RCOMP_1:23

for b₁, b₂ being real number holds [.b₁,b₂.] is closed

proof end;

theorem Th24: :: RCOMP_1:24

for b₁, b₂ being real number holds [.b₁,b₂.] is compact

proof end;

theorem Th25: :: RCOMP_1:25

for b₁, b₂ being real number holds ].b₁,b₂.[ is open

proof end;

registration

let c₁, c₂ be real number ;
cluster ].a₁,a₂.[ -> open ;
coherence by Th25;
cluster [.a₁,a₂.] -> closed ;
coherence by Th23;

end;

theorem Th26: :: RCOMP_1:26

for b₁ being Subset of REAL st b₁ is compact holds
b₁ is closed

proof end;

theorem Th27: :: RCOMP_1:27

for b₁ being Real_Sequence
for b₂ being Subset of REAL st ( for b₃ being real number st b₃ in b₂ holds
ex b₄ being real number ex b₅ being Nat st
( 0 < b₄ & ( for b₆ being Nat st b₅ < b₆ holds
b₄ < abs ((b₁ . b₆) - b₃) ) ) ) holds
for b₃ being Real_Sequence st b₃ is subsequence of b₁ & b₃ is convergent holds
not lim b₃ in b₂

proof end;

theorem Th28: :: RCOMP_1:28

for b₁ being Subset of REAL st b₁ is compact holds
b₁ is bounded

proof end;

theorem Th29: :: RCOMP_1:29

for b₁ being Subset of REAL st b₁ is bounded & b₁ is closed holds
b₁ is compact

proof end;

theorem Th30: :: RCOMP_1:30

for b₁ being Subset of REAL st b₁ <> {} & b₁ is closed & b₁ is bounded_above holds
upper_bound b₁ in b₁

proof end;

theorem Th31: :: RCOMP_1:31

for b₁ being Subset of REAL st b₁ <> {} & b₁ is closed & b₁ is bounded_below holds
lower_bound b₁ in b₁

proof end;

theorem Th32: :: RCOMP_1:32

for b₁ being Subset of REAL st b₁ <> {} & b₁ is compact holds
( upper_bound b₁ in b₁ & lower_bound b₁ in b₁ )

proof end;

theorem Th33: :: RCOMP_1:33

for b₁ being Subset of REAL st b₁ is compact & ( for b₂, b₃ being real number st b₂ in b₁ & b₃ in b₁ holds
[.b₂,b₃.] c= b₁ ) holds
ex b₂, b₃ being real number st b₁ = [.b₂,b₃.]

proof end;

registration

cluster open Element of K40(REAL );
existence

proof end;

end;

definition

let c₁ be real number ;
canceled;
mode Neighbourhood of c₁ -> Subset of REAL means :Def7: :: RCOMP_1:def 7
ex b₁ being real number st
( 0 < b₁ & a₂ = ].(a₁ - b₁),(a₁ + b₁).[ );
existence

proof end;

end;

:: deftheorem Def6 RCOMP_1:def 6 :

:: deftheorem Def7 defines Neighbourhood RCOMP_1:def 7 :

registration

let c₁ be real number ;
cluster -> open Neighbourhood of a₁;
coherence

proof end;

end;

theorem Th34: :: RCOMP_1:34

canceled;

theorem Th35: :: RCOMP_1:35

canceled;

theorem Th36: :: RCOMP_1:36

canceled;

theorem Th37: :: RCOMP_1:37

for b₁ being real number
for b₂ being Neighbourhood of b₁ holds b₁ in b₂

proof end;

theorem Th38: :: RCOMP_1:38

for b₁ being real number
for b₂, b₃ being Neighbourhood of b₁ ex b₄ being Neighbourhood of b₁ st
( b₄ c= b₂ & b₄ c= b₃ )

proof end;

theorem Th39: :: RCOMP_1:39

for b₁ being open Subset of REAL
for b₂ being real number st b₂ in b₁ holds
ex b₃ being Neighbourhood of b₂ st b₃ c= b₁

proof end;

theorem Th40: :: RCOMP_1:40

for b₁ being open Subset of REAL
for b₂ being real number st b₂ in b₁ holds
ex b₃ being real number st
( 0 < b₃ & ].(b₂ - b₃),(b₂ + b₃).[ c= b₁ )

proof end;

theorem Th41: :: RCOMP_1:41

for b₁ being Subset of REAL st ( for b₂ being real number st b₂ in b₁ holds
ex b₃ being Neighbourhood of b₂ st b₃ c= b₁ ) holds
b₁ is open

proof end;

theorem Th42: :: RCOMP_1:42

for b₁ being Subset of REAL holds
( ( for b₂ being real number st b₂ in b₁ holds
ex b₃ being Neighbourhood of b₂ st b₃ c= b₁ ) iff b₁ is open ) by Th39, Th41;

theorem Th43: :: RCOMP_1:43

for b₁ being Subset of REAL st b₁ is open & b₁ is bounded_above holds
not upper_bound b₁ in b₁

proof end;

theorem Th44: :: RCOMP_1:44

for b₁ being Subset of REAL st b₁ is open & b₁ is bounded_below holds
not lower_bound b₁ in b₁

proof end;

theorem Th45: :: RCOMP_1:45

for b₁ being Subset of REAL st b₁ is open & b₁ is bounded & ( for b₂, b₃ being real number st b₂ in b₁ & b₃ in b₁ holds
[.b₂,b₃.] c= b₁ ) holds
ex b₂, b₃ being real number st b₁ = ].b₂,b₃.[

proof end;

theorem Th46: :: RCOMP_1:46

for b₁, b₂ being real number holds ].b₁,b₂.[ misses {b₁,b₂}

proof end;

theorem Th47: :: RCOMP_1:47

for b₁, b₂, b₃ being real number holds
( b₃ in ].b₁,b₂.[ iff ( b₁ < b₃ & b₃ < b₂ ) )

proof end;

theorem Th48: :: RCOMP_1:48

for b₁, b₂, b₃ being real number holds
( b₃ in [.b₁,b₂.] iff ( b₁ <= b₃ & b₃ <= b₂ ) )

proof end;