:: by Noboru Endou

::

:: Received January 13, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

theorem Th1: :: MEASUR12:1

for A, B being non empty Interval st A is open_interval & B is open_interval & A \/ B is Interval holds

( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

proof end;

theorem Th2: :: MEASUR12:2

for A, B being open_interval Subset of REAL st A meets B holds

A \/ B is open_interval Subset of REAL

A \/ B is open_interval Subset of REAL

proof end;

Lm1: for A being closed_interval Subset of REAL

for B, C being open_interval Subset of REAL st A c= B \/ C & A meets B & A meets C holds

B meets C

proof end;

Lm2: for A, B, C being open_interval Subset of REAL st A c= B \/ C & A meets B & A meets C holds

B meets C

proof end;

Lm3: for A being right_open_interval Subset of REAL

for B, C being open_interval Subset of REAL st A c= B \/ C & A meets B & A meets C holds

B meets C

proof end;

Lm4: for A being left_open_interval Subset of REAL

for B, C being open_interval Subset of REAL st A c= B \/ C & A meets B & A meets C holds

B meets C

proof end;

theorem :: MEASUR12:3

for A being Interval

for B, C being open_interval Subset of REAL st A c= B \/ C & A meets B & A meets C holds

B meets C

for B, C being open_interval Subset of REAL st A c= B \/ C & A meets B & A meets C holds

B meets C

proof end;

theorem Th4: :: MEASUR12:4

for A, B being non empty set

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.] & A misses B & not q < r holds

s < p

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.] & A misses B & not q < r holds

s < p

proof end;

theorem Th5: :: MEASUR12:5

for A, B being non empty set

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.[ & A misses B & not q < r holds

s <= p

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.[ & A misses B & not q < r holds

s <= p

proof end;

theorem Th6: :: MEASUR12:6

for A, B being non empty set

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.] & A misses B & not q <= r holds

s < p

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.] & A misses B & not q <= r holds

s < p

proof end;

theorem Th7: :: MEASUR12:7

for A, B being non empty set

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

proof end;

theorem Th8: :: MEASUR12:8

for A, B being non empty set

