measure1.miz



    begin

    reserve X for set;

    theorem :: MEASURE1:1

    

     Th1: for X,Y be set holds ( union {X, Y, {} }) = ( union {X, Y})

    proof

      let X,Y be set;

      

      thus ( union {X, Y, {} }) = ( union ( {X, Y} \/ { {} })) by ENUMSET1: 3

      .= (( union {X, Y}) \/ ( union { {} })) by ZFMISC_1: 78

      .= (( union {X, Y}) \/ {} ) by ZFMISC_1: 25

      .= ( union {X, Y});

    end;

    theorem :: MEASURE1:2

    for A,B be Subset of X holds {A, B} is Subset-Family of X

    proof

      let A,B be Subset of X;

      set C = {A, B};

      C c= ( bool X)

      proof

        let x be object;

        assume x in C;

        then x = A or x = B by TARSKI:def 2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MEASURE1:3

    for A,B,C be Subset of X holds {A, B, C} is Subset-Family of X

    proof

      let A,B,C be Subset of X;

      set D = {A, B, C};

      D c= ( bool X)

      proof

        let x be object;

        assume x in D;

        then x = A or x = B or x = C by ENUMSET1:def 1;

        hence thesis;

      end;

      hence thesis;

    end;

    scheme :: MEASURE1:sch1

    DomsetFamEx { A() -> set , P[ set] } :

