:: Reconstruction of the One-Dimensional Lebesgue Measure
:: 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 ) )
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
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
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
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
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
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
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
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
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
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
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
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
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
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.] )
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.] )
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.[ )
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.[ )
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
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.[ )
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.] )
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.[ )
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
proof end;

theorem Th24: :: MEASUR12:24
for a, b being Real
for I being Subset of R^1 st I = [.a,b.] holds
I is compact
proof end;

definition
let f be FinSequence of ExtREAL ;
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
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof end;
uniqueness
for b1, b2 being Nat st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines max_p MEASUR12:def 1 :
for f being FinSequence of ExtREAL
for b2 being Nat holds
( b2 = max_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );

definition
let f be FinSequence of ExtREAL ;
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
ex b1 being Nat st
( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) )
proof end;
uniqueness
for b1, b2 being Nat st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b1 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b1 holds
b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines min_p MEASUR12:def 2 :
for f being FinSequence of ExtREAL
for b2 being Nat holds
( b2 = min_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b2 holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b2 holds
b2 <= j ) ) ) ) );

definition
let f be FinSequence of ExtREAL ;
func max f -> ExtReal equals :: MEASUR12:def 3
f . (max_p f);
correctness
coherence
f . (max_p f) is ExtReal;
;
func min f -> ExtReal equals :: MEASUR12:def 4
f . (min_p f);
correctness
coherence
f . (min_p f) is ExtReal;
;
end;

:: deftheorem defines max MEASUR12:def 3 :
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);

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 )
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 )
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))
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
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
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;
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
ex b1 being Interval_Covering of A st
for n being Element of NAT holds b1 . n is open_interval
proof end;
end;

:: deftheorem Def5 defines Open_Interval_Covering MEASUR12:def 5 :
for A being Subset of REAL
for b2 being Interval_Covering of A holds
( b2 is Open_Interval_Covering of A iff for n being Element of NAT holds b2 . n is open_interval );

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;

definition
let F be sequence of (bool REAL);
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
ex b1 being Interval_Covering of F st
for n being Element of NAT holds b1 . n is Open_Interval_Covering of F . n
proof end;
end;

:: deftheorem Def6 defines Open_Interval_Covering MEASUR12:def 6 :
for F being sequence of (bool REAL)
for b2 being Interval_Covering of F holds
( b2 is Open_Interval_Covering of F iff for n being Element of NAT holds b2 . n is Open_Interval_Covering of F . n );

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;

definition
let A be Subset of REAL;
defpred S1[ object ] means ex F being Open_Interval_Covering of A st $1 = vol F;
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
ex b1 being Subset of ExtREAL st
for x being R_eal holds
( x in b1 iff ex F being Open_Interval_Covering of A st x = vol F )
proof end;
uniqueness
for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds
( x in b1 iff ex F being Open_Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in b2 iff ex F being Open_Interval_Covering of A st x = vol F ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Svc2 MEASUR12:def 7 :
for A being Subset of REAL
for b2 being Subset of ExtREAL holds
( b2 = Svc2 A iff for x being R_eal holds
( x in b2 iff ex F being Open_Interval_Covering of A st x = vol F ) );

registration
let A be Subset of REAL;
cluster Svc2 A -> non empty ;
coherence
not Svc2 A is empty
proof end;
end;

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

theorem Th30: :: MEASUR12:30
for A being Subset of REAL holds
( Svc2 A c= Svc A & inf (Svc A) <= inf (Svc2 A) )
proof end;

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)
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
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
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
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)
proof end;

definition
let F be non empty Subset-Family of REAL;
:: original: Element
redefine mode Element of F -> Subset of REAL;
coherence
for b1 being Element of F holds b1 is Subset of REAL
proof end;
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 )
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
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
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
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
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) ) )
proof end;

theorem Th42: :: MEASUR12:42
for I being Element of Family_of_Intervals st I is open_interval holds
OS_Meas . I <= diameter I
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
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;

theorem Th44: :: MEASUR12:44
for I being Element of Family_of_Intervals st I is 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
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 )
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
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
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
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
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
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
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
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))
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 )
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
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;

theorem Th57: :: MEASUR12:57
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;
proof end;
end;

definition
func pre-Meas -> zeroed V115() Function of Family_of_Intervals,ExtREAL equals :: MEASUR12:def 8
OS_Meas | Family_of_Intervals;
correctness
coherence
OS_Meas | Family_of_Intervals is zeroed V115() Function of Family_of_Intervals,ExtREAL;
proof end;
end;

:: deftheorem defines pre-Meas MEASUR12:def 8 :
pre-Meas = OS_Meas | Family_of_Intervals;

theorem Th58: :: MEASUR12:58
for I being Element of Family_of_Intervals holds pre-Meas . I = diameter I
proof end;

theorem Th59: :: MEASUR12:59
for I being Interval holds pre-Meas . I = diameter I
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)
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 )
proof end;

theorem Th62: :: MEASUR12:62
for A being Interval holds pre-Meas * <*A*> = <*(pre-Meas . A)*>
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)) ) ) )
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() ) )
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() ) )
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 ) )
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
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)
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)
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;

definition
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
ex b1 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
b1 . A = Sum (pre-Meas * F) by MEASURE9:55;
uniqueness
for b1, b2 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
b1 . 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
b2 . A = Sum (pre-Meas * F) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines J-Meas MEASUR12:def 9 :
for b1 being Measure of (Field_generated_by Family_of_Intervals) holds
( b1 = 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
b1 . A = Sum (pre-Meas * F) );

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;

registration
cluster J-Meas -> completely-additive ;
coherence
J-Meas is completely-additive by MEASURE9:60;
end;

definition
func B-Meas -> sigma_Measure of Borel_Sets equals :: MEASUR12:def 10
(sigma_Meas (C_Meas J-Meas)) | Borel_Sets;
correctness
coherence
(sigma_Meas (C_Meas J-Meas)) | Borel_Sets is sigma_Measure of Borel_Sets;
by MEASURE9:61, MEASUR10:6;
end;

:: deftheorem defines B-Meas MEASUR12:def 10 :
B-Meas = (sigma_Meas (C_Meas J-Meas)) | Borel_Sets;

theorem Th71: :: MEASUR12:70
for A being Interval holds J-Meas . A = diameter A
proof end;

theorem Th72: :: MEASUR12:71
for A being Interval holds B-Meas . A = diameter A
proof end;

theorem Th73: :: MEASUR12:72
for A being Interval holds A in Borel_Sets
proof end;

definition
func L-Field -> SigmaField of REAL equals :: MEASUR12:def 11
 COM (Borel_Sets,B-Meas);
correctness
coherence
COM (Borel_Sets,B-Meas) is SigmaField of REAL;
;
end;

:: deftheorem defines L-Field MEASUR12:def 11 :
L-Field = COM (Borel_Sets,B-Meas);

definition
func L-Meas -> sigma_Measure of L-Field equals :: MEASUR12:def 12
 COM B-Meas;
correctness
coherence
COM B-Meas is sigma_Measure of L-Field;
;
end;

:: deftheorem defines L-Meas MEASUR12:def 12 :
L-Meas = COM B-Meas;

registration
cluster L-Meas -> complete ;
correctness
coherence
L-Meas is complete ;
proof end;
end;

theorem Th75: :: MEASUR12:73
{} is thin of B-Meas
proof end;

theorem :: MEASUR12:74
for a being Real holds {a} is thin of B-Meas
proof end;

theorem :: MEASUR12:75
Borel_Sets c= L-Field
proof end;

theorem :: MEASUR12:76
for A being Interval holds L-Meas . A = diameter A
proof end;