for p, q, r, s being R_eal st A = [.p,q.[ & B = [.r,s.[ & A misses B & not q <= r holds

s <= p

for p, q, r, s being R_eal st A = [.p,q.[ & B = [.r,s.[ & A misses B & not q <= r holds

s <= p

proof end;

theorem Th9: :: MEASUR12:9

for A, B being non empty set

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.] & A misses B & not q <= r holds

s < p

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.] & A misses B & not q <= r holds

s < p

proof end;

theorem Th10: :: MEASUR12:10

for A, B being non empty set

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

proof end;

theorem Th11: :: MEASUR12:11

for A, B being non empty set

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.] & A misses B & not q <= r holds

s <= p

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.] & A misses B & not q <= r holds

s <= p

proof end;

theorem Th12: :: MEASUR12:12

for A, B being non empty set

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

proof end;

theorem Th13: :: MEASUR12:13

for A, B being non empty set

for p, q, r, s being R_eal st A = ].p,q.[ & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

for p, q, r, s being R_eal st A = ].p,q.[ & B = ].r,s.[ & A misses B & not q <= r holds

s <= p

proof end;

theorem Th14: :: MEASUR12:14

for A, B being non empty Interval

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.] & A misses B holds

not A \/ B is Interval

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.] & A misses B holds

not A \/ B is Interval

proof end;

theorem Th15: :: MEASUR12:15

for A, B being non empty Interval

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.[ & A misses B & A \/ B is Interval holds

( p = s & A \/ B = [.r,q.] )

for p, q, r, s being R_eal st A = [.p,q.] & B = [.r,s.[ & A misses B & A \/ B is Interval holds

( p = s & A \/ B = [.r,q.] )

proof end;

theorem Th16: :: MEASUR12:16

for A, B being non empty Interval

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.] & A misses B & A \/ B is Interval holds

( q = r & A \/ B = [.p,s.] )

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.] & A misses B & A \/ B is Interval holds

( q = r & A \/ B = [.p,s.] )

proof end;

theorem Th17: :: MEASUR12:17

for A, B being non empty Interval

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval & not ( p = s & A \/ B = ].r,q.] ) holds

( q = r & A \/ B = [.p,s.[ )

for p, q, r, s being R_eal st A = [.p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval & not ( p = s & A \/ B = ].r,q.] ) holds

( q = r & A \/ B = [.p,s.[ )

proof end;

theorem Th18: :: MEASUR12:18

for A, B being non empty Interval

for p, q, r, s being R_eal st A = [.p,q.[ & B = [.r,s.[ & A misses B & A \/ B is Interval & not ( p = s & A \/ B = [.r,q.[ ) holds

( q = r & A \/ B = [.p,s.[ )

for p, q, r, s being R_eal st A = [.p,q.[ & B = [.r,s.[ & A misses B & A \/ B is Interval & not ( p = s & A \/ B = [.r,q.[ ) holds

( q = r & A \/ B = [.p,s.[ )

proof end;

theorem Th19: :: MEASUR12:19

for A, B being non empty Interval

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.] & A misses B holds

not A \/ B is Interval

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.] & A misses B holds

not A \/ B is Interval

proof end;

theorem Th20: :: MEASUR12:20

for A, B being non empty Interval

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.[ & A misses B & A \/ B is Interval holds

( p = s & A \/ B = ].r,q.[ )

for p, q, r, s being R_eal st A = [.p,q.[ & B = ].r,s.[ & A misses B & A \/ B is Interval holds

( p = s & A \/ B = ].r,q.[ )

proof end;

theorem Th21: :: MEASUR12:21

for A, B being non empty Interval

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.] & A misses B & A \/ B is Interval & not ( p = s & A \/ B = ].r,q.] ) holds

( q = r & A \/ B = ].p,s.] )

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.] & A misses B & A \/ B is Interval & not ( p = s & A \/ B = ].r,q.] ) holds

( q = r & A \/ B = ].p,s.] )

proof end;

theorem Th22: :: MEASUR12:22

for A, B being non empty Interval

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval holds

( q = r & A \/ B = ].p,s.[ )

for p, q, r, s being R_eal st A = ].p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval holds

( q = r & A \/ B = ].p,s.[ )

proof end;

theorem Th23: :: MEASUR12:23

for A, B being non empty Interval

for p, q, r, s being R_eal st A = ].p,q.[ & B = ].r,s.[ & A misses B holds

not A \/ B is Interval

for p, q, r, s being R_eal st A = ].p,q.[ & B = ].r,s.[ & A misses B holds

not A \/ B is Interval

proof end;

definition

let f be FinSequence of ExtREAL ;

ex b_{1} being Nat st

( ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) )

for b_{1}, b_{2} being Nat st ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) & ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) holds

b_{1} = b_{2}

end;
func max_p f -> Nat means :Def1: :: MEASUR12:def 1

( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . it holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds

it <= j ) ) ) );

existence ( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . it holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds

it <= j ) ) ) );

ex b

( ( len f = 0 implies b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

proof end;

uniqueness for b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

b

proof end;

:: deftheorem Def1 defines max_p MEASUR12:def 1 :

for f being FinSequence of ExtREAL

for b_{2} being Nat holds

( b_{2} = max_p f iff ( ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) ) );

for f being FinSequence of ExtREAL

for b

( b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

definition

let f be FinSequence of ExtREAL ;

ex b_{1} being Nat st

( ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) )

for b_{1}, b_{2} being Nat st ( len f = 0 implies b_{1} = 0 ) & ( len f > 0 implies ( b_{1} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{1} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{1} holds

b_{1} <= j ) ) ) & ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) holds

b_{1} = b_{2}

end;
func min_p f -> Nat means :Def2: :: MEASUR12:def 2

( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . it holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds

it <= j ) ) ) );

existence ( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . it holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . it holds

it <= j ) ) ) );

ex b