ex F be non empty Subset-Family of A() st for B be set holds B in F iff B c= A() & P[B]

      provided

       A1: ex B be set st B c= A() & P[B];

      defpred X[ set] means ex Z be set st $1 = Z & P[Z];

      consider X be set such that

       A2: for x be set holds x in X iff x in ( bool A()) & X[x] from XFAMILY:sch 1;

      X c= ( bool A()) by A2;

      then

      reconsider X as non empty Subset-Family of A() by A1, A2;

      take X;

      for B be set holds B in X iff B c= A() & P[B]

      proof

        let B be set;

        thus B in X implies B c= A() & P[B]

        proof

          assume

           A3: B in X;

          then ex Z be set st B = Z & P[Z] by A2;

          hence thesis by A3;

        end;

        assume B c= A() & P[B];

        hence thesis by A2;

      end;

      hence thesis;

    end;

    notation

      let X be set;

      let S be non empty Subset-Family of X;

      synonym X \ S for COMPLEMENT S;

    end

    registration

      let X be set;

      let S be non empty Subset-Family of X;

      cluster (X \ S) -> non empty;

      coherence

      proof

        consider x be Subset of X such that

         A1: x in S by SUBSET_1: 4;

        ((x ` ) ` ) in S by A1;

        hence thesis by SETFAM_1:def 7;

      end;

    end

    theorem :: MEASURE1:4

    

     Th4: for S be non empty Subset-Family of X holds ( meet S) = (X \ ( union (X \ S))) & ( union S) = (X \ ( meet (X \ S)))

    proof

      let S be non empty Subset-Family of X;

      

       A1: (X \ ( union (X \ S))) c= ( meet S)

      proof

        let x be object;

        assume

         A2: x in (X \ ( union (X \ S)));

        then

         A3: not x in ( union (X \ S)) by XBOOLE_0:def 5;

        for Y be set st Y in S holds x in Y

        proof

          let Y be set;

          assume that

           A4: Y in S and

           A5: not x in Y;

          reconsider Y as Subset of X by A4;

          ((Y ` ) ` ) in S by A4;

          then

           A6: (Y ` ) in (X \ S) by SETFAM_1:def 7;

          x in (Y ` ) by A2, A5, SUBSET_1: 29;

          hence contradiction by A3, A6, TARSKI:def 4;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      ( meet S) c= (X \ ( union (X \ S)))

      proof

        let x be object;

        assume

         A7: x in ( meet S);

         not x in ( union (X \ S))

        proof

          assume x in ( union (X \ S));

          then

          consider Z be set such that

           A8: x in Z and

           A9: Z in (X \ S) by TARSKI:def 4;

          reconsider Z as Subset of X by A9;

          (Z ` ) in S & not x in (Z ` ) by A8, A9, SETFAM_1:def 7, XBOOLE_0:def 5;

          hence thesis by A7, SETFAM_1:def 1;

        end;

        hence thesis by A7, XBOOLE_0:def 5;

      end;

      hence ( meet S) = (X \ ( union (X \ S))) by A1;

      thus ( union S) c= (X \ ( meet (X \ S)))

      proof

        let x be object;

        assume x in ( union S);

        then

        consider Y be set such that

         A10: x in Y and

         A11: Y in S by TARSKI:def 4;

        reconsider Y as Subset of X by A11;

         not x in ( meet (X \ S))

        proof

          ((Y ` ) ` ) in S by A11;

          then

           A12: (Y ` ) in (X \ S) by SETFAM_1:def 7;

          assume

           A13: x in ( meet (X \ S));

           not x in (Y ` ) by A10, XBOOLE_0:def 5;

          hence thesis by A13, A12, SETFAM_1:def 1;

        end;

        hence thesis by A10, A11, XBOOLE_0:def 5;

      end;

      let x be object;

      assume

       A14: x in (X \ ( meet (X \ S)));

      then not x in ( meet (X \ S)) by XBOOLE_0:def 5;

      then

      consider Z be set such that

       A15: Z in (X \ S) and

       A16: not x in Z by SETFAM_1:def 1;

      reconsider Z as Subset of X by A15;

      

       A17: (Z ` ) in S by A15, SETFAM_1:def 7;

      x in (Z ` ) by A14, A16, SUBSET_1: 29;

      hence thesis by A17, TARSKI:def 4;

    end;

    definition

      let X be set;

      let IT be Subset-Family of X;

      :: original: compl-closed

      redefine

      :: MEASURE1:def1

      attr IT is compl-closed means

      : Def1: for A be set holds A in IT implies (X \ A) in IT;

      compatibility

      proof

        hereby

          assume

           A1: IT is compl-closed;

          let A be set;

          assume

           A2: A in IT;

          then

          reconsider A9 = A as Subset of X;

          (A9 ` ) in IT by A1, A2;

          hence (X \ A) in IT;

        end;

        assume

         A3: for A be set holds A in IT implies (X \ A) in IT;

        let A be Subset of X;

        assume A in IT;

        hence thesis by A3;

      end;

    end

    registration

      let X be set;

      cluster cup-closed compl-closed -> cap-closed for Subset-Family of X;

      coherence

      proof

        let S be Subset-Family of X;

        assume

         A1: S is cup-closed compl-closed;

        let A,B be set;

        assume that

         A2: A in S and

         A3: B in S;

        (X \ A) in S & (X \ B) in S by A1, A2, A3;

        then

         A4: ((X \ A) \/ (X \ B)) in S by A1;

        (A /\ B) c= A by XBOOLE_1: 17;

        

        then (A /\ B) = (X /\ (A /\ B)) by A2, XBOOLE_1: 1, XBOOLE_1: 28

        .= (X \ (X \ (A /\ B))) by XBOOLE_1: 48

        .= (X \ ((X \ A) \/ (X \ B))) by XBOOLE_1: 54;

        hence thesis by A1, A4;

      end;

      cluster cap-closed compl-closed -> cup-closed for Subset-Family of X;

      coherence

      proof

        let S be Subset-Family of X;

        assume

         A5: S is cap-closed compl-closed;

        let A,B be set;

        assume

         A6: A in S & B in S;

        then (X \ A) in S & (X \ B) in S by A5;

        then

         A7: ((X \ A) /\ (X \ B)) in S by A5;

        (A \/ B) = (X /\ (A \/ B)) by A6, XBOOLE_1: 8, XBOOLE_1: 28

        .= (X \ (X \ (A \/ B))) by XBOOLE_1: 48

        .= (X \ ((X \ A) /\ (X \ B))) by XBOOLE_1: 53;

        hence thesis by A5, A7;

      end;

    end

    theorem :: MEASURE1:5

    for S be Field_Subset of X holds S = (X \ S)

    proof

      let S be Field_Subset of X;

      for A be object holds A in S iff A in (X \ S)

      proof

        let A be object;

        hereby

          assume

           A1: A in S;

          then

          reconsider B = A as Subset of X;

          (B ` ) in S by A1, PROB_1:def 1;

          hence A in (X \ S) by SETFAM_1:def 7;

        end;

        assume

         A2: A in (X \ S);

        then

        reconsider B = A as Subset of X;

        (B ` ) in S by A2, SETFAM_1:def 7;

        then ((B ` ) ` ) in S by PROB_1:def 1;

        hence thesis;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let X;

      cluster compl-closed cap-closed -> diff-closed for Subset-Family of X;

      coherence

      proof

        let S be Subset-Family of X such that

         A1: S is compl-closed and

         A2: S is cap-closed;

        let A,B be set;

        assume that

         A3: A in S and

         A4: B in S;

        

         A5: (A /\ (X \ B)) = ((A /\ X) \ B) by XBOOLE_1: 49

        .= (A \ B) by A3, XBOOLE_1: 28;

        (X \ B) in S by A4, A1;

        hence thesis by A3, A5, A2;

      end;

    end

    theorem :: MEASURE1:6

    for S be Field_Subset of X holds for A,B be set st A in S & B in S holds (A \ B) in S by FINSUB_1:def 3;

    theorem :: MEASURE1:7

    for S be Field_Subset of X holds {} in S & X in S by PROB_1: 4, PROB_1: 5;

    definition

      let X be non empty set, F be Function of X, ExtREAL ;

      :: original: nonnegative

      redefine

      :: MEASURE1:def2

      attr F is nonnegative means

      : Def2: for A be Element of X holds 0. <= (F . A);

      compatibility by SUPINF_2: 39;

    end

    definition

      let X be set, S be non empty Subset-Family of X;

      let F be Function of S, ExtREAL ;

      :: MEASURE1:def3

      attr F is additive means

      : Def3: for A,B be Element of S st A misses B & (A \/ B) in S holds (F . (A \/ B)) = ((F . A) + (F . B));

    end

    registration

      let X be set, S be Field_Subset of X;

      cluster nonnegative additive zeroed for Function of S, ExtREAL ;

      existence

      proof

        reconsider M = (S --> 0. ) as Function of S, ExtREAL ;

        

         A1: for A,B be Element of S st A misses B holds (M . (A \/ B)) = ((M . A) + (M . B))

        proof

          let A,B be Element of S;

          assume A misses B;

          

           A2: (M . A) = 0. & (M . B) = 0. by FUNCOP_1: 7;

          reconsider A, B as set;

          reconsider A, B as Element of S;

           0. = ((M . A) + (M . B)) by A2, XXREAL_3: 4;

          hence thesis by FUNCOP_1: 7;

        end;

        take M;

        (for x be Element of S holds 0. <= (M . x)) & (M . {} ) = 0. by FUNCOP_1: 7, PROB_1: 4;

        hence thesis by A1, VALUED_0:def 19;

      end;

    end

    definition

      let X be set, S be Field_Subset of X;

      mode Measure of S is nonnegative additive zeroed Function of S, ExtREAL ;

    end

    theorem :: MEASURE1:8

    

     Th8: for S be Field_Subset of X, M be Measure of S, A,B be Element of S st A c= B holds (M . A) <= (M . B)

    proof

      let S be Field_Subset of X, M be Measure of S, A,B be Element of S;

      reconsider C = (B \ A) as Element of S;

      

       A1: 0. <= (M . C) by Def2;

      A misses C by XBOOLE_1: 79;

      then

       A2: (M . (A \/ C)) = ((M . A) + (M . C)) by Def3;

      assume A c= B;

      then (M . B) = ((M . A) + (M . C)) by A2, XBOOLE_1: 45;

      hence thesis by A1, XXREAL_3: 39;

    end;

    theorem :: MEASURE1:9

    

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

    proof

      let S be Field_Subset of X, M be Measure of S, A,B be Element of S;

      set C = (B \ A);

      assume that

       A1: A c= B and

       A2: (M . A) < +infty ;

      

       A3: 0. <= (M . A) by Def2;

      A misses C by XBOOLE_1: 79;

      then (M . (A \/ C)) = ((M . A) + (M . C)) by Def3;

      then (M . B) = ((M . A) + (M . C)) by A1, XBOOLE_1: 45;

      hence thesis by A2, A3, XXREAL_3: 28;

    end;

    registration

      let X be set;

      cluster non empty compl-closed cap-closed for Subset-Family of X;

      existence

      proof

        take the non empty compl-closed cap-closed Subset-Family of X;

        thus thesis;

      end;

    end

    definition

      let X be set, S be non empty cup-closed Subset-Family of X, 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, S be Field_Subset of X, A,B be Element of S;

      :: original: /\

      redefine

      func A /\ B -> Element of S ;

      coherence by FINSUB_1:def 2;

      :: original: \

      redefine

      func A \ B -> Element of S ;

      coherence by FINSUB_1:def 3;

    end

    theorem :: MEASURE1:10

    

     Th10: for S be Field_Subset of X, M be Measure of S, A,B be Element of S holds (M . (A \/ B)) <= ((M . A) + (M . B))

    proof

      let S be Field_Subset of X, M be Measure of S, A,B be Element of S;

      set C = (B \ A);

      

       A1: A misses C by XBOOLE_1: 79;

      

       A2: (M . C) <= (M . B) by Th8, XBOOLE_1: 36;

      (M . (A \/ B)) = (M . (A \/ C)) by XBOOLE_1: 39

      .= ((M . A) + (M . C)) by A1, Def3;

      hence thesis by A2, XXREAL_3: 36;

    end;

    theorem :: MEASURE1:11

    for S be Field_Subset of X, M be Measure of S holds {} in S & X in S & for A,B be set st A in S & B in S holds (X \ A) in S & (A \/ B) in S & (A /\ B) in S by Def1, FINSUB_1:def 1, FINSUB_1:def 2, PROB_1: 4, PROB_1: 5;

    definition

      let X be set, S be Field_Subset of X, M be Measure of S;

      :: MEASURE1:def4

      mode measure_zero of M -> Element of S means

      : Def4: (M . it ) = 0. ;

      existence

      proof

        reconsider A = {} as Element of S by PROB_1: 4;

        take A;

        thus thesis by VALUED_0:def 19;

      end;

    end

    theorem :: MEASURE1:12

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

    proof

      let S be Field_Subset of X, M be Measure of S, A be Element of S, B be measure_zero of M;

      assume A c= B;

      then (M . A) <= (M . B) by Th8;

      then

       A1: (M . A) <= 0. by Def4;

       0. <= (M . A) by Def2;

      then (M . A) = 0. by A1;

      hence thesis by Def4;

    end;

    theorem :: MEASURE1:13

    for S be Field_Subset of X, M be Measure of S, A,B be 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

      let S be Field_Subset of X, M be Measure of S, A,B be measure_zero of M;

      

       A1: 0. <= (M . (A /\ B)) by Def2;

      

       A2: 0. <= (M . (A \ B)) by Def2;

      

       A3: (M . A) = 0. by Def4;

      then (M . (A \ B)) <= 0. by Th8, XBOOLE_1: 36;

      then

       A4: (M . (A \ B)) = 0. by A2;

      (M . B) = 0. by Def4;

      then (M . (A \/ B)) <= ( 0. + 0. ) by A3, Th10;

      then

       A5: (M . (A \/ B)) <= 0. by XXREAL_3: 4;

       0. <= (M . (A \/ B)) by Def2;

      then

       A6: (M . (A \/ B)) = 0. by A5;

      (M . (A /\ B)) <= 0. by A3, Th8, XBOOLE_1: 17;

      then (M . (A /\ B)) = 0. by A1;

      hence thesis by A6, A4, Def4;

    end;

    theorem :: MEASURE1:14

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

    proof

      let S be Field_Subset of X, M be Measure of S, A be Element of S, B be measure_zero of M;

      

       A1: (M . A) = (M . ((A /\ B) \/ (A \ B))) by XBOOLE_1: 51;

      

       A2: (M . B) = 0. by Def4;

      then

       A3: (M . (A /\ B)) <= 0. by Th8, XBOOLE_1: 17;

      

       A4: 0. <= (M . (A /\ B)) by Def2;

      then (M . (A /\ B)) = 0. by A3;

      then (M . A) <= ( 0. + (M . (A \ B))) by A1, Th10;

      then

       A5: (M . A) <= (M . (A \ B)) by XXREAL_3: 4;

      (M . (A \/ B)) <= ((M . A) + 0. ) by A2, Th10;

      then

       A6: (M . (A \/ B)) <= (M . A) by XXREAL_3: 4;

      (M . A) <= (M . (A \/ B)) & (M . (A \ B)) <= (M . A) by Th8, XBOOLE_1: 7, XBOOLE_1: 36;

      hence thesis by A4, A6, A3, A5, XXREAL_0: 1;

    end;

    theorem :: MEASURE1:15

    

     Th15: for A be Subset of X holds ex F be sequence of ( bool X) st ( rng F) = {A}

    proof

      let A be Subset of X;

      take ( NAT --> A);

      thus thesis by FUNCOP_1: 8;

    end;

    theorem :: MEASURE1:16

    

     Th16: for A be set holds ex F be sequence of {A} st for n be Element of NAT holds (F . n) = A

    proof

      let A be set;

      take ( NAT --> A);

      thus thesis by TARSKI:def 1;

    end;

    registration

      let X be set;

      cluster non empty countable for Subset-Family of X;

      existence

      proof

        reconsider S = { {} } as Subset-Family of X by SETFAM_1: 46;

        take S;

        thus S is non empty;

        ( {} X) is Subset of X;

        hence S is empty or ex F be sequence of ( bool X) st S = ( rng F) by Th15;

      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:17

    

     Th17: for A,B,C be Subset of X holds ex F be sequence of ( bool X) st ( rng F) = {A, B, C} & (F . 0 ) = A & (F . 1) = B & for n be Element of NAT st 1 < n holds (F . n) = C

    proof

      let A,B,C be Subset of X;

      take ((A,B) followed_by C);

      thus thesis by FUNCT_7: 122, FUNCT_7: 123, FUNCT_7: 124, FUNCT_7: 127;

    end;

    theorem :: MEASURE1:18

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

    proof

      let A,B be Subset of X;

      ex F be sequence of ( bool X) st ( rng F) = {A, B, ( {} X)} & (F . 0 ) = A & (F . 1) = B & for n be Element of NAT st 1 < n holds (F . n) = ( {} X) by Th17;

      hence thesis by SUPINF_2:def 8;

    end;

    theorem :: MEASURE1:19

    

     Th19: for A,B be Subset of X holds ex F be sequence of ( bool X) st ( rng F) = {A, B} & (F . 0 ) = A & for n be Nat st 0 < n holds (F . n) = B

    proof

      let A,B be Subset of X;

      take (A followed_by B);

      thus thesis by FUNCT_7: 119, FUNCT_7: 120, FUNCT_7: 126;

    end;

    theorem :: MEASURE1:20

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

    proof

      let A,B be Subset of X;

      ex F be sequence of ( bool X) st (( rng F) = {A, B} & (F . 0 ) = A & for n be Nat st 0 < n holds (F . n) = B) by Th19;

      hence thesis by SUPINF_2:def 8;

    end;

    theorem :: MEASURE1:21

    

     Th21: for S be N_Sub_set_fam of X holds (X \ S) is N_Sub_set_fam of X

    proof

      let S be N_Sub_set_fam of X;

      consider F be sequence of ( bool X) such that

       A1: S = ( rng F) by SUPINF_2:def 8;

      defpred P[ object, object] means ex V be Subset of X st V = (F . $1) & $2 = (V ` );

      

       A2: for n be object st n in NAT holds ex y be object st y in (X \ S) & P[n, y]

      proof

        let n be object;

        assume n in NAT ;

        then

        consider V be set such that

         A3: V in S and

         A4: V = (F . n) by A1, FUNCT_2: 4;

        reconsider V as Subset of X by A3;

        take (V ` );

        ((V ` ) ` ) in S by A3;

        hence thesis by A4, SETFAM_1:def 7;

      end;

      

       A5: ex G be sequence of (X \ S) st for n be object st n in NAT holds P[n, (G . n)] from FUNCT_2:sch 1( A2);

      

       A6: NAT = ( dom F) by FUNCT_2:def 1;

      ex G be sequence of ( bool X) st (X \ S) = ( rng G)

      proof

        consider G be sequence of (X \ S) such that

         A7: for n be object st n in NAT holds ex V be Subset of X st V = (F . n) & (G . n) = (V ` ) by A5;

        

         A8: ( dom G) = NAT by FUNCT_2:def 1;

        

         A9: (X \ S) c= ( rng G)

        proof

          let x be object;

          assume

           A10: x in (X \ S);

          then

          reconsider B = x as Subset of X;

          (B ` ) in S by A10, SETFAM_1:def 7;

          then

          consider n be object such that

           A11: n in NAT and

           A12: (F . n) = (B ` ) by A1, A6, FUNCT_1:def 3;

          ex V be Subset of X st V = (F . n) & (G . n) = (V ` ) by A7, A11;

          hence thesis by A8, A11, A12, FUNCT_1:def 3;

        end;

        reconsider G as sequence of ( bool X) by FUNCT_2: 7;

        take G;

        thus thesis by A9;

      end;

      hence thesis by SUPINF_2:def 8;

    end;

    definition

      let X be set;

      let IT be Subset-Family of X;

      :: MEASURE1:def5

      attr IT is sigma-additive means

      : Def5: for M be N_Sub_set_fam of X st M c= IT holds ( union M) in IT;

    end

    registration

      let X be set;

      cluster non empty compl-closed sigma-additive for Subset-Family of X;

      existence

      proof

        reconsider S = { {} , X} as non empty Subset-Family of X by PROB_1: 8;

        take S;

        thus S is non empty;

        thus for A be set holds A in S implies (X \ A) in S

        proof

          let A be set;

          

           A1: A = {} implies (X \ A) in S by TARSKI:def 2;

          

           A2: A = X implies (X \ A) in S

          proof

            assume A = X;

            then (X \ A) = {} by XBOOLE_1: 37;

            hence thesis by TARSKI:def 2;

          end;

          assume A in S;

          hence thesis by A1, A2, TARSKI:def 2;

        end;

        let M be N_Sub_set_fam of X;

        assume

         A3: M c= S;

        

         A4: not X in M implies ( union M) in S

        proof

          assume not X in M;

          then for A be set st A in M holds A c= {} by A3, TARSKI:def 2;

          then ( union M) c= {} by ZFMISC_1: 76;

          then ( union M) = {} ;

          hence thesis by TARSKI:def 2;

        end;

        X in M implies ( union M) in S

        proof

          assume X in M;

          then X c= ( union M) by ZFMISC_1: 74;

          then X = ( union M);

          hence thesis by TARSKI:def 2;

        end;

        hence thesis by A4;

      end;

    end

    registration

      let X;

      cluster compl-closed sigma-multiplicative -> sigma-additive for Subset-Family of X;

      coherence

      proof

        let F be Subset-Family of X such that

         A1: F is compl-closed and

         A2: F is sigma-multiplicative;

        let M be non empty countable Subset-Family of X such that

         A3: M c= F;

        consider f be SetSequence of X such that

         A4: M = ( rng f) by SUPINF_2:def 8;

        for n be Nat holds (( Complement f) . n) in F

        proof

          let n be Nat;

          reconsider n as Element of NAT by ORDINAL1:def 12;

          (f . n) in M & (( Complement f) . n) = ((f . n) ` ) by A4, FUNCT_2: 4, PROB_1:def 2;

          hence thesis by A1, A3;

        end;

        then ( rng ( Complement f)) c= F by NAT_1: 52;

        then

         A5: ( Intersection ( Complement f)) in F by A2;

        (( Intersection ( Complement f)) ` ) = ( union M) by A4, CARD_3:def 4;

        hence thesis by A1, A5;

      end;

      cluster compl-closed sigma-additive -> sigma-multiplicative for Subset-Family of X;

      coherence

      proof

        let F be Subset-Family of X such that

         A6: F is compl-closed and

         A7: F is sigma-additive;

        let f be SetSequence of X such that

         A8: ( rng f) c= F;

        ( dom ( Complement f)) = NAT by FUNCT_2:def 1;

        then

        reconsider M = ( rng ( Complement f)) as non empty countable Subset-Family of X by CARD_3: 93;

        M c= F

        proof

          let e be object;

          assume e in M;

          then

          consider n be object such that

           A9: n in NAT and

           A10: e = (( Complement f) . n) by FUNCT_2: 11;

          reconsider n as Element of NAT by A9;

          

           A11: (f . n) in ( rng f) by NAT_1: 51;

          e = ((f . n) ` ) by A10, PROB_1:def 2;

          hence thesis by A6, A8, A11;

        end;

        then ( Intersection f) = (( union M) ` ) & ( union M) in F by A7, CARD_3:def 4;

        hence thesis by A6;

      end;

    end

    registration

      let X be set;

      cluster -> non empty for SigmaField of X;

      coherence ;

    end

    theorem :: MEASURE1:22

    

     Th22: for S be non empty Subset-Family of X holds (for A be set holds A in S implies (X \ A) in S) & (for M be N_Sub_set_fam of X st M c= S holds ( meet M) in S) iff S is SigmaField of X

    proof

      let S be non empty Subset-Family of X;

      hereby

        assume that

         A1: for A be set holds A in S implies (X \ A) in S and

         A2: for M be N_Sub_set_fam of X st M c= S holds ( meet M) in S;

        for M be N_Sub_set_fam of X st M c= S holds ( union M) in S

        proof

          let M be N_Sub_set_fam of X;

          assume

           A3: M c= S;

          

           A4: (X \ M) c= S

          proof

            let y be object;

            assume

             A5: y in (X \ M);

            then

            reconsider B = y as Subset of X;

            (B ` ) in M by A5, SETFAM_1:def 7;

            then ((B ` ) ` ) in S by A1, A3;

            hence thesis;

          end;

          (X \ M) is N_Sub_set_fam of X by Th21;

          then (X \ ( meet (X \ M))) in S by A1, A2, A4;

          hence thesis by Th4;

        end;

        then

        reconsider S9 = S as non empty compl-closed sigma-additive Subset-Family of X by A1, Def1, Def5;

        S9 is SigmaField of X;

        hence S is SigmaField of X;

      end;

      assume

       A6: S is SigmaField of X;

      for M be N_Sub_set_fam of X st M c= S holds ( meet M) in S

      proof

        let M be N_Sub_set_fam of X;

        assume

         A7: M c= S;

        

         A8: (X \ M) c= S

        proof

          let y be object;

          assume

           A9: y in (X \ M);

          then

          reconsider B = y as Subset of X;

          (B ` ) in M by A9, SETFAM_1:def 7;

          then ((B ` ) ` ) in S by A6, A7, PROB_1:def 1;

          hence thesis;

        end;

        (X \ M) is N_Sub_set_fam of X by Th21;

        then ( union (X \ M)) in S by A6, A8, Def5;

        then (X \ ( union (X \ M))) in S by A6, Def1;

        hence thesis by Th4;

      end;

      hence thesis by A6, Def1;

    end;

    registration

      let X be set;

      let S be SigmaField of X;

      cluster disjoint_valued for sequence of S;

      existence

      proof

        consider F be sequence of { {} } such that

         A1: for n be Element of NAT holds (F . n) = {} by Th16;

         {} in S by PROB_1: 4;

        then { {} } c= S by ZFMISC_1: 31;

        then

        reconsider F as sequence of S by FUNCT_2: 7;

        take F;

        

         A2: for n be object holds (F . n) = {}

        proof

          let n be object;

          per cases ;

            suppose n in ( dom F);

            hence thesis by A1;

          end;

            suppose not n in ( dom F);

            hence thesis by FUNCT_1:def 2;

          end;

        end;

        thus for x,y be object st x <> y holds (F . x) misses (F . y)

        proof

          let x,y be object;

          (F . x) = {} by A2;

          hence thesis;

        end;

      end;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      mode Sep_Sequence of S is disjoint_valued sequence of S;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      let F be sequence of S;

      :: original: rng

      redefine

      func rng F -> non empty Subset-Family of X ;

      coherence

      proof

        ( rng F) <> {} ;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    theorem :: MEASURE1:23

    

     Th23: for S be SigmaField of X, F be sequence of S holds ( rng F) is N_Sub_set_fam of X

    proof

      let S be SigmaField of X;

      let F be sequence of S;

      ex H be sequence of ( bool X) st ( rng F) = ( rng H)

      proof

        ( rng F) c= ( bool X);

        then

        reconsider F as sequence of ( bool X) by FUNCT_2: 6;

        take F;

        thus thesis;

      end;

      hence thesis by SUPINF_2:def 8;

    end;

    theorem :: MEASURE1:24

    

     Th24: for S be SigmaField of X, F be sequence of S holds ( union ( rng F)) is Element of S

    proof

      let S be SigmaField of X, F be sequence of S;

      ( rng F) is N_Sub_set_fam of X & ( rng F) c= S by Th23, RELAT_1:def 19;

      hence thesis by Def5;

    end;

    theorem :: MEASURE1:25

    

     Th25: for Y,S be non empty set, F be Function of Y, S, M be Function of S, ExtREAL st M is nonnegative holds (M * F) is nonnegative

    proof

      let Y,S be non empty set;

      let F be Function of Y, S;

      let M be Function of S, ExtREAL ;

      assume

       A1: M is nonnegative;

      for n be Element of Y holds 0. <= ((M * F) . n)

      proof

        let n be Element of Y;

        ( dom (M * F)) = Y by FUNCT_2:def 1;

        then ((M * F) . n) = (M . (F . n)) by FUNCT_1: 12;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: MEASURE1:26

    

     Th26: for S be SigmaField of X, a,b be R_eal holds ex M be Function of S, ExtREAL st for A be Element of S holds (A = {} implies (M . A) = a) & (A <> {} implies (M . A) = b)

    proof

      let S be SigmaField of X, a,b be R_eal;

      defpred P[ object, object] means ($1 = {} implies $2 = a) & ($1 <> {} implies $2 = b);

      

       A1: for x be object st x in S holds ex y be object st y in ExtREAL & P[x, y]

      proof

        let x be object;

        x <> {} implies ex y be set st y in ExtREAL & P[x, y];

        hence thesis;

      end;

      ex F be Function of S, ExtREAL st for x be object st x in S holds P[x, (F . x)] from FUNCT_2:sch 1( A1);

      then

      consider M be Function of S, ExtREAL such that

       A2: for x be object st x in S holds P[x, (M . x)];

      take M;

      thus thesis by A2;

    end;

    theorem :: MEASURE1:27

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

    theorem :: MEASURE1:28

    

     Th28: for S be SigmaField of X holds ex M be Function of S, ExtREAL st for A be Element of S holds (M . A) = 0.

    proof

      let S be SigmaField of X;

      consider M be Function of S, ExtREAL such that

       A1: for A be Element of S holds (A = {} implies (M . A) = 0. ) & (A <> {} implies (M . A) = 0. ) by Th26;

      take M;

      thus thesis by A1;

    end;

    definition

      let X be set;

      let S be SigmaField of X;

      let F be Function of S, ExtREAL ;

      :: MEASURE1:def6

      attr F is sigma-additive means for s be Sep_Sequence of S holds ( SUM (F * s)) = (F . ( union ( rng s)));

    end

    registration

      let X be set;

      let S be SigmaField of X;

      cluster nonnegative sigma-additive zeroed for Function of S, ExtREAL ;

      existence

      proof

        consider M be Function of S, ExtREAL such that

         A1: for A be Element of S holds (M . A) = 0. by Th28;

        take M;

        for A be Element of S holds 0. <= (M . A) by A1;

        hence

         A2: M is nonnegative;

        thus M is sigma-additive

        proof

          let F be Sep_Sequence of S;

          

           A3: for r be Element of NAT st 0 <= r holds ((M * F) . r) = 0.

          proof

            let r be Element of NAT ;

            ( dom (M * F)) = NAT by FUNCT_2:def 1;

            then ((M * F) . r) = (M . (F . r)) by FUNCT_1: 12;

            hence thesis by A1;

          end;

          (M * F) is nonnegative by A2, Th25;

          then

           A4: ( SUM (M * F)) = (( Ser (M * F)) . 0 ) by A3, SUPINF_2: 48;

          ( union ( rng F)) is Element of S by Th24;

          then

           A5: (M . ( union ( rng F))) = 0. by A1;

          (( Ser (M * F)) . 0 ) = ((M * F) . 0 ) by SUPINF_2:def 11;

          hence thesis by A5, A3, A4;

        end;

         {} is Element of S by PROB_1: 4;

        then (M . {} ) = 0. by A1;

        hence thesis by VALUED_0:def 19;

      end;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      mode sigma_Measure of S is nonnegative sigma-additive zeroed Function of S, ExtREAL ;

    end

    registration

      let X be set;

      cluster sigma-additive compl-closed -> cup-closed for non empty Subset-Family of X;

      coherence ;

    end

    registration

      let X be set, S be SigmaField of X;

      cluster sigma-additive -> additive for nonnegative zeroed Function of S, ExtREAL ;

      coherence

      proof

        let M be nonnegative zeroed Function of S, ExtREAL ;

        assume

         A1: M is sigma-additive;

        for A,B be Element of S holds (A misses B implies (M . (A \/ B)) = ((M . A) + (M . B)))

        proof

          set n2 = (1 + 1);

          let A,B be Element of S;

          assume

           A2: A misses B;

          

           A3: A in S & B in S;

          reconsider A, B as Subset of X;

           {} is Subset of X by XBOOLE_1: 2;

          then

          consider F be sequence of ( bool X) such that

           A4: ( rng F) = {A, B, {} } and

           A5: (F . 0 ) = A & (F . 1) = B and

           A6: for n be Element of NAT st 1 < n holds (F . n) = {} by Th17;

           {} in S by PROB_1: 4;

          then for x be object holds x in {A, B, {} } implies x in S by A3, ENUMSET1:def 1;

          then {A, B, {} } c= S;

          then

          reconsider F as sequence of S by A4, FUNCT_2: 6;

          

           A7: for n,m be Element of NAT st n <> m holds (F . n) misses (F . m)

          proof

            let n,m be Element of NAT ;

            

             A8: n = 0 or n = 1 or 1 < n by NAT_1: 25;

            

             A9: m = 0 or m = 1 or 1 < m by NAT_1: 25;

            

             A10: 1 < n & m = 1 implies (F . n) misses (F . m)

            proof

              assume that

               A11: 1 < n and m = 1;

              (F . n) = {} by A6, A11;

              then ((F . n) /\ (F . m)) = {} ;

              hence thesis;

            end;

            

             A12: 1 < n & m = 0 implies (F . n) misses (F . m)

            proof

              assume that

               A13: 1 < n and m = 0 ;

              (F . n) = {} by A6, A13;

              then ((F . n) /\ (F . m)) = {} ;

              hence thesis;

            end;

            

             A14: 1 < n & 1 < m implies (F . n) misses (F . m)

            proof

              assume that

               A15: 1 < n and 1 < m;

              (F . n) = {} by A6, A15;

              then ((F . n) /\ (F . m)) = {} ;

              hence thesis;

            end;

            

             A16: n = 1 & 1 < m implies (F . n) misses (F . m)

            proof

              assume that n = 1 and

               A17: 1 < m;

              (F . m) = {} by A6, A17;

              then ((F . n) /\ (F . m)) = {} ;

              hence thesis;

            end;

            

             A18: n = 0 & 1 < m implies (F . n) misses (F . m)

            proof

              assume that n = 0 and

               A19: 1 < m;

              (F . m) = {} by A6, A19;

              then ((F . n) /\ (F . m)) = {} ;

              hence thesis;

            end;

            assume n <> m;

            hence thesis by A2, A5, A8, A9, A18, A16, A12, A10, A14;

          end;

          for m,n be object st m <> n holds (F . m) misses (F . n)

          proof

            let m,n be object;

            assume

             A20: m <> n;

            per cases ;

              suppose m in NAT & n in NAT ;

              hence thesis by A7, A20;

            end;

              suppose not m in NAT or not n in NAT ;

              then not m in ( dom F) or not n in ( dom F);

              then (F . m) = {} or (F . n) = {} by FUNCT_1:def 2;

              hence thesis;

            end;

          end;

          then

          reconsider F as disjoint_valued sequence of S by PROB_2:def 2;

          ( union {A, B, {} }) = ( union {A, B}) by Th1;

          then

           A21: ( union ( rng F)) = (A \/ B) by A4, ZFMISC_1: 75;

          

           A22: for r be Element of NAT holds ((M * F) . 0 ) = (M . A) & ((M * F) . 1) = (M . B) & ((1 + 1) <= r implies ((M * F) . r) = 0. )

          proof

            let r be Element of NAT ;

            

             A23: for r be Element of NAT holds ((M * F) . r) = (M . (F . r))

            proof

              let r be Element of NAT ;

              ( dom (M * F)) = NAT by FUNCT_2:def 1;

              hence thesis by FUNCT_1: 12;

            end;

            (1 + 1) <= r implies ((M * F) . r) = 0.

            proof

              assume (1 + 1) <= r;

              then 1 < r by NAT_1: 13;

              then (F . r) = {} by A6;

              then ((M * F) . r) = (M . {} ) by A23;

              hence thesis by VALUED_0:def 19;

            end;

            hence thesis by A5, A23;

          end;

          set H = (M * F);

          

           A24: ( 0 + 1) = ( 0 + 1);

          set y1 = (( Ser H) . 1);

          

           A25: H is nonnegative by Th25;

          reconsider A, B as Element of S;

          (( Ser H) . n2) = (y1 + (H . n2)) by SUPINF_2:def 11;

          

          then (( Ser H) . n2) = (y1 + 0. ) by A22

          .= (( Ser H) . 1) by XXREAL_3: 4

          .= ((( Ser H) . 0 ) + (H . 1)) by A24, SUPINF_2:def 11

          .= ((M . A) + (M . B)) by A22, SUPINF_2:def 11;

          then ( SUM (M * F)) = ((M . A) + (M . B)) by A22, A25, SUPINF_2: 48;

          hence thesis by A21, A1;

        end;

        then M is additive;

        hence thesis;

      end;

    end

    theorem :: MEASURE1:29

    for S be SigmaField of X, M be sigma_Measure of S holds M is Measure of S;

    theorem :: MEASURE1:30

    for S be SigmaField of X, M be sigma_Measure of S, A,B be Element of S st A misses B holds (M . (A \/ B)) = ((M . A) + (M . B)) by Def3;

    theorem :: MEASURE1:31

    for S be SigmaField of X, M be sigma_Measure of S, A,B be Element of S st A c= B holds (M . A) <= (M . B) by Th8;

    theorem :: MEASURE1:32

    for S be SigmaField of X, M be sigma_Measure of S, A,B be Element of S st A c= B & (M . A) < +infty holds (M . (B \ A)) = ((M . B) - (M . A)) by Th9;

    theorem :: MEASURE1:33

    for S be SigmaField of X, M be sigma_Measure of S, A,B be Element of S holds (M . (A \/ B)) <= ((M . A) + (M . B)) by Th10;

    theorem :: MEASURE1:34

    for S be SigmaField of X, M be sigma_Measure of S holds {} in S & X in S & for A,B be set st A in S & B in S holds (X \ A) in S & (A \/ B) in S & (A /\ B) in S by Def1, FINSUB_1:def 1, FINSUB_1:def 2, PROB_1: 4, PROB_1: 5;

    theorem :: MEASURE1:35

    for S be SigmaField of X, M be sigma_Measure of S, T be N_Sub_set_fam of X st (for A be set st A in T holds A in S) holds ( union T) in S & ( meet T) in S

    proof

      let S be SigmaField of X, M be sigma_Measure of S, T be N_Sub_set_fam of X;

      assume

       A1: for A be set st A in T holds A in S;

      T c= S by A1;

      hence thesis by Def5, Th22;

    end;

    definition

      let X be set, S be SigmaField of X, M be sigma_Measure of S;

      :: MEASURE1:def7

      mode measure_zero of M -> Element of S means

      : Def7: (M . it ) = 0. ;

      existence

      proof

         {} is Element of S by PROB_1: 4;

        then

        consider A be Element of S such that

         A1: A = {} ;

        take A;

        thus thesis by A1, VALUED_0:def 19;

      end;

    end

    theorem :: MEASURE1:36

    for S be SigmaField of X, M be sigma_Measure of S, A be Element of S, B be measure_zero of M st A c= B holds A is measure_zero of M

    proof

      let S be SigmaField of X, M be sigma_Measure of S, A be Element of S, B be measure_zero of M;

      assume A c= B;

      then (M . A) <= (M . B) by Th8;

      then

       A1: (M . A) <= 0. by Def7;

       0. <= (M . A) by Def2;

      then (M . A) = 0. by A1;

      hence thesis by Def7;

    end;

    theorem :: MEASURE1:37

    for S be SigmaField of X, M be sigma_Measure of S, A,B be 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

      let S be SigmaField of X, M be sigma_Measure of S, A,B be measure_zero of M;

      

       A1: 0. <= (M . (A /\ B)) by Def2;

      

       A2: 0. <= (M . (A \ B)) by Def2;

      

       A3: (M . A) = 0. by Def7;

      then (M . (A \ B)) <= 0. by Th8, XBOOLE_1: 36;

      then

       A4: (M . (A \ B)) = 0. by A2;

      (M . B) = 0. by Def7;

      then (M . (A \/ B)) <= ( 0. + 0. ) by A3, Th10;

      then

       A5: (M . (A \/ B)) <= 0. by XXREAL_3: 4;

       0. <= (M . (A \/ B)) by Def2;

      then

       A6: (M . (A \/ B)) = 0. by A5;

      (M . (A /\ B)) <= 0. by A3, Th8, XBOOLE_1: 17;

      then (M . (A /\ B)) = 0. by A1;

      hence thesis by A6, A4, Def7;

    end;

    theorem :: MEASURE1:38

    for S be SigmaField of X, M be sigma_Measure of S, A be Element of S, B be measure_zero of M holds (M . (A \/ B)) = (M . A) & (M . (A /\ B)) = 0. & (M . (A \ B)) = (M . A)

    proof

      let S be SigmaField of X, M be sigma_Measure of S, A be Element of S, B be measure_zero of M;

      

       A1: (M . A) = (M . ((A /\ B) \/ (A \ B))) by XBOOLE_1: 51;

      

       A2: (M . B) = 0. by Def7;

      then

       A3: (M . (A /\ B)) <= 0. by Th8, XBOOLE_1: 17;

      

       A4: 0. <= (M . (A /\ B)) by Def2;

      then (M . (A /\ B)) = 0. by A3;

      then (M . A) <= ( 0. + (M . (A \ B))) by A1, Th10;

      then

       A5: (M . A) <= (M . (A \ B)) by XXREAL_3: 4;

      (M . (A \/ B)) <= ((M . A) + 0. ) by A2, Th10;

      then

       A6: (M . (A \/ B)) <= (M . A) by XXREAL_3: 4;

      (M . A) <= (M . (A \/ B)) & (M . (A \ B)) <= (M . A) by Th8, XBOOLE_1: 7, XBOOLE_1: 36;

      hence thesis by A4, A6, A3, A5, XXREAL_0: 1;

    end;

    definition

      let X be set, S be Field_Subset of X;

      let F be Function of S, ExtREAL ;

      :: original: additive

      redefine

      :: MEASURE1:def8

      attr F is additive means for A,B be Element of S st A misses B holds (F . (A \/ B)) = ((F . A) + (F . B));

      compatibility ;

    end