:: MEASURE6 semantic presentation

theorem Th1: :: MEASURE6:1

ex b₁ being Function of NAT ,[:NAT ,NAT :] st
( b₁ is one-to-one & dom b₁ = NAT & rng b₁ = [:NAT ,NAT :] )

proof end;

theorem Th2: :: MEASURE6:2

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative holds
0. <=' SUM b₁

proof end;

theorem Th3: :: MEASURE6:3

for b₁ being Function of NAT , ExtREAL
for b₂ being R_eal st ex b₃ being Nat st b₂ <=' b₁ . b₃ & b₁ is nonnegative holds
b₂ <=' SUM b₁

proof end;

theorem Th4: :: MEASURE6:4

canceled;

theorem Th5: :: MEASURE6:5

canceled;

theorem Th6: :: MEASURE6:6

canceled;

theorem Th7: :: MEASURE6:7

canceled;

theorem Th8: :: MEASURE6:8

for b₁, b₂ being R_eal st b₁ is Real holds
( (b₂ - b₁) + b₁ = b₂ & (b₂ + b₁) - b₁ = b₂ )

proof end;

theorem Th9: :: MEASURE6:9

canceled;

theorem Th10: :: MEASURE6:10

for b₁, b₂, b₃ being R_eal st b₃ in REAL & b₂ <' b₁ holds
(b₃ + b₁) - (b₃ + b₂) = b₁ - b₂

proof end;

theorem Th11: :: MEASURE6:11