( ( len f = 0 implies b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

proof end;

uniqueness for b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

b

proof end;

:: deftheorem Def2 defines min_p MEASUR12:def 2 :

for f being FinSequence of ExtREAL

for b_{2} being Nat holds

( b_{2} = min_p f iff ( ( len f = 0 implies b_{2} = 0 ) & ( len f > 0 implies ( b_{2} in dom f & ( for i being Nat

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b_{2} holds

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b_{2} holds

b_{2} <= j ) ) ) ) );

for f being FinSequence of ExtREAL

for b

( b

for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b

r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b

b

definition

let f be FinSequence of ExtREAL ;

correctness

coherence

f . (max_p f) is ExtReal;

;

correctness

coherence

f . (min_p f) is ExtReal;

;

end;
correctness

coherence

f . (max_p f) is ExtReal;

;

correctness

coherence

f . (min_p f) is ExtReal;

;

:: deftheorem defines max MEASUR12:def 3 :

for f being FinSequence of ExtREAL holds max f = f . (max_p f);

for f being FinSequence of ExtREAL holds max f = f . (max_p f);

:: deftheorem defines min MEASUR12:def 4 :

for f being FinSequence of ExtREAL holds min f = f . (min_p f);

for f being FinSequence of ExtREAL holds min f = f . (min_p f);

theorem :: MEASUR12:25

for f being FinSequence of ExtREAL

for i being Nat st 1 <= i & i <= len f holds

( f . i <= f . (max_p f) & f . i <= max f )

for i being Nat st 1 <= i & i <= len f holds

( f . i <= f . (max_p f) & f . i <= max f )

proof end;

theorem Th26: :: MEASUR12:26

for f being FinSequence of ExtREAL

for i being Nat st 1 <= i & i <= len f holds

( f . i >= f . (min_p f) & f . i >= min f )

for i being Nat st 1 <= i & i <= len f holds

( f . i >= f . (min_p f) & f . i >= min f )

proof end;

theorem Th27: :: MEASUR12:27

for F being Function

for x, y being object st x in dom F & y in dom F holds

Swap (F,x,y) = F * (Swap ((id (dom F)),x,y))

for x, y being object st x in dom F & y in dom F holds

Swap (F,x,y) = F * (Swap ((id (dom F)),x,y))

proof end;

theorem Th28: :: MEASUR12:28

for F being Function

for x, y being object st x in dom F & y in dom F holds

F, Swap (F,x,y) are_fiberwise_equipotent

for x, y being object st x in dom F & y in dom F holds

F, Swap (F,x,y) are_fiberwise_equipotent

proof end;

theorem Th29: :: MEASUR12:29

for X being set

for F being Function

for x, y being object st not x in X & not y in X holds

F | X = (Swap (F,x,y)) | X

for F being Function

for x, y being object st not x in X & not y in X holds

F | X = (Swap (F,x,y)) | X

proof end;

REAL in bool REAL

by ZFMISC_1:def 1;

then reconsider G0 = NAT --> REAL as sequence of (bool REAL) by FUNCOP_1:45;

Lm5: rng G0 = {REAL}

by FUNCOP_1:8;

Lm6: for n being Element of NAT holds G0 . n is Interval

;

Lm7: REAL is open_interval Subset of REAL

proof end;

definition

let A be Subset of REAL;

ex b_{1} being Interval_Covering of A st

for n being Element of NAT holds b_{1} . n is open_interval

end;
mode Open_Interval_Covering of A -> Interval_Covering of A means :Def5: :: MEASUR12:def 5

for n being Element of NAT holds it . n is open_interval ;

existence for n being Element of NAT holds it . n is open_interval ;

ex b

for n being Element of NAT holds b

proof end;

:: deftheorem Def5 defines Open_Interval_Covering MEASUR12:def 5 :

for A being Subset of REAL

for b_{2} being Interval_Covering of A holds

( b_{2} is Open_Interval_Covering of A iff for n being Element of NAT holds b_{2} . n is open_interval );

for A being Subset of REAL

for b

( b

Lm8: for A being Subset of REAL holds G0 is Open_Interval_Covering of A

proof end;

definition

let A be Subset of REAL;

let F be Open_Interval_Covering of A;

let n be Element of NAT ;

:: original: .

redefine func F . n -> open_interval Subset of REAL;

correctness

coherence

F . n is open_interval Subset of REAL;

by Def5;

end;
let F be Open_Interval_Covering of A;

let n be Element of NAT ;

:: original: .

redefine func F . n -> open_interval Subset of REAL;

correctness

coherence

F . n is open_interval Subset of REAL;

by Def5;

definition

let F be sequence of (bool REAL);

ex b_{1} being Interval_Covering of F st

for n being Element of NAT holds b_{1} . n is Open_Interval_Covering of F . n

end;
mode Open_Interval_Covering of F -> Interval_Covering of F means :Def6: :: MEASUR12:def 6

for n being Element of NAT holds it . n is Open_Interval_Covering of F . n;

existence for n being Element of NAT holds it . n is Open_Interval_Covering of F . n;

ex b

for n being Element of NAT holds b

proof end;

:: deftheorem Def6 defines Open_Interval_Covering MEASUR12:def 6 :

for F being sequence of (bool REAL)

for b_{2} being Interval_Covering of F holds

( b_{2} is Open_Interval_Covering of F iff for n being Element of NAT holds b_{2} . n is Open_Interval_Covering of F . n );

for F being sequence of (bool REAL)

for b

( b

definition

let F be sequence of (bool REAL);

let H be Open_Interval_Covering of F;

let n be Element of NAT ;

:: original: .

redefine func H . n -> Open_Interval_Covering of F . n;

correctness

coherence

H . n is Open_Interval_Covering of F . n;

by Def6;

end;
let H be Open_Interval_Covering of F;

let n be Element of NAT ;

:: original: .

redefine func H . n -> Open_Interval_Covering of F . n;

correctness

coherence

H . n is Open_Interval_Covering of F . n;

by Def6;

definition

let A be Subset of REAL;

defpred S_{1}[ object ] means ex F being Open_Interval_Covering of A st $1 = vol F;

ex b_{1} being Subset of ExtREAL st

for x being R_eal holds

( x in b_{1} iff ex F being Open_Interval_Covering of A st x = vol F )

for b_{1}, b_{2} being Subset of ExtREAL st ( for x being R_eal holds

( x in b_{1} iff ex F being Open_Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds

( x in b_{2} iff ex F being Open_Interval_Covering of A st x = vol F ) ) holds

b_{1} = b_{2}

end;
defpred S

func Svc2 A -> Subset of ExtREAL means :Def7: :: MEASUR12:def 7

for x being R_eal holds

( x in it iff ex F being Open_Interval_Covering of A st x = vol F );

existence for x being R_eal holds

( x in it iff ex F being Open_Interval_Covering of A st x = vol F );

ex b

for x being R_eal holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines Svc2 MEASUR12:def 7 :

for A being Subset of REAL

for b_{2} being Subset of ExtREAL holds

( b_{2} = Svc2 A iff for x being R_eal holds

( x in b_{2} iff ex F being Open_Interval_Covering of A st x = vol F ) );

for A being Subset of REAL

for b

( b

( x in b

registration
end;

reconsider D = NAT --> ({} REAL) as sequence of (bool REAL) ;

theorem Th31: :: MEASUR12:31

for F being sequence of (bool REAL)

for G being Open_Interval_Covering of F

for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds

On (G,H) is Open_Interval_Covering of union (rng F)

for G being Open_Interval_Covering of F

for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds

On (G,H) is Open_Interval_Covering of union (rng F)

proof end;

theorem Th32: :: MEASUR12:32

for A being Subset of REAL

for G being sequence of (bool REAL) st A c= union (rng G) & ( for n being Element of NAT holds G . n is open_interval ) holds

G is Open_Interval_Covering of A

for G being sequence of (bool REAL) st A c= union (rng G) & ( for n being Element of NAT holds G . n is open_interval ) holds

G is Open_Interval_Covering of A

proof end;

theorem Th33: :: MEASUR12:33

for F being sequence of (bool REAL)

for G being sequence of (Funcs (NAT,(bool REAL))) st ( for n being Element of NAT holds G . n is Open_Interval_Covering of F . n ) holds

G is Open_Interval_Covering of F

for G being sequence of (Funcs (NAT,(bool REAL))) st ( for n being Element of NAT holds G . n is Open_Interval_Covering of F . n ) holds

G is Open_Interval_Covering of F

proof end;

theorem Th34: :: MEASUR12:34

for H being sequence of [:NAT,NAT:] st H is one-to-one & rng H = [:NAT,NAT:] holds

for k being Nat ex m being Element of NAT st

for F being sequence of (bool REAL)

for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m

for k being Nat ex m being Element of NAT st

for F being sequence of (bool REAL)

for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m

proof end;

theorem :: MEASUR12:35

for F being sequence of (bool REAL)

for G being Open_Interval_Covering of F holds inf (Svc2 (union (rng F))) <= SUM (vol G)

for G being Open_Interval_Covering of F holds inf (Svc2 (union (rng F))) <= SUM (vol G)

proof end;

definition

let F be non empty Subset-Family of REAL;

:: original: Element

redefine mode Element of F -> Subset of REAL;

coherence

for b_{1} being Element of F holds b_{1} is Subset of REAL

end;
:: original: Element

redefine mode Element of F -> Subset of REAL;

coherence

for b

proof end;

Lm9: for a1, b1 being Real

for a2, b2 being R_eal st a1 = a2 & b1 = b2 holds

a1 - b1 = a2 - b2

proof end;

theorem Th36: :: MEASUR12:36

for A being Element of Family_of_Intervals st A is open_interval holds

ex F being Open_Interval_Covering of A st

( F . 0 = A & ( for n being Nat st n <> 0 holds

F . n = {} ) & union (rng F) = A & SUM (F vol) = diameter A )

ex F being Open_Interval_Covering of A st

( F . 0 = A & ( for n being Nat st n <> 0 holds

F . n = {} ) & union (rng F) = A & SUM (F vol) = diameter A )

proof end;

theorem Th37: :: MEASUR12:37

for A, B being Subset of REAL

for F being Interval_Covering of A st B c= A holds

F is Interval_Covering of B

for F being Interval_Covering of A st B c= A holds

F is Interval_Covering of B

proof end;

theorem Th38: :: MEASUR12:38

for A, B being Subset of REAL

for F being Open_Interval_Covering of A st B c= A holds

F is Open_Interval_Covering of B

for F being Open_Interval_Covering of A st B c= A holds

F is Open_Interval_Covering of B

proof end;

theorem Th39: :: MEASUR12:39

for A, B being Subset of REAL

for F being Interval_Covering of A

for G being Interval_Covering of B st F = G holds

F vol = G vol

for F being Interval_Covering of A

for G being Interval_Covering of B st F = G holds

F vol = G vol

proof end;

theorem Th40: :: MEASUR12:40

for F being FinSequence of bool REAL

for k being Nat st ( for n being Nat st n in dom F holds

F . n is open_interval Subset of REAL ) & ( for n being Nat st 1 <= n & n < len F holds

union (rng (F | n)) meets F . (n + 1) ) holds

union (rng (F | k)) is open_interval Subset of REAL

for k being Nat st ( for n being Nat st n in dom F holds

F . n is open_interval Subset of REAL ) & ( for n being Nat st 1 <= n & n < len F holds

union (rng (F | n)) meets F . (n + 1) ) holds

union (rng (F | k)) is open_interval Subset of REAL

proof end;

theorem Th41: :: MEASUR12:41

for A being non empty closed_interval Subset of REAL

for F being FinSequence of bool REAL st A c= union (rng F) & ( for n being Nat st n in dom F holds

A meets F . n ) & ( for n being Nat st n in dom F holds

F . n is open_interval Subset of REAL ) holds

ex G being FinSequence of bool REAL st

( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len G holds

union (rng (G | n)) meets G . (n + 1) ) )

for F being FinSequence of bool REAL st A c= union (rng F) & ( for n being Nat st n in dom F holds

A meets F . n ) & ( for n being Nat st n in dom F holds

F . n is open_interval Subset of REAL ) holds

ex G being FinSequence of bool REAL st

( F,G are_fiberwise_equipotent & ( for n being Nat st 1 <= n & n < len G holds

union (rng (G | n)) meets G . (n + 1) ) )

proof end;

theorem Th43: :: MEASUR12:43

for I being Element of Family_of_Intervals st I <> {} & I is right_open_interval holds

OS_Meas . I <= diameter I

OS_Meas . I <= diameter I

proof end;

Lm10: for I being Element of Family_of_Intervals st I <> {} & I is left_open_interval holds

OS_Meas . I <= diameter I

proof end;

Lm11: for I being Element of Family_of_Intervals st I <> {} & I is closed_interval holds

OS_Meas . I <= diameter I

proof end;

Lm12: for A, B being Interval st A is open_interval & B is open_interval & A \/ B is Interval holds

diameter (A \/ B) <= (diameter A) + (diameter B)

proof end;

theorem Th45: :: MEASUR12:45

for A being non empty closed_interval Subset of REAL

for F being FinSequence of bool REAL

for G being FinSequence of ExtREAL st A c= union (rng F) & len F = len G & ( for n being Nat st n in dom F holds

F . n is open_interval Subset of REAL ) & ( for n being Nat st n in dom F holds

G . n = diameter (F . n) ) & ( for n being Nat st n in dom F holds

A meets F . n ) holds

diameter A <= Sum G

for F being FinSequence of bool REAL

for G being FinSequence of ExtREAL st A c= union (rng F) & len F = len G & ( for n being Nat st n in dom F holds

F . n is open_interval Subset of REAL ) & ( for n being Nat st n in dom F holds

G . n = diameter (F . n) ) & ( for n being Nat st n in dom F holds

A meets F . n ) holds

diameter A <= Sum G

proof end;

theorem Th46: :: MEASUR12:46

for X being non empty set

for f being sequence of X

for i, j being Nat ex g being sequence of X st

( ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) & f . i = g . j & f . j = g . i )

for f being sequence of X

for i, j being Nat ex g being sequence of X st

( ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) & f . i = g . j & f . j = g . i )

proof end;

theorem :: MEASUR12:47

for f, g being sequence of ExtREAL st f is V115() & ex N being Nat st

( (Ser f) . N <= (Ser g) . N & ( for n being Nat st n > N holds

f . n <= g . n ) ) holds

SUM f <= SUM g

( (Ser f) . N <= (Ser g) . N & ( for n being Nat st n > N holds

f . n <= g . n ) ) holds

SUM f <= SUM g

proof end;

theorem Th48: :: MEASUR12:48

for f, g being sequence of ExtREAL

for j, k being Nat st k < j & ( for n being Nat st n < j holds

f . n = g . n ) holds

(Ser f) . k = (Ser g) . k

for j, k being Nat st k < j & ( for n being Nat st n < j holds

f . n = g . n ) holds

(Ser f) . k = (Ser g) . k

proof end;

theorem Th49: :: MEASUR12:49

for f, g being sequence of ExtREAL

for i, j being Nat st f is V115() & i >= j & ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) & f . i = g . j & f . j = g . i holds

(Ser f) . i = (Ser g) . i

for i, j being Nat st f is V115() & i >= j & ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) & f . i = g . j & f . j = g . i holds

(Ser f) . i = (Ser g) . i

proof end;

theorem Th50: :: MEASUR12:50

for f, g being sequence of ExtREAL

for i, j being Nat st f is V115() & f . i = g . j & f . j = g . i & ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) holds

for n being Nat st n >= i & n >= j holds

(Ser f) . n = (Ser g) . n

for i, j being Nat st f is V115() & f . i = g . j & f . j = g . i & ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) holds

for n being Nat st n >= i & n >= j holds

(Ser f) . n = (Ser g) . n

proof end;

Lm13: for f, g being sequence of ExtREAL

for i, j being Nat st f is V115() & i >= j & ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) & f . i = g . j & f . j = g . i holds

