measure2.miz



    begin

    reserve X for set;

    theorem :: MEASURE2:1

    for S be SigmaField of X, M be sigma_Measure of S, F be sequence of S holds (M * F) is nonnegative by MEASURE1: 25;

    definition

      let X be set;

      let S be SigmaField of X;

      :: MEASURE2:def1

      mode N_Measure_fam of S -> N_Sub_set_fam of X means

      : Def1: it c= S;

      existence

      proof

         {} is Subset of X & { {} , {} } = { {} } by ENUMSET1: 29, XBOOLE_1: 2;

        then

        reconsider C = { {} } as N_Sub_set_fam of X by MEASURE1: 20;

        take C;

         {} in S by PROB_1: 4;

        hence thesis by ZFMISC_1: 31;

      end;

    end

    theorem :: MEASURE2:2

    

     Th2: for S be SigmaField of X, T be N_Measure_fam of S holds ( meet T) in S & ( union T) in S

    proof

      let S be SigmaField of X, T be N_Measure_fam of S;

      T c= S by Def1;

      hence thesis by MEASURE1: 22, MEASURE1:def 5;

    end;

    definition

      let X be set, S be SigmaField of X, T be N_Measure_fam of S;

      :: original: meet

      redefine

      func meet T -> Element of S ;

      coherence by Th2;

      :: original: union

      redefine

      func union T -> Element of S ;

      coherence by Th2;

    end

    theorem :: MEASURE2:3

    

     Th3: for S be SigmaField of X, N be sequence of S holds ex F be sequence of S st (F . 0 ) = (N . 0 ) & for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n))

    proof

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

      reconsider S as non empty set;

      defpred P[ set, set, set] means for A,B be Element of S, c be Nat holds c = $1 & A = $2 & B = $3 implies B = ((N . (c + 1)) \ (N . c));

      reconsider A = (N . 0 ) as Element of S;

      

       A1: for c be Nat, A be Element of S holds ex B be Element of S st P[c, A, B]

      proof

        let c be Nat, A be Element of S;

        reconsider B = ((N . (c + 1)) \ (N . c)) as Element of S;

        take B;

        thus thesis;

      end;

      consider F be sequence of S such that

       A2: (F . 0 ) = A & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

      for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n))

      proof

        let n be Nat;

        for a,b be Element of S, s be Nat st s = n & a = (F . n) & b = (F . (n + 1)) holds b = ((N . (s + 1)) \ (N . s)) by A2;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: MEASURE2:4

    

     Th4: for S be SigmaField of X, N be sequence of S holds ex F be sequence of S st (F . 0 ) = (N . 0 ) & for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \/ (F . n))

    proof

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

      defpred P[ set, set, set] means for A,B be Element of S, c be Nat holds (c = $1 & A = $2 & B = $3 implies B = ((N . (c + 1)) \/ A));

      

       A1: for c be Nat holds for A be Element of S holds ex B be Element of S st P[c, A, B]

      proof

        let c be Nat, A be Element of S;

        reconsider B = ((N . (c + 1)) \/ A) as Element of S;

        take B;

        thus thesis;

      end;

      consider F be sequence of S such that

       A2: (F . 0 ) = (N . 0 ) & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

      for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \/ (F . n)) by A2;

      hence thesis by A2;

    end;

    theorem :: MEASURE2:5

    

     Th5: for S be non empty Subset-Family of X, N,F be sequence of S holds (F . 0 ) = (N . 0 ) & (for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \/ (F . n))) implies for r be set holds for n be Nat holds (r in (F . n) iff ex k be Nat st k <= n & r in (N . k))

    proof

      let S be non empty Subset-Family of X, N,F be sequence of S;

      assume that

       A1: (F . 0 ) = (N . 0 ) and

       A2: for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \/ (F . n));

      let r be set, n be Nat;

      defpred P[ Nat] means (ex k be Nat st k <= $1 & r in (N . k)) implies r in (F . $1);

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: (ex k be Nat st k <= n & r in (N . k)) implies r in (F . n);

        

         A5: (F . (n + 1)) = ((N . (n + 1)) \/ (F . n)) by A2;

        given k be Nat such that

         A6: k <= (n + 1) and

         A7: r in (N . k);

        k <= n or k = (n + 1) by A6, NAT_1: 8;

        hence thesis by A4, A7, A5, XBOOLE_0:def 3;

      end;

      thus r in (F . n) implies ex k be Nat st k <= n & r in (N . k)

      proof

        defpred P[ Nat] means r in (F . $1);

        assume

         A8: r in (F . n);

        then

         A9: ex n be Nat st P[n];

        ex s be Nat st P[s] & for k be Nat st P[k] holds s <= k from NAT_1:sch 5( A9);

        then

        consider s be Nat such that

         A10: r in (F . s) and

         A11: for k be Nat st r in (F . k) holds s <= k;

        

         A12: (ex k be Nat st s = (k + 1)) implies ex k be Element of NAT st k <= n & r in (N . k)

        proof

          given k be Nat such that

           A13: s = (k + 1);

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

          

           A14: not r in (F . k)

          proof

            assume r in (F . k);

            then s <= k by A11;

            hence thesis by A13, NAT_1: 13;

          end;

          take s;

          

           A15: s in NAT by ORDINAL1:def 12;

          (F . s) = ((N . s) \/ (F . k)) by A2, A13;

          hence thesis by A8, A10, A11, A14, A15, XBOOLE_0:def 3;

        end;

        s = 0 implies ex k be Element of NAT st k <= n & r in (N . k) by A1, A10, NAT_1: 2;

        hence thesis by A12, NAT_1: 6;

      end;

      

       A16: P[ 0 ] by A1, NAT_1: 3;

      for n be Nat holds P[n] from NAT_1:sch 2( A16, A3);

      hence thesis;

    end;

    theorem :: MEASURE2:6

    

     Th6: for S be non empty Subset-Family of X, N,F be sequence of S holds ((F . 0 ) = (N . 0 ) & (for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \/ (F . n))) implies for n,m be Nat st n < m holds (F . n) c= (F . m))

    proof

      let S be non empty Subset-Family of X, N,F be sequence of S;

      assume that

       A1: (F . 0 ) = (N . 0 ) and

       A2: for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \/ (F . n));

      defpred X[ Nat] means for m be Nat st $1 < m holds (F . $1) c= (F . m);

      

       A3: X[ 0 ]

      proof

        

         A4: for k be Nat st 0 < (k + 1) holds (F . 0 ) c= (F . (k + 1))

        proof

          defpred P[ Nat] means 0 < ($1 + 1) implies (F . 0 ) c= (F . ($1 + 1));

          

           A5: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            

             A6: 0 <= k by NAT_1: 2;

            (F . ((k + 1) + 1)) = ((N . ((k + 1) + 1)) \/ (F . (k + 1))) by A2;

            then

             A7: (F . (k + 1)) c= (F . ((k + 1) + 1)) by XBOOLE_1: 7;

            assume 0 < (k + 1) implies (F . 0 ) c= (F . (k + 1));

            hence thesis by A7, A6, NAT_1: 13, XBOOLE_1: 1;

          end;

          (F . ( 0 + 1)) = ((N . ( 0 + 1)) \/ (F . 0 )) by A2;

          then

           A8: P[ 0 ] by XBOOLE_1: 7;

          thus for k be Nat holds P[k] from NAT_1:sch 2( A8, A5);

        end;

        let m be Nat;

        assume

         A9: 0 < m;

        then

        consider k be Nat such that

         A10: m = (k + 1) by NAT_1: 6;

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

        m = (k + 1) by A10;

        hence thesis by A9, A4;

      end;

      

       A11: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        assume

         A12: for m be Nat st n < m holds (F . n) c= (F . m);

        let m be Nat;

        assume

         A13: (n + 1) < m;

        let r be object;

        

         A14: r in (F . n) implies r in (F . m)

        proof

          assume

           A15: r in (F . n);

          n < m implies r in (F . m)

          proof

            assume n < m;

            then (F . n) c= (F . m) by A12;

            hence thesis by A15;

          end;

          hence thesis by A13, NAT_1: 13;

        end;

        assume

         A16: r in (F . (n + 1));

        

         A17: (F . (n + 1)) = ((N . (n + 1)) \/ (F . n)) by A2;

        r in (N . (n + 1)) implies r in (F . m) by A1, A2, A13, Th5;

        hence thesis by A16, A17, A14, XBOOLE_0:def 3;

      end;

      thus for n be Nat holds X[n] from NAT_1:sch 2( A3, A11);

    end;

    theorem :: MEASURE2:7

    

     Th7: for S be non empty Subset-Family of X, N,G,F be sequence of S holds (G . 0 ) = (N . 0 ) & (for n be Nat holds (G . (n + 1)) = ((N . (n + 1)) \/ (G . n))) & (F . 0 ) = (N . 0 ) & (for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (G . n))) implies for n,m be Nat st n <= m holds (F . n) c= (G . m)

    proof

      let S be non empty Subset-Family of X, N,G,F be sequence of S;

      assume that

       A1: (G . 0 ) = (N . 0 ) and

       A2: for n be Nat holds (G . (n + 1)) = ((N . (n + 1)) \/ (G . n)) and

       A3: (F . 0 ) = (N . 0 ) and

       A4: for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (G . n));

      let n,m be Nat;

      

       A5: for n be Nat holds (F . n) c= (G . n)

      proof

        defpred P[ Nat] means (F . $1) c= (G . $1);

        

         A6: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume (F . n) c= (G . n);

          (G . (n + 1)) = ((N . (n + 1)) \/ (G . n)) by A2;

          then

           A7: (N . (n + 1)) c= (G . (n + 1)) by XBOOLE_1: 7;

          (F . (n + 1)) = ((N . (n + 1)) \ (G . n)) by A4;

          hence thesis by A7, XBOOLE_1: 1;

        end;

        

         A8: P[ 0 ] by A1, A3;

        thus for n be Nat holds P[n] from NAT_1:sch 2( A8, A6);

      end;

      

       A9: n < m implies (F . n) c= (G . m)

      proof

        assume n < m;

        then

         A10: (G . n) c= (G . m) by A1, A2, Th6;

        (F . n) c= (G . n) by A5;

        hence thesis by A10;

      end;

      assume n <= m;

      then n = m or n < m by XXREAL_0: 1;

      hence thesis by A5, A9;

    end;

    theorem :: MEASURE2:8

    

     Th8: for S be SigmaField of X holds for N,G be sequence of S holds ex F be sequence of S st (F . 0 ) = (N . 0 ) & for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (G . n))

    proof

      let S be SigmaField of X;

      let N,G be sequence of S;

      defpred P[ set, set, set] means for A,B be Element of S, c be Nat holds (c = $1 & A = $2 & B = $3 implies B = ((N . (c + 1)) \ (G . c)));

      

       A1: for c be Nat holds for A be Element of S holds ex B be Element of S st P[c, A, B]

      proof

        let c be Nat;

        let A be Element of S;

        consider B be set such that

         A2: B = ((N . (c + 1)) \ (G . c));

        reconsider B as Element of S by A2;

        take B;

        thus thesis by A2;

      end;

      consider F be sequence of S such that

       A3: (F . 0 ) = (N . 0 ) & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

      for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (G . n))

      proof

        let n be Nat;

        for a,b be Element of S, s be Nat st s = n & a = (F . n) & b = (F . (n + 1)) holds b = ((N . (s + 1)) \ (G . s)) by A3;

        hence thesis;

      end;

      hence thesis by A3;

    end;

    theorem :: MEASURE2:9

    for S be SigmaField of X holds for N be sequence of S holds ex F be sequence of S st (F . 0 ) = {} & for n be Nat holds (F . (n + 1)) = ((N . 0 ) \ (N . n))

    proof

      let S be SigmaField of X;

      let N be sequence of S;

      defpred P[ set, set, set] means for A,B be Element of S, c be Nat holds (c = $1 & A = $2 & B = $3 implies B = ((N . 0 ) \ (N . c)));

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

      

       A1: for c be Nat holds for A be Element of S holds ex B be Element of S st P[c, A, B]

      proof

        let c be Nat;

        let A be Element of S;

        reconsider B = ((N . 0 ) \ (N . c)) as Element of S;

        take B;

        thus thesis;

      end;

      consider F be sequence of S such that

       A2: (F . 0 ) = A & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

      for n be Nat holds (F . (n + 1)) = ((N . 0 ) \ (N . n))

      proof

        let n be Nat;

        for a,b be Element of S, s be Nat st s = n & a = (F . n) & b = (F . (n + 1)) holds b = ((N . 0 ) \ (N . s)) by A2;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: MEASURE2:10

    

     Th10: for S be SigmaField of X holds for N,G,F be sequence of S holds (G . 0 ) = (N . 0 ) & (for n be Nat holds (G . (n + 1)) = ((N . (n + 1)) \/ (G . n))) & (F . 0 ) = (N . 0 ) & (for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (G . n))) implies for n,m be Nat st n < m holds (F . n) misses (F . m)

    proof

      let S be SigmaField of X;

      let N,G,F be sequence of S;

      assume that

       A1: ((G . 0 ) = (N . 0 ) & for n be Nat holds (G . (n + 1)) = ((N . (n + 1)) \/ (G . n))) & (F . 0 ) = (N . 0 ) and

       A2: for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (G . n));

      let n,m be Nat;

      assume

       A3: n < m;

      then 0 <> m by NAT_1: 2;

      then

      consider k be Nat such that

       A4: m = (k + 1) by NAT_1: 6;

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

      (F . (k + 1)) = ((N . (k + 1)) \ (G . k)) by A2;

      then

       A5: (G . k) misses (F . (k + 1)) by XBOOLE_1: 79;

      n <= k by A3, A4, NAT_1: 13;

      

      hence ((F . n) /\ (F . m)) = (((F . n) /\ (G . k)) /\ (F . (k + 1))) by A1, A2, A4, Th7, XBOOLE_1: 28

      .= ((F . n) /\ ((G . k) /\ (F . (k + 1)))) by XBOOLE_1: 16

      .= ((F . n) /\ {} ) by A5

      .= {} ;

    end;

    theorem :: MEASURE2:11

    

     Th11: for S be SigmaField of X, M be sigma_Measure of S, T be N_Measure_fam of S, F be sequence of S st T = ( rng F) holds (M . ( union T)) <= ( SUM (M * F))

    proof

      let S be SigmaField of X, M be sigma_Measure of S, T be N_Measure_fam of S, F be sequence of S;

      consider G be sequence of S such that

       A1: (G . 0 ) = (F . 0 ) & for n be Nat holds (G . (n + 1)) = ((F . (n + 1)) \/ (G . n)) by Th4;

      consider H be sequence of S such that

       A2: (H . 0 ) = (F . 0 ) and

       A3: for n be Nat holds (H . (n + 1)) = ((F . (n + 1)) \ (G . n)) by Th8;

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

      proof

        let n,m be object;

        assume

         A4: n <> m;

        per cases ;

          suppose n in ( dom H) & m in ( dom H);

          then

          reconsider n9 = n, m9 = m as Element of NAT ;

          

           A5: m9 < n9 implies (H . m) misses (H . n) by A1, A2, A3, Th10;

          n9 < m9 implies (H . n) misses (H . m) by A1, A2, A3, Th10;

          hence thesis by A4, A5, XXREAL_0: 1;

        end;

          suppose not (n in ( dom H) & m in ( dom H));

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

          hence thesis;

        end;

      end;

      then H is Sep_Sequence of S by PROB_2:def 2;

      then

       A6: ( SUM (M * H)) = (M . ( union ( rng H))) by MEASURE1:def 6;

      

       A7: for n be Element of NAT holds (H . n) c= (F . n)

      proof

        let n be Element of NAT ;

        

         A8: (ex k be Nat st n = (k + 1)) implies (H . n) c= (F . n)

        proof

          given k be Nat such that

           A9: n = (k + 1);

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

          (H . n) = ((F . n) \ (G . k)) by A3, A9;

          hence thesis by XBOOLE_1: 36;

        end;

        n = 0 or ex k be Nat st n = (k + 1) by NAT_1: 6;

        hence thesis by A2, A8;

      end;

      

       A10: for n be Element of NAT holds ((M * H) . n) <= ((M * F) . n)

      proof

        let n be Element of NAT ;

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

        then

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

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

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

        hence thesis by A7, A11, MEASURE1: 31;

      end;

      

       A12: ( union ( rng H)) = ( union ( rng F))

      proof

        thus ( union ( rng H)) c= ( union ( rng F))

        proof

          let r be object;

          assume r in ( union ( rng H));

          then

          consider E be set such that

           A13: r in E and

           A14: E in ( rng H) by TARSKI:def 4;

          consider s be object such that

           A15: s in ( dom H) and

           A16: E = (H . s) by A14, FUNCT_1:def 3;

          reconsider s as Element of NAT by A15;

          

           A17: (F . s) in ( rng F) by FUNCT_2: 4;

          E c= (F . s) by A7, A16;

          hence thesis by A13, A17, TARSKI:def 4;

        end;

        let r be object;

        assume r in ( union ( rng F));

        then

        consider E be set such that

         A18: r in E and

         A19: E in ( rng F) by TARSKI:def 4;

        

         A20: ex s be object st s in ( dom F) & E = (F . s) by A19, FUNCT_1:def 3;

        ex s1 be Element of NAT st r in (H . s1)

        proof

          defpred P[ Nat] means r in (F . $1);

          

           A21: ex k be Nat st P[k] by A18, A20;

          ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A21);

          then

          consider k be Nat such that

           A22: r in (F . k) and

           A23: for n be Nat st r in (F . n) holds k <= n;

          

           A24: (ex l be Nat st k = (l + 1)) implies ex s1 be Element of NAT st r in (H . s1)

          proof

            given l be Nat such that

             A25: k = (l + 1);

            take k;

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

            

             A26: not r in (G . l)

            proof

              assume r in (G . l);

              then

              consider i be Nat such that

               A27: i <= l and

               A28: r in (F . i) by A1, Th5;

              k <= i by A23, A28;

              hence thesis by A25, A27, NAT_1: 13;

            end;

            (H . (l + 1)) = ((F . (l + 1)) \ (G . l)) by A3;

            hence thesis by A22, A25, A26, XBOOLE_0:def 5;

          end;

          k = 0 implies ex s1 be Element of NAT st r in (H . s1) by A2, A22;

          hence thesis by A24, NAT_1: 6;

        end;

        then

        consider s1 be Element of NAT such that

         A29: r in (H . s1);

        (H . s1) in ( rng H) by FUNCT_2: 4;

        hence thesis by A29, TARSKI:def 4;

      end;

      assume T = ( rng F);

      hence thesis by A10, A6, A12, SUPINF_2: 43;

    end;

    theorem :: MEASURE2:12

    

     Th12: for S be SigmaField of X, T be N_Measure_fam of S holds ex F be sequence of S st T = ( rng F)

    proof

      let S be SigmaField of X, T be N_Measure_fam of S;

      consider F be sequence of ( bool X) such that

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

      ( rng F) c= S by A1, Def1;

      then F is sequence of S by FUNCT_2: 6;

      then

      consider F be sequence of S such that

       A2: T = ( rng F) by A1;

      take F;

      thus thesis by A2;

    end;

    theorem :: MEASURE2:13

    

     Th13: for N,F be Function st ((F . 0 ) = {} & for n be Nat holds (F . (n + 1)) = ((N . 0 ) \ (N . n)) & (N . (n + 1)) c= (N . n)) holds for n be Nat holds (F . n) c= (F . (n + 1))

    proof

      let N,F be Function;

      assume that

       A1: (F . 0 ) = {} and

       A2: for n be Nat holds (F . (n + 1)) = ((N . 0 ) \ (N . n)) & (N . (n + 1)) c= (N . n);

      defpred P[ Nat] means (F . $1) c= (F . ($1 + 1));

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume (F . n) c= (F . (n + 1));

        (F . ((n + 1) + 1)) = ((N . 0 ) \ (N . (n + 1))) by A2;

        then ((N . 0 ) \ (N . n)) c= (F . ((n + 1) + 1)) by A2, XBOOLE_1: 34;

        hence thesis by A2;

      end;

      let n be Nat;

      (F . ( 0 + 1)) = ((N . 0 ) \ (N . 0 )) by A2;

      then

       A4: P[ 0 ] by A1, XBOOLE_1: 37;

      for n be Nat holds P[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: MEASURE2:14

    for S be SigmaField of X, M be sigma_Measure of S, T be N_Measure_fam of S st (for A be set st A in T holds A is measure_zero of M) holds ( union T) is measure_zero of M

    proof

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

      consider F be sequence of S such that

       A1: T = ( rng F) by Th12;

      set G = (M * F);

      assume

       A2: for A be set st A in T holds A is measure_zero of M;

      

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

      proof

        let r be Element of NAT ;

        (F . r) is measure_zero of M by A2, A1, FUNCT_2: 4;

        then (M . (F . r)) = 0. by MEASURE1:def 7;

        hence thesis by FUNCT_2: 15;

      end;

      G is nonnegative by MEASURE1: 25;

      then ( SUM G) = (( Ser G) . 0 ) by A3, SUPINF_2: 48;

      then ( SUM G) = (G . 0 ) by SUPINF_2:def 11;

      then ( SUM (M * F)) = 0. by A3;

      then

       A4: (M . ( union T)) <= 0. by A1, Th11;

       0. <= (M . ( union T)) by MEASURE1:def 2;

      then (M . ( union T)) = 0. by A4, XXREAL_0: 1;

      hence thesis by MEASURE1:def 7;

    end;

    theorem :: MEASURE2:15

    for S be SigmaField of X, M be sigma_Measure of S, T be N_Measure_fam of S st (ex A be set st A in T & A is measure_zero of M) holds ( meet T) is measure_zero of M by MEASURE1: 36, SETFAM_1: 3;

    theorem :: MEASURE2:16

    for S be SigmaField of X, M be sigma_Measure of S, T be N_Measure_fam of S st (for A be set st A in T holds A is measure_zero of M) holds ( meet T) is measure_zero of M

    proof

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

      assume

       A1: for A be set holds A in T implies A is measure_zero of M;

      ex A be set st A in T & A is measure_zero of M

      proof

        consider F be sequence of ( bool X) such that

         A2: T = ( rng F) by SUPINF_2:def 8;

        take (F . 0 );

        thus thesis by A1, A2, FUNCT_2: 4;

      end;

      hence thesis by MEASURE1: 36, SETFAM_1: 3;

    end;

    definition

      let X be set;

      let S be SigmaField of X;

      let IT be N_Measure_fam of S;

      :: MEASURE2:def2

      attr IT is non-decreasing means

      : Def2: ex F be sequence of S st IT = ( rng F) & for n be Nat holds (F . n) c= (F . (n + 1));

    end

    registration

      let X be set;

      let S be SigmaField of X;

      cluster non-decreasing for N_Measure_fam of S;

      existence

      proof

        consider A be set such that

         A1: A in S by PROB_1: 4;

        reconsider A as Subset of X by A1;

        consider B,C be Subset of X such that

         A2: B = A & C = A;

        

         A3: {A} c= S by A1, ZFMISC_1: 31;

        consider F be sequence of ( bool X) such that

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

         A5: (F . 0 ) = B & for n be Nat st 0 < n holds (F . n) = C by MEASURE1: 19;

        

         A6: ( rng F) = {A} by A2, A4, ENUMSET1: 29;

        then

         A7: ( rng F) c= S by A1, ZFMISC_1: 31;

         {A} is N_Sub_set_fam of X by A6, SUPINF_2:def 8;

        then

        reconsider T = {A} as N_Measure_fam of S by A3, Def1;

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

        take T, F;

        for n be Nat holds (F . n) c= (F . (n + 1))

        proof

          let n be Nat;

          (F . n) = A by A2, A5, NAT_1: 3;

          hence thesis by A2, A5, NAT_1: 3;

        end;

        hence thesis by A2, A4, ENUMSET1: 29;

      end;

    end

    definition

      let X be set;

      let S be SigmaField of X;

      let IT be N_Measure_fam of S;

      :: MEASURE2:def3

      attr IT is non-increasing means ex F be sequence of S st IT = ( rng F) & for n be Element of NAT holds (F . (n + 1)) c= (F . n);

    end

    registration

      let X be set;

      let S be SigmaField of X;

      cluster non-increasing for N_Measure_fam of S;

      existence

      proof

        consider A be set such that

         A1: A in S by PROB_1: 4;

        reconsider A as Subset of X by A1;

        

         A2: {A} c= S by A1, ZFMISC_1: 31;

        set B = A, C = A;

        consider F be sequence of ( bool X) such that

         A3: ( rng F) = {B, C} and

         A4: (F . 0 ) = B & for n be Nat st 0 < n holds (F . n) = C by MEASURE1: 19;

        

         A5: ( rng F) = {A} by A3, ENUMSET1: 29;

        then

         A6: ( rng F) c= S by A1, ZFMISC_1: 31;

         {A} is N_Sub_set_fam of X by A5, SUPINF_2:def 8;

        then

        reconsider T = {A} as N_Measure_fam of S by A2, Def1;

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

        take T, F;

        for n be Element of NAT holds (F . (n + 1)) c= (F . n)

        proof

          let n be Element of NAT ;

          (F . n) = A by A4, NAT_1: 3;

          hence thesis by A4, NAT_1: 3;

        end;

        hence thesis by A3, ENUMSET1: 29;

      end;

    end

    theorem :: MEASURE2:17

    for S be SigmaField of X, N,F be sequence of S holds ((F . 0 ) = {} & for n be Nat holds (F . (n + 1)) = ((N . 0 ) \ (N . n)) & (N . (n + 1)) c= (N . n)) implies ( rng F) is non-decreasing N_Measure_fam of S

    proof

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

      assume (F . 0 ) = {} & for n be Nat holds (F . (n + 1)) = ((N . 0 ) \ (N . n)) & (N . (n + 1)) c= (N . n);

      then

       A1: for n be Nat holds (F . n) c= (F . (n + 1)) by Th13;

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

      hence thesis by A1, Def1, Def2;

    end;

    theorem :: MEASURE2:18

    

     Th18: for N be Function st (for n be Nat holds (N . n) c= (N . (n + 1))) holds for m,n be Nat st n <= m holds (N . n) c= (N . m)

    proof

      let N be Function;

      defpred P[ Nat] means for n be Nat st n <= $1 holds (N . n) c= (N . $1);

      assume

       A1: for n be Nat holds (N . n) c= (N . (n + 1));

      

       A2: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A3: for n be Nat st n <= m holds (N . n) c= (N . m);

        let n be Nat;

        

         A4: n <= m implies (N . n) c= (N . (m + 1))

        proof

          assume n <= m;

          then

           A5: (N . n) c= (N . m) by A3;

          (N . m) c= (N . (m + 1)) by A1;

          hence thesis by A5;

        end;

        assume n <= (m + 1);

        hence thesis by A4, NAT_1: 8;

      end;

      

       A6: P[ 0 ] by NAT_1: 3;

      thus for m be Nat holds P[m] from NAT_1:sch 2( A6, A2);

    end;

    theorem :: MEASURE2:19

    

     Th19: for N,F be Function st ((F . 0 ) = (N . 0 ) & for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1))) holds for n,m be Nat st n < m holds (F . n) misses (F . m)

    proof

      let N,F be Function;

      assume that

       A1: (F . 0 ) = (N . 0 ) and

       A2: for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1));

      let n,m be Nat;

      assume

       A3: n < m;

      then 0 <> m by NAT_1: 2;

      then

      consider k be Nat such that

       A4: m = (k + 1) by NAT_1: 6;

      

       A5: for n be Nat holds (F . n) c= (N . n)

      proof

        defpred P[ Nat] means (F . $1) c= (N . $1);

        

         A6: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume (F . n) c= (N . n);

          (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) by A2;

          hence thesis;

        end;

        

         A7: P[ 0 ] by A1;

        thus for n be Nat holds P[n] from NAT_1:sch 2( A7, A6);

      end;

      

       A8: for n,m be Nat st n <= m holds (F . n) c= (N . m)

      proof

        let n,m be Nat;

        

         A9: n < m implies (F . n) c= (N . m)

        proof

          assume n < m;

          then

           A10: (N . n) c= (N . m) by A2, Th18;

          (F . n) c= (N . n) by A5;

          hence thesis by A10;

        end;

        assume n <= m;

        then n = m or n < m by XXREAL_0: 1;

        hence thesis by A5, A9;

      end;

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

      (F . (k + 1)) = ((N . (k + 1)) \ (N . k)) by A2;

      then

       A11: (N . k) misses (F . (k + 1)) by XBOOLE_1: 79;

      n <= k by A3, A4, NAT_1: 13;

      

      then ((F . n) /\ (F . (k + 1))) = (((F . n) /\ (N . k)) /\ (F . (k + 1))) by A8, XBOOLE_1: 28

      .= ((F . n) /\ ((N . k) /\ (F . (k + 1)))) by XBOOLE_1: 16

      .= ((F . n) /\ {} ) by A11

      .= {} ;

      hence thesis by A4;

    end;

    theorem :: MEASURE2:20

    

     Th20: for S be SigmaField of X, N,F be sequence of S holds ((F . 0 ) = (N . 0 ) & for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1))) implies ( union ( rng F)) = ( union ( rng N))

    proof

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

      assume that

       A1: (F . 0 ) = (N . 0 ) and

       A2: for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1));

      thus ( union ( rng F)) c= ( union ( rng N))

      proof

        let x be object;

        assume x in ( union ( rng F));

        then

        consider Y be set such that

         A3: x in Y and

         A4: Y in ( rng F) by TARSKI:def 4;

        consider n be object such that

         A5: n in ( dom F) and

         A6: Y = (F . n) by A4, FUNCT_1:def 3;

        reconsider n as Element of NAT by A5;

        

         A7: (ex k be Nat st n = (k + 1)) implies ex Z be set st x in Z & Z in ( rng N)

        proof

          given k be Nat such that

           A8: n = (k + 1);

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

          Y = ((N . (k + 1)) \ (N . k)) by A2, A6, A8;

          then x in (N . (k + 1)) by A3, XBOOLE_0:def 5;

          hence thesis by FUNCT_2: 4;

        end;

        n = 0 implies ex Z be set st x in Z & Z in ( rng N) by A1, A3, A6, FUNCT_2: 4;

        hence thesis by A7, NAT_1: 6, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union ( rng N));

      then

      consider Y be set such that

       A9: x in Y and

       A10: Y in ( rng N) by TARSKI:def 4;

      

       A11: ex n be object st n in ( dom N) & Y = (N . n) by A10, FUNCT_1:def 3;

      ex Z be set st x in Z & Z in ( rng F)

      proof

        ex s be Element of NAT st x in (F . s)

        proof

          defpred P[ Nat] means x in (N . $1);

          

           A12: ex k be Nat st P[k] by A9, A11;

          ex k be Nat st P[k] & for r be Nat st P[r] holds k <= r from NAT_1:sch 5( A12);

          then

          consider k be Nat such that

           A13: x in (N . k) and

           A14: for r be Nat st x in (N . r) holds k <= r;

          

           A15: (ex l be Nat st k = (l + 1)) implies ex s be Element of NAT st x in (F . s)

          proof

            given l be Nat such that

             A16: k = (l + 1);

            take k;

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

            

             A17: not x in (N . l)

            proof

              assume x in (N . l);

              then (l + 1) <= l by A14, A16;

              hence thesis by NAT_1: 13;

            end;

            (F . (l + 1)) = ((N . (l + 1)) \ (N . l)) by A2;

            hence thesis by A13, A16, A17, XBOOLE_0:def 5;

          end;

          k = 0 implies ex s be Element of NAT st x in (F . s) by A1, A13;

          hence thesis by A15, NAT_1: 6;

        end;

        hence thesis by FUNCT_2: 4;

      end;

      hence thesis by TARSKI:def 4;

    end;

    theorem :: MEASURE2:21

    

     Th21: for S be SigmaField of X, N,F be sequence of S holds ((F . 0 ) = (N . 0 ) & for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1))) implies F is Sep_Sequence of S

    proof

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

      assume

       A1: (F . 0 ) = (N . 0 ) & for n be Nat holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1));

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

      proof

        let n,m be object;

        assume

         A2: n <> m;

        per cases ;

          suppose n in ( dom F) & m in ( dom F);

          then

          reconsider n9 = n, m9 = m as Element of NAT ;

          

           A3: m9 < n9 implies (F . m) misses (F . n) by A1, Th19;

          n9 < m9 implies (F . n) misses (F . m) by A1, Th19;

          hence thesis by A2, A3, XXREAL_0: 1;

        end;

          suppose not (n in ( dom F) & m in ( dom F));

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

          hence thesis;

        end;

      end;

      hence thesis by PROB_2:def 2;

    end;

    theorem :: MEASURE2:22

    for S be SigmaField of X, N,F be sequence of S holds ((F . 0 ) = (N . 0 ) & for n be Element of NAT holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1))) implies ((N . 0 ) = (F . 0 ) & for n be Element of NAT holds (N . (n + 1)) = ((F . (n + 1)) \/ (N . n)))

    proof

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

      assume that

       A1: (F . 0 ) = (N . 0 ) and

       A2: for n be Element of NAT holds (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) & (N . n) c= (N . (n + 1));

      for n be Element of NAT holds (N . (n + 1)) = ((F . (n + 1)) \/ (N . n))

      proof

        let n be Element of NAT ;

        (F . (n + 1)) = ((N . (n + 1)) \ (N . n)) by A2;

        hence thesis by A2, XBOOLE_1: 45;

      end;

      hence thesis by A1;

    end;

    theorem :: MEASURE2:23

    for S be SigmaField of X, M be sigma_Measure of S, F be sequence of S st (for n be Nat holds (F . n) c= (F . (n + 1))) holds (M . ( union ( rng F))) = ( sup ( rng (M * F)))

    proof

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let F be sequence of S;

      consider G be sequence of S such that

       A1: (G . 0 ) = (F . 0 ) and

       A2: for n be Nat holds (G . (n + 1)) = ((F . (n + 1)) \ (F . n)) by Th3;

      assume

       A3: for n be Nat holds (F . n) c= (F . (n + 1));

      then

       A4: G is Sep_Sequence of S by A1, A2, Th21;

      

       A5: for m be object st m in NAT holds (( Ser (M * G)) . m) = ((M * F) . m)

      proof

        defpred P[ Nat] means (( Ser (M * G)) . $1) = ((M * F) . $1);

        let m be object;

        assume

         A6: m in NAT ;

        

         A7: for m be Nat holds P[m] implies P[(m + 1)]

        proof

          let m be Nat;

          

           A8: ((M * G) . (m + 1)) = (M . (G . (m + 1))) by FUNCT_2: 15;

          

           A9: ((M * F) . (m + 1)) = (M . (F . (m + 1))) by FUNCT_2: 15;

          

           A10: (G . (m + 1)) = ((F . (m + 1)) \ (F . m)) by A2;

          

           A11: m in NAT by ORDINAL1:def 12;

          assume (( Ser (M * G)) . m) = ((M * F) . m);

          

          then (( Ser (M * G)) . (m + 1)) = (((M * F) . m) + ((M * G) . (m + 1))) by SUPINF_2:def 11

          .= ((M . (F . m)) + (M . (G . (m + 1)))) by A8, FUNCT_2: 15, A11

          .= (M . ((F . m) \/ (G . (m + 1)))) by A10, MEASURE1: 30, XBOOLE_1: 79

          .= ((M * F) . (m + 1)) by A3, A9, A10, XBOOLE_1: 45;

          hence thesis;

        end;

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

        .= (M . (F . 0 )) by A1, FUNCT_2: 15

        .= ((M * F) . 0 ) by FUNCT_2: 15;

        then

         A12: P[ 0 ];

        for m be Nat holds P[m] from NAT_1:sch 2( A12, A7);

        hence thesis by A6;

      end;

      

       A13: ( dom ( Ser (M * G))) = NAT & ( dom (M * F)) = NAT by FUNCT_2:def 1;

      (M . ( union ( rng F))) = (M . ( union ( rng G))) by A3, A1, A2, Th20

      .= ( SUM (M * G)) by A4, MEASURE1:def 6

      .= ( sup ( rng (M * F))) by A13, A5, FUNCT_1: 2;

      hence thesis;

    end;