for b₁, b₂, b₃ being R_eal st b₃ in REAL & b₁ <=' b₂ holds
( b₃ + b₁ <=' b₃ + b₂ & b₁ + b₃ <=' b₂ + b₃ & b₁ - b₃ <=' b₂ - b₃ )

proof end;

theorem Th12: :: MEASURE6:12

for b₁, b₂, b₃ being R_eal st b₃ in REAL & b₁ <' b₂ holds
( b₃ + b₁ <' b₃ + b₂ & b₁ + b₃ <' b₂ + b₃ & b₁ - b₃ <' b₂ - b₃ )

proof end;

definition

let c₁ be real number ;
func R_EAL c₁ -> R_eal equals :: MEASURE6:def 1
a₁;
coherence

proof end;

end;

:: deftheorem Def1 defines R_EAL MEASURE6:def 1 :

theorem Th13: :: MEASURE6:13

for b₁, b₂ being real number holds
( b₁ <= b₂ iff R_EAL b₁ <=' R_EAL b₂ ) by SUPINF_1:120;

theorem Th14: :: MEASURE6:14

for b₁, b₂ being real number holds
( b₁ < b₂ iff R_EAL b₁ <' R_EAL b₂ ) by Th13;

theorem Th15: :: MEASURE6:15

for b₁, b₂, b₃ being R_eal st b₁ <' b₂ & b₂ <' b₃ holds
b₂ is Real

proof end;

theorem Th16: :: MEASURE6:16

for b₁, b₂, b₃ being R_eal st b₁ is Real & b₃ is Real & b₁ <=' b₂ & b₂ <=' b₃ holds
b₂ is Real

proof end;

theorem Th17: :: MEASURE6:17

for b₁, b₂, b₃ being R_eal st b₁ is Real & b₁ <=' b₂ & b₂ <' b₃ holds
b₂ is Real

proof end;

theorem Th18: :: MEASURE6:18

for b₁, b₂, b₃ being R_eal st b₁ <' b₂ & b₂ <=' b₃ & b₃ is Real holds
b₂ is Real

proof end;

theorem Th19: :: MEASURE6:19

for b₁, b₂ being R_eal st 0. <' b₁ & b₁ <' b₂ holds
0. <' b₂ - b₁

proof end;

theorem Th20: :: MEASURE6:20

for b₁, b₂, b₃ being R_eal st 0. <=' b₁ & 0. <=' b₃ & b₃ + b₁ <' b₂ holds
b₃ <' b₂ - b₁

proof end;

theorem Th21: :: MEASURE6:21

for b₁ being R_eal holds b₁ - 0. = b₁

proof end;

theorem Th22: :: MEASURE6:22

for b₁, b₂, b₃ being R_eal st 0. <=' b₁ & 0. <=' b₃ & b₃ + b₁ <' b₂ holds
b₃ <=' b₂

proof end;

theorem Th23: :: MEASURE6:23

for b₁ being R_eal st 0. <' b₁ holds
ex b₂ being R_eal st
( 0. <' b₂ & b₂ <' b₁ )

proof end;

theorem Th24: :: MEASURE6:24

for b₁, b₂ being R_eal st 0. <' b₁ & b₁ <' b₂ holds
ex b₃ being R_eal st
( 0. <' b₃ & b₁ + b₃ <' b₂ & b₃ in REAL )

proof end;

theorem Th25: :: MEASURE6:25

for b₁, b₂ being R_eal st 0. <=' b₁ & b₁ <' b₂ holds
ex b₃ being R_eal st
( 0. <' b₃ & b₁ + b₃ <' b₂ & b₃ in REAL )

proof end;

theorem Th26: :: MEASURE6:26

for b₁ being R_eal st 0. <' b₁ holds
ex b₂ being R_eal st
( 0. <' b₂ & b₂ + b₂ <' b₁ )

proof end;

definition

let c₁ be R_eal;
assume E15: 0. <' c₁ ;
func Seg c₁ -> non empty Subset of ExtREAL means :Def2: :: MEASURE6:def 2
for b₁ being R_eal holds
( b₁ in a₂ iff ( 0. <' b₁ & b₁ + b₁ <' a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Seg MEASURE6:def 2 :

definition

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

end;

:: deftheorem Def3 defines len MEASURE6:def 3 :

theorem Th27: :: MEASURE6:27

for b₁ being R_eal st 0. <' b₁ holds
0. <' len b₁

proof end;

theorem Th28: :: MEASURE6:28

for b₁ being R_eal st 0. <' b₁ holds
len b₁ <=' b₁

proof end;

theorem Th29: :: MEASURE6:29

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

proof end;

theorem Th30: :: MEASURE6:30

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

proof end;

theorem Th31: :: MEASURE6:31

for b₁ being R_eal st 0. <' b₁ holds
ex b₂ being Function of NAT , ExtREAL st
( ( for b₃ being Nat holds 0. <' b₂ . b₃ ) & SUM b₂ <' b₁ )

proof end;

theorem Th32: :: MEASURE6:32

for b₁ being R_eal
for b₂ being non empty Subset of ExtREAL st 0. <' b₁ & inf b₂ is Real holds
ex b₃ being R_eal st
( b₃ in b₂ & b₃ <' (inf b₂) + b₁ )

proof end;

theorem Th33: :: MEASURE6:33

for b₁ being R_eal
for b₂ being non empty Subset of ExtREAL st 0. <' b₁ & sup b₂ is Real holds
ex b₃ being R_eal st
( b₃ in b₂ & (sup b₂) - b₁ <' b₃ )

proof end;

theorem Th34: :: MEASURE6:34

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

proof end;

definition

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

end;

theorem Th35: :: MEASURE6:35

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

proof end;

theorem Th36: :: MEASURE6:36

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

proof end;

theorem Th37: :: MEASURE6:37

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

proof end;

theorem Th38: :: MEASURE6:38

for b₁ being Interval
for b₂, b₃ being R_eal
for b₄, b₅, b₆ being Real st b₁ = ].b₂,b₃.[ & b₄ in b₁ & b₅ in b₁ & b₄ <= b₆ & b₆ <= b₅ holds
b₆ in b₁

proof end;

theorem Th39: :: MEASURE6:39

for b₁ being Interval
for b₂, b₃ being R_eal
for b₄, b₅, b₆ being Real st b₁ = [.b₂,b₃.] & b₄ in b₁ & b₅ in b₁ & b₄ <= b₆ & b₆ <= b₅ holds
b₆ in b₁

proof end;

theorem Th40: :: MEASURE6:40

for b₁ being Interval
for b₂, b₃ being R_eal
for b₄, b₅, b₆ being Real st b₁ = ].b₂,b₃.] & b₄ in b₁ & b₅ in b₁ & b₄ <= b₆ & b₆ <= b₅ holds
b₆ in b₁

proof end;

theorem Th41: :: MEASURE6:41

for b₁ being Interval
for b₂, b₃ being R_eal
for b₄, b₅, b₆ being Real st b₁ = [.b₂,b₃.[ & b₄ in b₁ & b₅ in b₁ & b₄ <= b₆ & b₆ <= b₅ holds
b₆ in b₁

proof end;

theorem Th42: :: MEASURE6:42

for b₁ being non empty Subset of ExtREAL
for b₂, b₃ being R_eal st b₂ = inf b₁ & b₃ = sup b₁ & ( for b₄, b₅ being Real st b₄ in b₁ & b₅ in b₁ holds
for b₆ being Real st b₄ <= b₆ & b₆ <= b₅ holds
b₆ in b₁ ) & not b₂ in b₁ & not b₃ in b₁ holds
b₁ = ].b₂,b₃.[

proof end;

theorem Th43: :: MEASURE6:43

for b₁ being non empty Subset of ExtREAL
for b₂, b₃ being R_eal st b₂ = inf b₁ & b₃ = sup b₁ & ( for b₄, b₅ being Real st b₄ in b₁ & b₅ in b₁ holds
for b₆ being Real st b₄ <= b₆ & b₆ <= b₅ holds
b₆ in b₁ ) & b₂ in b₁ & b₃ in b₁ & b₁ c= REAL holds
b₁ = [.b₂,b₃.]

proof end;

theorem Th44: :: MEASURE6:44

for b₁ being non empty Subset of ExtREAL
for b₂, b₃ being R_eal st b₂ = inf b₁ & b₃ = sup b₁ & ( for b₄, b₅ being Real st b₄ in b₁ & b₅ in b₁ holds
for b₆ being Real st b₄ <= b₆ & b₆ <= b₅ holds
b₆ in b₁ ) & b₂ in b₁ & not b₃ in b₁ & b₁ c= REAL holds
b₁ = [.b₂,b₃.[

proof end;

theorem Th45: :: MEASURE6:45

proof end;

theorem Th46: :: MEASURE6:46

for b₁ being Subset of REAL holds
( b₁ is Interval iff for b₂, b₃ being Real st b₂ in b₁ & b₃ in b₁ holds
for b₄ being Real st b₂ <= b₄ & b₄ <= b₃ holds
b₄ in b₁ )

proof end;

theorem Th47: :: MEASURE6:47

for b₁, b₂ being Interval st b₁ meets b₂ holds
b₁ \/ b₂ is Interval

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

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

definition

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

proof end;

uniqueness

proof end;

end;

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

theorem Th48: :: MEASURE6:48

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

proof end;

theorem Th49: :: MEASURE6:49

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

proof end;

theorem Th50: :: MEASURE6:50

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

proof end;

theorem Th51: :: MEASURE6:51

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

proof end;

theorem Th52: :: MEASURE6:52

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

proof end;

theorem Th53: :: MEASURE6:53

canceled;

theorem Th54: :: MEASURE6:54

for b₁ being Interval
for b₂ being real number st b₂ in b₁ holds
( ^^ b₁ <=' R_EAL b₂ & R_EAL b₂ <=' b₁ ^^ )

proof end;

theorem Th55: :: MEASURE6:55

for b₁, b₂ being Interval
for b₃, b₄ being real number st b₃ in b₁ & b₄ in b₂ & b₁ ^^ <=' ^^ b₂ holds
b₃ <= b₄

proof end;

theorem Th56: :: MEASURE6:56

for b₁ being Interval
for b₂ being R_eal st b₂ in b₁ holds
( ^^ b₁ <=' b₂ & b₂ <=' b₁ ^^ )

proof end;

theorem Th57: :: MEASURE6:57

for b₁ being Interval st b₁ <> {} holds
for b₂ being R_eal st ^^ b₁ <' b₂ & b₂ <' b₁ ^^ holds
b₂ in b₁

proof end;

theorem Th58: :: MEASURE6:58

for b₁, b₂ being Interval st b₁ ^^ = ^^ b₂ & ( b₁ ^^ in b₁ or ^^ b₂ in b₂ ) holds
b₁ \/ b₂ is Interval

proof end;

definition

let c₁ be Subset of REAL ;
let c₂ be real number ;
func c₂ + c₁ -> Subset of REAL means :Def6: :: MEASURE6:def 6
for b₁ being Real holds
( b₁ in a₃ iff ex b₂ being Real st
( b₂ in a₁ & b₁ = a₂ + b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines + MEASURE6:def 6 :

theorem Th59: :: MEASURE6:59

for b₁ being Subset of REAL
for b₂ being real number holds (- b₂) + (b₂ + b₁) = b₁

proof end;

theorem Th60: :: MEASURE6:60

for b₁ being real number
for b₂ being Subset of REAL st b₂ = REAL holds
b₁ + b₂ = b₂

proof end;

theorem Th61: :: MEASURE6:61

for b₁ being real number holds b₁ + {} = {}

proof end;

theorem Th62: :: MEASURE6:62

for b₁ being Interval
for b₂ being real number holds
( b₁ is open_interval iff b₂ + b₁ is open_interval )

proof end;

theorem Th63: :: MEASURE6:63

for b₁ being Interval
for b₂ being real number holds
( b₁ is closed_interval iff b₂ + b₁ is closed_interval )

proof end;

theorem Th64: :: MEASURE6:64

for b₁ being Interval
for b₂ being real number holds
( b₁ is right_open_interval iff b₂ + b₁ is right_open_interval )

proof end;

theorem Th65: :: MEASURE6:65

for b₁ being Interval
for b₂ being real number holds
( b₁ is left_open_interval iff b₂ + b₁ is left_open_interval )

proof end;

theorem Th66: :: MEASURE6:66

for b₁ being Interval
for b₂ being real number holds b₂ + b₁ is Interval

proof end;

registration

let c₁ be Interval;
let c₂ be real number ;
cluster a₂ + a₁ -> interval ;
correctness by Th66;

end;

theorem Th67: :: MEASURE6:67

for b₁ being Interval
for b₂ being real number holds vol b₁ = vol (b₂ + b₁)

proof end;