SUM f <= SUM g

proof end;

theorem Th51: :: MEASUR12:51

for f, g being sequence of ExtREAL

for i, j being Nat st f is V115() & i >= j & ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) & f . i = g . j & f . j = g . i holds

SUM f = SUM g

for i, j being Nat st f is V115() & i >= j & ( for n being Nat st n <> i & n <> j holds

f . n = g . n ) & f . i = g . j & f . j = g . i holds

SUM f = SUM g

proof end;

theorem Th52: :: MEASUR12:52

for A being Subset of REAL

for F1, F2 being Interval_Covering of A

for n, m being Nat st ( for k being Nat st k <> n & k <> m holds

F1 . k = F2 . k ) & F1 . n = F2 . m & F1 . m = F2 . n holds

vol F1 = vol F2

for F1, F2 being Interval_Covering of A

for n, m being Nat st ( for k being Nat st k <> n & k <> m holds

F1 . k = F2 . k ) & F1 . n = F2 . m & F1 . m = F2 . n holds

vol F1 = vol F2

proof end;

theorem :: MEASUR12:53

for A being Subset of REAL

for F1, F2 being Interval_Covering of A

for n, m being Nat st ( for k being Nat st k <> n & k <> m holds

F1 . k = F2 . k ) & F1 . n = F2 . m & F1 . m = F2 . n holds

