:: 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 b₁ being Nat st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) & ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= j ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines max_p MEASUR12:def 1 :
for f being FinSequence of ExtREAL
for b₂ being Nat holds
( b₂ = max_p f iff ( ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 <= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= 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 b₁ being Nat st
( ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ( len f = 0 implies b₁ = 0 ) & ( len f > 0 implies ( b₁ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₁ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₁ holds
b₁ <= j ) ) ) & ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= j ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines min_p MEASUR12:def 2 :
for f being FinSequence of ExtREAL
for b₂ being Nat holds
( b₂ = min_p f iff ( ( len f = 0 implies b₂ = 0 ) & ( len f > 0 implies ( b₂ in dom f & ( for i being Nat
for r1, r2 being ExtReal st i in dom f & r1 = f . i & r2 = f . b₂ holds
r1 >= r2 ) & ( for j being Nat st j in dom f & f . j = f . b₂ holds
b₂ <= 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 b₁ being Interval_Covering of A st
for n being Element of NAT holds b₁ . n is open_interval

proof end;

end;

:: deftheorem Def5 defines Open_Interval_Covering MEASUR12:def 5 :
for A being Subset of REAL
for b₂ being Interval_Covering of A holds
( b₂ is Open_Interval_Covering of A iff for n being Element of NAT holds b₂ . 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 b₁ being Interval_Covering of F st
for n being Element of NAT holds b₁ . 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 b₂ being Interval_Covering of F holds
( b₂ is Open_Interval_Covering of F iff for n being Element of NAT holds b₂ . 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 S₁[ 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 b₁ being Subset of ExtREAL st
for x being R_eal holds
( x in b₁ iff ex F being Open_Interval_Covering of A st x = vol F )

proof end;

uniqueness
for b₁, b₂ being Subset of ExtREAL st ( for x being R_eal holds
( x in b₁ iff ex F being Open_Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in b₂ iff ex F being Open_Interval_Covering of A st x = vol F ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Svc2 MEASUR12:def 7 :
for A being Subset of REAL
for b₂ being Subset of ExtREAL holds
( b₂ = Svc2 A iff for x being R_eal holds
( x in b₂ 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 b₁ being Element of F holds b₁ 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 b₁ 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₁ . A = Sum (pre-Meas * F) by MEASURE9:55;
uniqueness
for b₁, b₂ 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₁ . 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₂ . A = Sum (pre-Meas * F) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines J-Meas MEASUR12:def 9 :
for b₁ being Measure of (Field_generated_by Family_of_Intervals) holds
( b₁ = 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₁ . 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;