let X be set ;
let IT be Subset-Family of X;
canceled;
canceled;
redefine attr IT is compl-closed means :Def3: :: MEASURE1:def 3
for A being set st A in IT holds
X \ A in IT;
compatibility

proof end;

end;

:: deftheorem MEASURE1:def 1 :

:: deftheorem MEASURE1:def 2 :

:: deftheorem Def3 defines compl-closed MEASURE1:def 3 :

theorem Th16: :: MEASURE1:16

for X being set
for F being Subset-Family of X st F is cup-closed & F is compl-closed holds
F is cap-closed

proof end;

registration

let X be set ;
cluster cup-closed compl-closed -> cap-closed Element of bool (bool X);
coherence by Th16;
cluster cap-closed compl-closed -> cup-closed Element of bool (bool X);
coherence

proof end;

end;

theorem Th17: :: MEASURE1:17

for X being set
for S being Field_Subset of X holds S = X \ S

proof end;

theorem :: MEASURE1:18

for X, M being set holds
( M is Field_Subset of X iff ex S being non empty Subset-Family of X st
( M = S & ( for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A \/ B in S ) ) ) ) )

proof end;

theorem Th19: :: MEASURE1:19

for X being set
for S being non empty Subset-Family of X holds
( S is Field_Subset of X iff for A being set st A in S holds
( X \ A in S & ( for A, B being set st A in S & B in S holds
A /\ B in S ) ) )

proof end;

theorem Th20: :: MEASURE1:20

for X being set
for S being Field_Subset of X
for A, B being set st A in S & B in S holds
A \ B in S

proof end;

theorem :: MEASURE1:21

for X being set
for S being Field_Subset of X holds
( {} in S & X in S ) by PROB_1:10, PROB_1:11;

definition

let S be non empty set ;
let F be Function of S, ExtREAL ;
let A be Element of S;
:: original: .
redefine func F . A -> R_eal;
coherence by FUNCT_2:7;

end;

definition

let X be non empty set ;
let F be Function of X, ExtREAL ;
redefine attr F is nonnegative means :Def4: :: MEASURE1:def 4
for A being Element of X holds 0. <=' F . A;
compatibility by SUPINF_2:58;

end;

:: deftheorem Def4 defines nonnegative MEASURE1:def 4 :

theorem :: MEASURE1:22

canceled;

theorem Th23: :: MEASURE1:23

for X being set
for S being Field_Subset of X ex M being Function of S, ExtREAL st
( M is nonnegative & M . {} = 0. & ( for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B) ) )

proof end;

definition

let X be set ;
let S be Field_Subset of X;
mode Measure of S -> Function of S, ExtREAL means :Def5: :: MEASURE1:def 5
( it is nonnegative & it . {} = 0. & ( for A, B being Element of S st A misses B holds
it . (A \/ B) = (it . A) + (it . B) ) );
existence by Th23;

end;

:: deftheorem Def5 defines Measure MEASURE1:def 5 :

theorem :: MEASURE1:24

canceled;

theorem Th25: :: MEASURE1:25

for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B holds
M . A <=' M . B

proof end;

theorem Th26: :: MEASURE1:26

for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B & M . A <' +infty holds
M . (B \ A) = (M . B) - (M . A)

proof end;

registration

let X be set ;
cluster non empty cup-closed cap-closed compl-closed Element of bool (bool X);
existence

proof end;

end;

definition

let X be set ;
let S be non empty cup-closed Subset-Family of X;
let A, B be Element of S;
:: original: \/
redefine func A \/ B -> Element of S;
coherence by FINSUB_1:def 1;

end;

definition

let X be set ;
let S be Field_Subset of X;
let A, B be Element of S;
:: original: /\
redefine func A /\ B -> Element of S;
coherence by Th19;
:: original: \
redefine func A \ B -> Element of S;
coherence by Th20;

end;

theorem Th27: :: MEASURE1:27

for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S holds M . (A \/ B) <=' (M . A) + (M . B)

proof end;

definition

let X be set ;
let S be Field_Subset of X;
let M be Measure of S;
let A be set ;
pred A is_measurable M means :Def6: :: MEASURE1:def 6
A in S;

end;