for k being Nat st k >= n & k >= m holds

(Ser (F1 vol)) . k = (Ser (F2 vol)) . k

for F1, F2 being Interval_Covering of A

for n, m being Nat st ( for k being Nat st k <> n & k <> m holds

F1 . k = F2 . k ) & F1 . n = F2 . m & F1 . m = F2 . n holds

for k being Nat st k >= n & k >= m holds

(Ser (F1 vol)) . k = (Ser (F2 vol)) . k

proof end;

theorem :: MEASUR12:54

for X being non empty set

for seq being sequence of X

for f being FinSequence of X st rng f c= rng seq holds

ex N being Nat st rng f c= rng (seq | (Segm N))

for seq being sequence of X

for f being FinSequence of X st rng f c= rng seq holds

ex N being Nat st rng f c= rng (seq | (Segm N))

proof end;

theorem Th55: :: MEASUR12:55

for A being non empty Subset of REAL

for F being Interval_Covering of A

for G being one-to-one FinSequence of bool REAL st rng G c= rng F holds

ex F1 being Interval_Covering of A st

( ( for n being Nat st n in dom G holds

G . n = F1 . n ) & vol F1 = vol F )

for F being Interval_Covering of A

for G being one-to-one FinSequence of bool REAL st rng G c= rng F holds

