let x be R_eal;
assume A1: 0. <' x ;
func Seg x -> non empty Subset of ExtREAL means :Def2: :: MEASURE6:def 2
for y being R_eal holds
( y in it iff ( 0. <' y & y + y <' x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Seg MEASURE6:def 2 :

definition

let x be R_eal;
func len x -> R_eal equals :: MEASURE6:def 3
sup (Seg x);
correctness ;

end;

:: deftheorem defines len MEASURE6:def 3 :

theorem Th27: :: MEASURE6:27

for x being R_eal st 0. <' x holds
0. <' len x

proof end;

theorem Th28: :: MEASURE6:28

for x being R_eal st 0. <' x holds
len x <=' x

proof end;

theorem Th29: :: MEASURE6:29

for x being R_eal st 0. <' x & x <' +infty holds
len x is Real

proof end;

theorem Th30: :: MEASURE6:30

for x being R_eal st 0. <' x holds
(len x) + (len x) <=' x

proof end;

theorem :: MEASURE6:31

for eps being R_eal st 0. <' eps holds
ex F being Function of NAT , ExtREAL st
( ( for n being Nat holds 0. <' F . n ) & SUM F <' eps )

proof end;

theorem :: MEASURE6:32

for eps being R_eal
for X being non empty Subset of ExtREAL st 0. <' eps & inf X is Real holds
ex x being R_eal st
( x in X & x <' (inf X) + eps )

proof end;

theorem :: MEASURE6:33

for eps being R_eal
for X being non empty Subset of ExtREAL st 0. <' eps & sup X is Real holds
ex x being R_eal st
( x in X & (sup X) - eps <' x )

proof end;

theorem :: MEASURE6:34

for F being Function of NAT , ExtREAL st F is nonnegative & SUM F <' +infty holds
for n being Nat holds F . n in REAL

proof end;

definition

:: original: -infty
redefine func -infty -> R_eal;
correctness by SUPINF_1:11;
:: original: +infty
redefine func +infty -> R_eal;
correctness by SUPINF_1:11;

end;

theorem :: MEASURE6:35

( REAL is Interval & REAL = ].-infty ,+infty .[ & REAL = [.-infty ,+infty .] & REAL = [.-infty ,+infty .[ & REAL = ].-infty ,+infty .] )

proof end;

theorem Th36: :: MEASURE6:36

for a, b being R_eal st b = -infty holds
( ].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {} )

proof end;

theorem Th37: :: MEASURE6:37

for a, b being R_eal st a = +infty holds
( ].a,b.[ = {} & [.a,b.] = {} & [.a,b.[ = {} & ].a,b.] = {} )

proof end;

theorem Th38: :: MEASURE6:38

for A being Interval
for a, b being R_eal
for c, d, e being Real st A = ].a,b.[ & c in A & d in A & c <= e & e <= d holds
e in A

proof end;

theorem Th39: :: MEASURE6:39

for A being Interval
for a, b being R_eal
for c, d, e being Real st A = [.a,b.] & c in A & d in A & c <= e & e <= d holds
e in A

proof end;

theorem Th40: :: MEASURE6:40

for A being Interval
for a, b being R_eal
for c, d, e being Real st A = ].a,b.] & c in A & d in A & c <= e & e <= d holds
e in A

proof end;

theorem Th41: :: MEASURE6:41

for A being Interval
for a, b being R_eal
for c, d, e being Real st A = [.a,b.[ & c in A & d in A & c <= e & e <= d holds
e in A

proof end;

theorem Th42: :: MEASURE6:42

for A being non empty Subset of ExtREAL
for m, M being R_eal st m = inf A & M = sup A & ( for c, d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A ) & not m in A & not M in A holds
A = ].m,M.[

proof end;

theorem Th43: :: MEASURE6:43

for A being non empty Subset of ExtREAL
for m, M being R_eal st m = inf A & M = sup A & ( for c, d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A ) & m in A & M in A & A c= REAL holds
A = [.m,M.]

proof end;

theorem Th44: :: MEASURE6:44

for A being non empty Subset of ExtREAL
for m, M being R_eal st m = inf A & M = sup A & ( for c, d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A ) & m in A & not M in A & A c= REAL holds
A = [.m,M.[

proof end;

theorem Th45: :: MEASURE6:45

for A being non empty Subset of ExtREAL
for m, M being R_eal st m = inf A & M = sup A & ( for c, d being Real st c in A & d in A holds
for e being Real st c <= e & e <= d holds
e in A ) & not m in A & M in A & A c= REAL holds
A = ].m,M.]

proof end;

theorem Th46: :: MEASURE6:46

for A being Subset of REAL holds
( A is Interval iff for a, b being Real st a in A & b in A holds
for c being Real st a <= c & c <= b holds
c in A )

proof end;

theorem :: MEASURE6:47

for A, B being Interval st A meets B holds
A \/ B is Interval

proof end;

definition

let A be Interval;
assume A1: A <> {} ;
func ^^ A -> R_eal means :Def4: :: MEASURE6:def 4
ex b being R_eal st
( it <=' b & ( A = ].it,b.[ or A = ].it,b.] or A = [.it,b.] or A = [.it,b.[ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ^^ MEASURE6:def 4 :

definition

let A be Interval;
assume A1: A <> {} ;
func A ^^ -> R_eal means :Def5: :: MEASURE6:def 5
ex a being R_eal st
( a <=' it & ( A = ].a,it.[ or A = ].a,it.] or A = [.a,it.] or A = [.a,it.[ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ^^ MEASURE6:def 5 :

theorem Th48: :: MEASURE6:48

for A being Interval st A is open_interval & A <> {} holds
( ^^ A <=' A ^^ & A = ].(^^ A),(A ^^ ).[ )

proof end;

theorem Th49: :: MEASURE6:49

for A being Interval st A is closed_interval & A <> {} holds
( ^^ A <=' A ^^ & A = [.(^^ A),(A ^^ ).] )

proof end;

theorem Th50: :: MEASURE6:50

for A being Interval st A is right_open_interval & A <> {} holds
( ^^ A <=' A ^^ & A = [.(^^ A),(A ^^ ).[ )

proof end;

theorem Th51: :: MEASURE6:51

for A being Interval st A is left_open_interval & A <> {} holds
( ^^ A <=' A ^^ & A = ].(^^ A),(A ^^ ).] )

proof end;

theorem Th52: :: MEASURE6:52

for A being Interval st A <> {} holds
( ^^ A <=' A ^^ & ( A = ].(^^ A),(A ^^ ).[ or A = ].(^^ A),(A ^^ ).] or A = [.(^^ A),(A ^^ ).] or A = [.(^^ A),(A ^^ ).[ ) )

proof end;

theorem :: MEASURE6:53

canceled;

theorem Th54: :: MEASURE6:54

for A being Interval
for a being real number st a in A holds
( ^^ A <=' R_EAL a & R_EAL a <=' A ^^ )

proof end;

theorem Th55: :: MEASURE6:55

for A, B being Interval
for a, b being real number st a in A & b in B & A ^^ <=' ^^ B holds
a <= b

proof end;

theorem :: MEASURE6:56

for A being Interval
for a being R_eal st a in A holds
( ^^ A <=' a & a <=' A ^^ )

proof end;

theorem Th57: :: MEASURE6:57

for A being Interval st A <> {} holds
for a being R_eal st ^^ A <' a & a <' A ^^ holds
a in A

proof end;

theorem :: MEASURE6:58

for A, B being Interval st A ^^ = ^^ B & ( A ^^ in A or ^^ B in B ) holds
A \/ B is Interval

proof end;

definition

let A be Subset of REAL ;
let x be real number ;
func x + A -> Subset of REAL means :Def6: :: MEASURE6:def 6
for y being Real holds
( y in it iff ex z being Real st
( z in A & y = x + z ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines + MEASURE6:def 6 :

theorem Th59: :: MEASURE6:59

for A being Subset of REAL
for x being real number holds (- x) + (x + A) = A

proof end;

theorem :: MEASURE6:60

for x being real number
for A being Subset of REAL st A = REAL holds
x + A = A

proof end;

theorem :: MEASURE6:61

for x being real number holds x + {} = {}

proof end;

theorem Th62: :: MEASURE6:62

for A being Interval
for x being real number holds
( A is open_interval iff x + A is open_interval )

proof end;

theorem Th63: :: MEASURE6:63

for A being Interval
for x being real number holds
( A is closed_interval iff x + A is closed_interval )

proof end;

theorem Th64: :: MEASURE6:64

for A being Interval
for x being real number holds
( A is right_open_interval iff x + A is right_open_interval )

proof end;

theorem Th65: :: MEASURE6:65

for A being Interval
for x being real number holds
( A is left_open_interval iff x + A is left_open_interval )

proof end;

theorem Th66: :: MEASURE6:66

for A being Interval
for x being real number holds x + A is Interval

proof end;

registration

let A be Interval;
let x be real number ;
cluster x + A -> interval ;
correctness by Th66;

end;

theorem :: MEASURE6:67

for A being Interval
for x being real number holds vol A = vol (x + A)

proof end;