:: deftheorem Def6 defines is_measurable MEASURE1:def 6 :

theorem :: MEASURE1:28

canceled;

theorem :: MEASURE1:29

for X being set
for S being Field_Subset of X
for M being Measure of S holds
( {} is_measurable M & X is_measurable M & ( for A, B being set st A is_measurable M & B is_measurable M holds
( X \ A is_measurable M & A \/ B is_measurable M & A /\ B is_measurable M ) ) )

proof end;

definition

let X be set ;
let S be Field_Subset of X;
let M be Measure of S;
mode measure_zero of M -> Element of S means :Def7: :: MEASURE1:def 7
M . it = 0. ;
existence

proof end;

end;

:: deftheorem Def7 defines measure_zero MEASURE1:def 7 :

theorem :: MEASURE1:30

canceled;

theorem :: MEASURE1:31

for X being set
for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M

proof end;

theorem :: MEASURE1:32

for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )

proof end;

theorem :: MEASURE1:33

for X being set
for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )

proof end;

theorem Th34: :: MEASURE1:34

for X being set
for A being Subset of X ex F being Function of NAT , bool X st rng F = {A}

proof end;

theorem Th35: :: MEASURE1:35

for A being set ex F being Function of NAT ,{A} st
for n being Nat holds F . n = A

proof end;

registration

let X be set ;
cluster non empty countable Element of bool (bool X);
existence

proof end;

end;

definition

let X be set ;
mode N_Sub_set_fam of X is non empty countable Subset-Family of X;

end;

theorem :: MEASURE1:36

canceled;

theorem :: MEASURE1:37

canceled;

theorem Th38: :: MEASURE1:38

for X being set
for A, B, C being Subset of X ex F being Function of NAT , bool X st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Nat st 1 < n holds
F . n = C ) )

proof end;

theorem :: MEASURE1:39

for X being set
for A, B being Subset of X holds {A,B,{} } is N_Sub_set_fam of X

proof end;

theorem Th40: :: MEASURE1:40

for X being set
for A, B being Subset of X ex F being Function of NAT , bool X st
( rng F = {A,B} & F . 0 = A & ( for n being Nat st 0 < n holds
F . n = B ) )

proof end;

theorem Th41: :: MEASURE1:41

for X being set
for A, B being Subset of X holds {A,B} is N_Sub_set_fam of X

proof end;

theorem Th42: :: MEASURE1:42

for X being set
for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X

proof end;

definition

let X be set ;
let IT be Subset-Family of X;
canceled;
attr IT is sigma_Field_Subset-like means :Def9: :: MEASURE1:def 9
for M being N_Sub_set_fam of X st M c= IT holds
union M in IT;

end;

:: deftheorem MEASURE1:def 8 :

:: deftheorem Def9 defines sigma_Field_Subset-like MEASURE1:def 9 :

registration

let X be set ;
cluster non empty compl-closed sigma_Field_Subset-like Element of bool (bool X);
existence

proof end;

end;

definition

let X be set ;
mode sigma_Field_Subset of X is non empty compl-closed sigma_Field_Subset-like Subset-Family of X;

end;

Lm1: for X being set
for S being non empty Subset-Family of X st S is sigma_Field_Subset of X holds
S is Field_Subset of X

proof end;

theorem :: MEASURE1:43

canceled;

theorem :: MEASURE1:44

canceled;

theorem Th45: :: MEASURE1:45

for X being set
for S being sigma_Field_Subset of X holds
( {} in S & X in S )

proof end;

registration

let X be set ;
cluster -> Element of bool (bool X);
coherence ;

end;

theorem Th46: :: MEASURE1:46

for X being set
for S being sigma_Field_Subset of X
for A, B being set st A in S & B in S holds
( A \/ B in S & A /\ B in S )

proof end;

theorem Th47: :: MEASURE1:47

for X being set
for S being sigma_Field_Subset of X
for A, B being set st A in S & B in S holds
A \ B in S

proof end;

theorem :: MEASURE1:48

for X being set
for S being sigma_Field_Subset of X holds S = X \ S

proof end;

theorem Th49: :: MEASURE1:49

for X being set
for S being non empty Subset-Family of X holds
( ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is sigma_Field_Subset of X )

proof end;