ex F1 being Interval_Covering of A st

( ( for n being Nat st n in dom G holds

G . n = F1 . n ) & vol F1 = vol F )

proof end;

theorem Th56: :: MEASUR12:56

for A being non empty Subset of REAL

for F being Interval_Covering of A

for G being one-to-one FinSequence of bool REAL

for H being FinSequence of ExtREAL st rng G c= rng F & dom G = dom H & ( for n being Nat holds H . n = diameter (G . n) ) holds

Sum H <= vol F

for F being Interval_Covering of A

for G being one-to-one FinSequence of bool REAL

for H being FinSequence of ExtREAL st rng G c= rng F & dom G = dom H & ( for n being Nat holds H . n = diameter (G . n) ) holds

Sum H <= vol F

proof end;

Lm14: for I being Element of Family_of_Intervals st not I is empty & I is closed_interval holds

diameter I <= OS_Meas . I

proof end;

Lm15: for I being Element of Family_of_Intervals st not I is empty & I is open_interval & diameter I < +infty holds

diameter I <= OS_Meas . I

proof end;

Lm16: for I being Element of Family_of_Intervals st not I is empty & I is left_open_interval & diameter I < +infty holds

diameter I <= OS_Meas . I

proof end;

Lm17: for I being Element of Family_of_Intervals st not I is empty & I is right_open_interval & diameter I < +infty holds

diameter I <= OS_Meas . I

proof end;

Lm18: for a, b being Real st a <= b holds

diameter [.a,b.] = b - a

proof end;

Lm19: for I being Element of Family_of_Intervals holds

( not diameter I = +infty or sup I = +infty or inf I = -infty )

proof end;

Lm20: for I being non empty closed_interval Subset of REAL holds diameter I = OS_Meas . I

proof end;

Lm21: for I being Element of Family_of_Intervals st diameter I = +infty holds

diameter I <= OS_Meas . I

proof end;

Lm22: for I being Interval holds diameter I <= OS_Meas . I

proof end;

definition

let F be FinSequence of Family_of_Intervals ;

let n be Nat;

:: original: .

redefine func F . n -> interval Subset of REAL;

correctness

coherence

F . n is interval Subset of REAL;

end;
let n be Nat;

:: original: .

redefine func F . n -> interval Subset of REAL;

correctness

coherence

F . n is interval Subset of REAL;

proof end;

definition

coherence

OS_Meas | Family_of_Intervals is zeroed V115() Function of Family_of_Intervals,ExtREAL;

end;

func pre-Meas -> zeroed V115() Function of Family_of_Intervals,ExtREAL equals :: MEASUR12:def 8

OS_Meas | Family_of_Intervals;

correctness OS_Meas | Family_of_Intervals;

coherence

OS_Meas | Family_of_Intervals is zeroed V115() Function of Family_of_Intervals,ExtREAL;

proof end;

theorem Th60: :: MEASUR12:60

for A, B being Element of Family_of_Intervals st A misses B & A \/ B is Interval holds

pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)

pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)

proof end;

theorem Th61: :: MEASUR12:61

for F being non empty disjoint_valued FinSequence of Family_of_Intervals st Union F is Interval holds

ex n being Nat st

( n in dom F & (Union F) \ (F . n) is Interval )

ex n being Nat st

( n in dom F & (Union F) \ (F . n) is Interval )

proof end;

theorem Th63: :: MEASUR12:63

for F being disjoint_valued FinSequence of Family_of_Intervals st Union F in Family_of_Intervals holds

ex G being disjoint_valued FinSequence of Family_of_Intervals st

( F,G are_fiberwise_equipotent & ( for n being Nat st n in dom G holds

( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) ) )

ex G being disjoint_valued FinSequence of Family_of_Intervals st

( F,G are_fiberwise_equipotent & ( for n being Nat st n in dom G holds

( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) ) )

proof end;

theorem Th64: :: MEASUR12:64

for F, G being FinSequence of ExtREAL holds

( ( F is V339() & G is V339() implies F ^ G is V339() ) & ( F is V340() & G is V340() implies F ^ G is V340() ) )

( ( F is V339() & G is V339() implies F ^ G is V339() ) & ( F is V340() & G is V340() implies F ^ G is V340() ) )