registration

let X be set ;
let S be sigma_Field_Subset of X;
cluster disjoint_valued M8( NAT ,S);
existence

proof end;

end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
mode Sep_Sequence of S is disjoint_valued Function of NAT ,S;

end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
let F be Function of NAT ,S;
:: original: rng
redefine func rng F -> non empty Subset-Family of X;
coherence

proof end;

end;

theorem :: MEASURE1:50

canceled;

theorem :: MEASURE1:51

canceled;

theorem Th52: :: MEASURE1:52

for X being set
for S being sigma_Field_Subset of X
for F being Function of NAT ,S holds rng F is N_Sub_set_fam of X

proof end;

theorem Th53: :: MEASURE1:53

for X being set
for S being sigma_Field_Subset of X
for F being Function of NAT ,S holds union (rng F) is Element of S

proof end;

theorem Th54: :: MEASURE1:54

for Y, S being non empty set
for F being Function of Y,S
for M being Function of S, ExtREAL st M is nonnegative holds
M * F is nonnegative

proof end;

theorem Th55: :: MEASURE1:55

for X being set
for S being sigma_Field_Subset of X
for a, b being R_eal ex M being Function of S, ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

proof end;

theorem :: MEASURE1:56

for X being set
for S being sigma_Field_Subset of X ex M being Function of S, ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = 0. ) & ( A <> {} implies M . A = +infty ) ) by Th55;

theorem Th57: :: MEASURE1:57

for X being set
for S being sigma_Field_Subset of X ex M being Function of S, ExtREAL st
for A being Element of S holds M . A = 0.

proof end;

theorem Th58: :: MEASURE1:58

for X being set
for S being sigma_Field_Subset of X ex M being Function of S, ExtREAL st
( M is nonnegative & M . {} = 0. & ( for F being Sep_Sequence of S holds SUM (M * F) = M . (union (rng F)) ) )

proof end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
canceled;
mode sigma_Measure of S -> Function of S, ExtREAL means :Def11: :: MEASURE1:def 11
( it is nonnegative & it . {} = 0. & ( for F being Sep_Sequence of S holds SUM (it * F) = it . (union (rng F)) ) );
existence by Th58;

end;

:: deftheorem MEASURE1:def 10 :

:: deftheorem Def11 defines sigma_Measure MEASURE1:def 11 :

registration

let X be set ;
cluster non empty compl-closed sigma_Field_Subset-like -> non empty cup-closed Element of bool (bool X);
coherence by Lm1;

end;

theorem :: MEASURE1:59

canceled;

theorem Th60: :: MEASURE1:60

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S holds M is Measure of S

proof end;

theorem :: MEASURE1:61

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)

proof end;

theorem Th62: :: MEASURE1:62

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B holds
M . A <=' M . B

proof end;

theorem :: MEASURE1:63

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B & M . A <' +infty holds
M . (B \ A) = (M . B) - (M . A)

proof end;

theorem Th64: :: MEASURE1:64

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for A, B being Element of S holds M . (A \/ B) <=' (M . A) + (M . B)

proof end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
let A be set ;
pred A is_measurable M means :Def12: :: MEASURE1:def 12
A in S;

end;

:: deftheorem Def12 defines is_measurable MEASURE1:def 12 :

theorem :: MEASURE1:65

canceled;

theorem :: MEASURE1:66

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S holds
( {} is_measurable M & X is_measurable M & ( for A, B being set st A is_measurable M & B is_measurable M holds
( X \ A is_measurable M & A \/ B is_measurable M & A /\ B is_measurable M ) ) )

proof end;

theorem :: MEASURE1:67

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for T being N_Sub_set_fam of X st ( for A being set st A in T holds
A is_measurable M ) holds
( union T is_measurable M & meet T is_measurable M )

proof end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
mode measure_zero of M -> Element of S means :Def13: :: MEASURE1:def 13
M . it = 0. ;
existence

proof end;

end;

:: deftheorem Def13 defines measure_zero MEASURE1:def 13 :

theorem :: MEASURE1:68

canceled;

theorem :: MEASURE1:69

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M

proof end;

theorem :: MEASURE1:70

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )

proof end;

theorem :: MEASURE1:71

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )

proof end;