proof end;

theorem Th65: :: MEASUR12:65

for F being FinSequence of ExtREAL

for k being Nat holds

( ( F is V339() implies F /^ k is V339() ) & ( F is V340() implies F /^ k is V340() ) )

for k being Nat holds

( ( F is V339() implies F /^ k is V339() ) & ( F is V340() implies F /^ k is V340() ) )

proof end;

theorem Th66: :: MEASUR12:66

for F being FinSequence of ExtREAL holds

( ( F is V339() implies Sum F <> -infty ) & ( F is V340() implies Sum F <> +infty ) )

( ( F is V339() implies Sum F <> -infty ) & ( F is V340() implies Sum F <> +infty ) )

proof end;

theorem Th67: :: MEASUR12:67

for R1, R2 being V339() FinSequence of ExtREAL st R1,R2 are_fiberwise_equipotent holds

Sum R1 = Sum R2

Sum R1 = Sum R2

proof end;

theorem Th68: :: MEASUR12:68

for F being disjoint_valued FinSequence of Family_of_Intervals st Union F in Family_of_Intervals holds

pre-Meas . (Union F) = Sum (pre-Meas * F)

pre-Meas . (Union F) = Sum (pre-Meas * F)

proof end;

theorem Th69: :: MEASUR12:69

for K being disjoint_valued Function of NAT,Family_of_Intervals st Union K in Family_of_Intervals holds

pre-Meas . (Union K) <= SUM (pre-Meas * K)

pre-Meas . (Union K) <= SUM (pre-Meas * K)

proof end;

definition

:: original: pre-Meas

redefine func pre-Meas -> pre-Measure of Family_of_Intervals ;

correctness

coherence

pre-Meas is pre-Measure of Family_of_Intervals ;

by Th68, Th69, MEASURE9:def 7;

end;
redefine func pre-Meas -> pre-Measure of Family_of_Intervals ;

correctness

coherence

pre-Meas is pre-Measure of Family_of_Intervals ;

by Th68, Th69, MEASURE9:def 7;

definition

ex b_{1} being Measure of (Field_generated_by Family_of_Intervals) st

for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b_{1} . A = Sum (pre-Meas * F)
by MEASURE9:55;

uniqueness

for b_{1}, b_{2} being Measure of (Field_generated_by Family_of_Intervals) st ( for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b_{1} . A = Sum (pre-Meas * F) ) & ( for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b_{2} . A = Sum (pre-Meas * F) ) holds

b_{1} = b_{2}
end;

func J-Meas -> Measure of (Field_generated_by Family_of_Intervals) means :Def9: :: MEASUR12:def 9

for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

it . A = Sum (pre-Meas * F);

existence for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

it . A = Sum (pre-Meas * F);

ex b

for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b

uniqueness

for b

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b

b

proof end;

:: deftheorem Def9 defines J-Meas MEASUR12:def 9 :

for b_{1} being Measure of (Field_generated_by Family_of_Intervals) holds

( b_{1} = J-Meas iff for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b_{1} . A = Sum (pre-Meas * F) );

for b

( b

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

b

Lm23: for A being set st A in Field_generated_by Family_of_Intervals holds

for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds

J-Meas . A = Sum (pre-Meas * F)

by Def9;

definition

:: original: J-Meas

redefine func J-Meas -> induced_Measure of Family_of_Intervals , pre-Meas ;

correctness

coherence

J-Meas is induced_Measure of Family_of_Intervals , pre-Meas ;

by Lm23, MEASURE9:def 8;

end;
redefine func J-Meas -> induced_Measure of Family_of_Intervals , pre-Meas ;

correctness

coherence

J-Meas is induced_Measure of Family_of_Intervals , pre-Meas ;

by Lm23, MEASURE9:def 8;

registration
end;

definition

coherence

(sigma_Meas (C_Meas J-Meas)) | Borel_Sets is sigma_Measure of Borel_Sets;

by MEASURE9:61, MEASUR10:6;

end;

func B-Meas -> sigma_Measure of Borel_Sets equals :: MEASUR12:def 10

(sigma_Meas (C_Meas J-Meas)) | Borel_Sets;

correctness (sigma_Meas (C_Meas J-Meas)) | Borel_Sets;

coherence

(sigma_Meas (C_Meas J-Meas)) | Borel_Sets is sigma_Measure of Borel_Sets;

by MEASURE9:61, MEASUR10:6;

registration
end;