kurato_0.miz

    begin

    theorem :: KURATO_0:1

    for F be Function, i be set st i in ( dom F) holds ( meet F) c= (F . i)

    proof

      let F be Function, i be set;

      assume

       A1: i in ( dom F);

      let x be object;

      assume x in ( meet F);

      hence thesis by A1, FUNCT_6: 25, RELAT_1: 38;

    end;

    theorem :: KURATO_0:2

    for A,B,C,D be set st A meets B & C meets D holds [:A, C:] meets [:B, D:]

    proof

      let A,B,C,D be set;

      assume that

       A1: A meets B and

       A2: C meets D;

      consider x be object such that

       A3: x in A & x in B by A1, XBOOLE_0: 3;

      consider y be object such that

       A4: y in C & y in D by A2, XBOOLE_0: 3;

       [x, y] in [:A, C:] & [x, y] in [:B, D:] by A3, A4, ZFMISC_1: 87;

      hence thesis by XBOOLE_0: 3;

    end;

    registration

      let X be set;

      cluster -> non empty for SetSequence of X;

      coherence ;

    end

    registration

      let T be non empty set;

      cluster non-empty for SetSequence of T;

      existence

      proof

        set a = the Element of T;

        reconsider A = {a} as Subset of T;

        set X = ( NAT --> A);

        reconsider X as SetSequence of T;

        take X;

        thus thesis;

      end;

    end

    definition

      let X be set, F be SetSequence of X;

      :: original: Union

      redefine

      func Union F -> Subset of X ;

      coherence

      proof

        ( Union F) c= X;

        hence thesis;

      end;

      :: original: meet

      redefine

      func meet F -> Subset of X ;

      coherence

      proof

        reconsider G = ( rng F) as Subset-Family of X;

        ( meet G) c= X;

        hence thesis by FUNCT_6:def 4;

      end;

    end

    begin

    definition

      let X be set, F be SetSequence of X;

      :: KURATO_0:def1

      func lim_inf F -> Subset of X means

      : Def1: ex f be SetSequence of X st it = ( Union f) & for n be Nat holds (f . n) = ( meet (F ^\ n));

      existence

      proof

        deffunc F( Nat) = ( meet (F ^\ $1));

        consider f be SetSequence of X such that

         A1: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take ( Union f), f;

        thus ( Union f) = ( Union f);

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let A1,A2 be Subset of X;

        given f1 be SetSequence of X such that

         A2: A1 = ( Union f1) and

         A3: for n be Nat holds (f1 . n) = ( meet (F ^\ n));

        given f2 be SetSequence of X such that

         A4: A2 = ( Union f2) and

         A5: for n be Nat holds (f2 . n) = ( meet (F ^\ n));

        for n be Element of NAT holds (f1 . n) = (f2 . n)

        proof

          let n be Element of NAT ;

          (f1 . n) = ( meet (F ^\ n)) by A3

          .= (f2 . n) by A5;

          hence thesis;

        end;

        hence thesis by A2, A4, FUNCT_2: 63;

      end;

      :: KURATO_0:def2

      func lim_sup F -> Subset of X means

      : Def2: ex f be SetSequence of X st it = ( meet f) & for n be Nat holds (f . n) = ( Union (F ^\ n));

      existence

      proof

        deffunc F( Nat) = ( Union (F ^\ $1));

        consider f be SetSequence of X such that

         A6: for n be Element of NAT holds (f . n) = F(n) from FUNCT_2:sch 4;

        take ( meet f), f;

        thus ( meet f) = ( meet f);

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let A1,A2 be Subset of X;

        given f1 be SetSequence of X such that

         A7: A1 = ( meet f1) and

         A8: for n be Nat holds (f1 . n) = ( Union (F ^\ n));

        given f2 be SetSequence of X such that

         A9: A2 = ( meet f2) and

         A10: for n be Nat holds (f2 . n) = ( Union (F ^\ n));

        for n be Element of NAT holds (f1 . n) = (f2 . n)

        proof

          let n be Element of NAT ;

          (f1 . n) = ( Union (F ^\ n)) by A8

          .= (f2 . n) by A10;

          hence thesis;

        end;

        hence thesis by A7, A9, FUNCT_2: 63;

      end;

    end

    theorem :: KURATO_0:3



     Th3: for X be set, F be SetSequence of X, x be object holds x in ( meet F) iff for z be Nat holds x in (F . z)

    proof

      let X be set, F be SetSequence of X, x be object;

      hereby

        assume

         A1: x in ( meet F);

        let z be Nat;

        z in NAT by ORDINAL1:def 12;

        then z in ( dom F) by FUNCT_2:def 1;

        hence x in (F . z) by A1, FUNCT_6: 25;

      end;

      assume for z be Nat holds x in (F . z);

      then for y be object st y in ( dom F) holds x in (F . y);

      hence thesis by FUNCT_6: 25;

    end;

    theorem :: KURATO_0:4



     Th4: for X be set, F be SetSequence of X, x be object holds x in ( lim_inf F) iff ex n be Nat st for k be Nat holds x in (F . (n + k))

    proof

      let X be set, F be SetSequence of X, x be object;

      consider f be SetSequence of X such that

       A1: ( lim_inf F) = ( Union f) and

       A2: for n be Nat holds (f . n) = ( meet (F ^\ n)) by Def1;

      hereby

        consider f be SetSequence of X such that

         A3: ( lim_inf F) = ( Union f) and

         A4: for n be Nat holds (f . n) = ( meet (F ^\ n)) by Def1;

        assume x in ( lim_inf F);

        then

        consider n be Nat such that

         A5: x in (f . n) by A3, PROB_1: 12;

        set G = (F ^\ n);

        reconsider n as Nat;

        take n;

        let k be Nat;



         A6: (G . k) = (F . (n + k)) by NAT_1:def 3;

        x in ( meet (F ^\ n)) by A4, A5;

        hence x in (F . (n + k)) by A6, Th3;

      end;

      given n be Nat such that

       A7: for k be Nat holds x in (F . (n + k));

      set G = (F ^\ n);

      for z be Nat holds x in (G . z)

      proof

        let z be Nat;

        (G . z) = (F . (n + z)) by NAT_1:def 3;

        hence thesis by A7;

      end;

      then x in ( meet G) by Th3;

      then x in (f . n) by A2;

      hence thesis by A1, PROB_1: 12;

    end;

    theorem :: KURATO_0:5



     Th5: for X be set, F be SetSequence of X, x be object holds x in ( lim_sup F) iff for n be Nat holds ex k be Nat st x in (F . (n + k))

    proof

      let X be set, F be SetSequence of X, x be object;

      consider f be SetSequence of X such that

       A1: ( lim_sup F) = ( meet f) and

       A2: for n be Nat holds (f . n) = ( Union (F ^\ n)) by Def2;

      hereby

        assume

         A3: x in ( lim_sup F);

        let n be Nat;

        set G = (F ^\ n);

        consider f be SetSequence of X such that

         A4: ( lim_sup F) = ( meet f) and

         A5: for n be Nat holds (f . n) = ( Union (F ^\ n)) by Def2;

        (f . n) = ( Union G) by A5;

        then x in ( Union G) by A3, A4, Th3;

        then

        consider k be Nat such that

         A6: x in (G . k) by PROB_1: 12;

        reconsider k as Nat;

        take k;

        thus x in (F . (n + k)) by A6, NAT_1:def 3;

      end;

      assume

       A7: for n be Nat holds ex k be Nat st x in (F . (n + k));

      for z be Nat holds x in (f . z)

      proof

        let z be Nat;

        set G = (F ^\ z);

        consider k be Nat such that

         A8: x in (F . (z + k)) by A7;

        (f . z) = ( Union G) & (G . k) = (F . (z + k)) by A2, NAT_1:def 3;

        hence thesis by A8, PROB_1: 12;

      end;

      hence thesis by A1, Th3;

    end;

    theorem :: KURATO_0:6

    for X be set, F be SetSequence of X holds ( lim_inf F) c= ( lim_sup F)

    proof

      let X be set, F be SetSequence of X;

      let x be object;

      assume x in ( lim_inf F);

      then

      consider n be Nat such that

       A1: for k be Nat holds x in (F . (n + k)) by Th4;

      now

        let k be Nat;

        x in (F . (n + k)) by A1;

        hence ex n be Nat st x in (F . (k + n));

      end;

      hence thesis by Th5;

    end;

    theorem :: KURATO_0:7



     Th7: for X be set, F be SetSequence of X holds ( meet F) c= ( lim_inf F)

    proof

      let X be set, F be SetSequence of X;

      let x be object;

      assume x in ( meet F);

      then for k be Nat holds x in (F . ( 0 qua Nat + k)) by Th3;

      hence thesis by Th4;

    end;

    theorem :: KURATO_0:8



     Th8: for X be set, F be SetSequence of X holds ( lim_sup F) c= ( Union F)

    proof

      let X be set, F be SetSequence of X;

      let x be object;

      assume x in ( lim_sup F);

      then ex k be Nat st x in (F . ( 0 qua Nat + k)) by Th5;

      hence thesis by PROB_1: 12;

    end;

    theorem :: KURATO_0:9

    for X be set, F be SetSequence of X holds ( lim_inf F) = (( lim_sup ( Complement F)) ` )

    proof

      let X be set, F be SetSequence of X;

      set G = ( Complement F);

      thus ( lim_inf F) c= (( lim_sup ( Complement F)) ` )

      proof

        let x be object;

        assume

         A1: x in ( lim_inf F);

        then

        consider n be Nat such that

         A2: for k be Nat holds x in (F . (n + k)) by Th4;

        for k be Nat holds not x in (G . (n + k))

        proof

          let k be Nat;

          reconsider nk = (n + k) as Element of NAT by ORDINAL1:def 12;



           A3: (G . (n + k)) = ((F . nk) ` ) by PROB_1:def 2;

          assume x in (G . (n + k));

          then not x in (F . (n + k)) by A3, XBOOLE_0:def 5;

          hence thesis by A2;

        end;

        then not x in ( lim_sup G) by Th5;

        hence thesis by A1, XBOOLE_0:def 5;

      end;

      thus (( lim_sup ( Complement F)) ` ) c= ( lim_inf F)

      proof

        let x be object;

        assume

         A4: x in (( lim_sup ( Complement F)) ` );

        then not x in ( lim_sup ( Complement F)) by XBOOLE_0:def 5;

        then

        consider n be Nat such that

         A5: for k be Nat holds not x in (G . (n + k)) by Th5;

        for k be Nat holds x in (F . (n + k))

        proof

          let k be Nat;

          reconsider nk = (n + k) as Element of NAT by ORDINAL1:def 12;

          assume not x in (F . (n + k));

          then x in ((F . nk) ` ) by A4, XBOOLE_0:def 5;

          then x in (G . (n + k)) by PROB_1:def 2;

          hence thesis by A5;

        end;

        hence thesis by Th4;

      end;

    end;

    theorem :: KURATO_0:10

    for X be set, A,B,C be SetSequence of X st for n be Nat holds (C . n) = ((A . n) /\ (B . n)) holds ( lim_inf C) = (( lim_inf A) /\ ( lim_inf B))

    proof

      let X be set, A,B,C be SetSequence of X;

      assume

       A1: for n be Nat holds (C . n) = ((A . n) /\ (B . n));

      thus ( lim_inf C) c= (( lim_inf A) /\ ( lim_inf B))

      proof

        let x be object;

        assume x in ( lim_inf C);

        then

        consider n be Nat such that

         A2: for k be Nat holds x in (C . (n + k)) by Th4;

        for k be Nat holds x in (B . (n + k))

        proof

          let k be Nat;

          (C . (n + k)) = ((A . (n + k)) /\ (B . (n + k))) & x in (C . (n + k)) by A1, A2;

          hence thesis by XBOOLE_0:def 4;

        end;

        then

         A3: x in ( lim_inf B) by Th4;

        for k be Nat holds x in (A . (n + k))

        proof

          let k be Nat;

          (C . (n + k)) = ((A . (n + k)) /\ (B . (n + k))) & x in (C . (n + k)) by A1, A2;

          hence thesis by XBOOLE_0:def 4;

        end;

        then x in ( lim_inf A) by Th4;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      thus (( lim_inf A) /\ ( lim_inf B)) c= ( lim_inf C)

      proof

        let x be object;

        assume

         A4: x in (( lim_inf A) /\ ( lim_inf B));

        then x in ( lim_inf A) by XBOOLE_0:def 4;

        then

        consider n1 be Nat such that

         A5: for k be Nat holds x in (A . (n1 + k)) by Th4;

        x in ( lim_inf B) by A4, XBOOLE_0:def 4;

        then

        consider n2 be Nat such that

         A6: for k be Nat holds x in (B . (n2 + k)) by Th4;

        set n = ( max (n1,n2));



         A0: n is Nat by TARSKI: 1;



         A7: for k be Nat holds x in (B . (n + k))

        proof

          let k be Nat;

          consider g be Nat such that

           A8: n = (n2 + g) by NAT_1: 10, XXREAL_0: 25;

          reconsider g as Nat;

          x in (B . (n2 + (g + k))) by A6;

          hence thesis by A8;

        end;



         A9: for k be Nat holds x in (A . (n + k))

        proof

          let k be Nat;

          consider g be Nat such that

           A10: n = (n1 + g) by NAT_1: 10, XXREAL_0: 25;

          reconsider g as Nat;

          x in (A . (n1 + (g + k))) by A5;

          hence thesis by A10;

        end;

        for k be Nat holds x in (C . (n + k))

        proof

          let k be Nat;

          x in (A . (n + k)) & x in (B . (n + k)) by A9, A7;

          then x in ((A . (n + k)) /\ (B . (n + k))) by XBOOLE_0:def 4;

          hence thesis by A1;

        end;

        hence thesis by A0, Th4;

      end;

    end;

    theorem :: KURATO_0:11

    for X be set, A,B,C be SetSequence of X st for n be Nat holds (C . n) = ((A . n) \/ (B . n)) holds ( lim_sup C) = (( lim_sup A) \/ ( lim_sup B))

    proof

      let X be set, A,B,C be SetSequence of X;

      assume

       A1: for n be Nat holds (C . n) = ((A . n) \/ (B . n));

      thus ( lim_sup C) c= (( lim_sup A) \/ ( lim_sup B))

      proof

        let x be object;

        assume

         A2: x in ( lim_sup C);

        (for n be Nat holds ex k be Nat st x in (A . (n + k))) or for n be Nat holds ex k be Nat st x in (B . (n + k))

        proof

          given n1 be Nat such that

           A3: for k be Nat holds not x in (A . (n1 + k));

          given n2 be Nat such that

           A4: for k be Nat holds not x in (B . (n2 + k));

          set n = ( max (n1,n2));

          consider g be Nat such that

           A5: n = (n1 + g) by NAT_1: 10, XXREAL_0: 25;

          consider h be Nat such that

           A6: n = (n2 + h) by NAT_1: 10, XXREAL_0: 25;

          reconsider n as Nat by TARSKI: 1;

          consider k be Nat such that

           A7: x in (C . (n + k)) by A2, Th5;



           A8: x in ((A . (n + k)) \/ (B . (n + k))) by A1, A7;

          per cases by A8, XBOOLE_0:def 3;

            suppose x in (A . (n + k));

            then x in (A . (n1 + (g + k))) by A5;

            hence thesis by A3;

          end;

            suppose x in (B . (n + k));

            then x in (B . (n2 + (h + k))) by A6;

            hence thesis by A4;

          end;

        end;

        then x in ( lim_sup A) or x in ( lim_sup B) by Th5;

        hence thesis by XBOOLE_0:def 3;

      end;

      thus (( lim_sup A) \/ ( lim_sup B)) c= ( lim_sup C)

      proof

        let x be object;

        assume

         A9: x in (( lim_sup A) \/ ( lim_sup B));

        per cases by A9, XBOOLE_0:def 3;

          suppose

           A10: x in ( lim_sup A);

          for n be Nat holds ex k be Nat st x in (C . (n + k))

          proof

            let n be Nat;

            consider k be Nat such that

             A11: x in (A . (n + k)) by A10, Th5;

            take k;

            x in ((A . (n + k)) \/ (B . (n + k))) by A11, XBOOLE_0:def 3;

            hence thesis by A1;

          end;

          hence thesis by Th5;

        end;

          suppose

           A12: x in ( lim_sup B);

          for n be Nat holds ex k be Nat st x in (C . (n + k))

          proof

            let n be Nat;

            consider k be Nat such that

             A13: x in (B . (n + k)) by A12, Th5;

            take k;

            x in ((A . (n + k)) \/ (B . (n + k))) by A13, XBOOLE_0:def 3;

            hence thesis by A1;

          end;

          hence thesis by Th5;

        end;

      end;

    end;

    theorem :: KURATO_0:12

    for X be set, A,B,C be SetSequence of X st for n be Nat holds (C . n) = ((A . n) \/ (B . n)) holds (( lim_inf A) \/ ( lim_inf B)) c= ( lim_inf C)

    proof

      let X be set, A,B,C be SetSequence of X;

      assume

       A1: for n be Nat holds (C . n) = ((A . n) \/ (B . n));

      let x be object;

      assume

       A2: x in (( lim_inf A) \/ ( lim_inf B));

      per cases by A2, XBOOLE_0:def 3;

        suppose x in ( lim_inf A);

        then

        consider n be Nat such that

         A3: for k be Nat holds x in (A . (n + k)) by Th4;

        for k be Nat holds x in (C . (n + k))

        proof

          let k be Nat;

          x in (A . (n + k)) by A3;

          then x in ((A . (n + k)) \/ (B . (n + k))) by XBOOLE_0:def 3;

          hence thesis by A1;

        end;

        hence thesis by Th4;

      end;

        suppose x in ( lim_inf B);

        then

        consider n be Nat such that

         A4: for k be Nat holds x in (B . (n + k)) by Th4;

        for k be Nat holds x in (C . (n + k))

        proof

          let k be Nat;

          x in (B . (n + k)) by A4;

          then x in ((A . (n + k)) \/ (B . (n + k))) by XBOOLE_0:def 3;

          hence thesis by A1;

        end;

        hence thesis by Th4;

      end;

    end;

    theorem :: KURATO_0:13

    for X be set, A,B,C be SetSequence of X st (for n be Nat holds (C . n) = ((A . n) /\ (B . n))) holds ( lim_sup C) c= (( lim_sup A) /\ ( lim_sup B))

    proof

      let X be set, A,B,C be SetSequence of X;

      assume

       A1: for n be Nat holds (C . n) = ((A . n) /\ (B . n));

      let x be object;

      assume

       A2: x in ( lim_sup C);

      for n be Nat holds ex k be Nat st x in (B . (n + k))

      proof

        let n be Nat;

        consider k be Nat such that

         A3: x in (C . (n + k)) by A2, Th5;

        take k;

        x in ((A . (n + k)) /\ (B . (n + k))) by A1, A3;

        hence thesis by XBOOLE_0:def 4;

      end;

      then

       A4: x in ( lim_sup B) by Th5;

      for n be Nat holds ex k be Nat st x in (A . (n + k))

      proof

        let n be Nat;

        consider k be Nat such that

         A5: x in (C . (n + k)) by A2, Th5;

        take k;

        x in ((A . (n + k)) /\ (B . (n + k))) by A1, A5;

        hence thesis by XBOOLE_0:def 4;

      end;

      then x in ( lim_sup A) by Th5;

      hence thesis by A4, XBOOLE_0:def 4;

    end;

    theorem :: KURATO_0:14



     Th14: for X be set, A be SetSequence of X, B be Subset of X st (for n be Nat holds (A . n) = B) holds ( lim_sup A) = B

    proof

      let X be set, A be SetSequence of X, B be Subset of X;

      assume

       A1: for n be Nat holds (A . n) = B;

      thus ( lim_sup A) c= B

      proof

        let x be object;

        assume x in ( lim_sup A);

        then ex k be Nat st x in (A . ( 0 qua Nat + k)) by Th5;

        hence thesis by A1;

      end;

      thus B c= ( lim_sup A)

      proof

        let x be object;

        assume

         A2: x in B;

        for m be Nat holds ex k be Nat st x in (A . (m + k))

        proof

          let m be Nat;

          take 0 ;

          thus thesis by A1, A2;

        end;

        hence thesis by Th5;

      end;

    end;

    theorem :: KURATO_0:15



     Th15: for X be set, A be SetSequence of X, B be Subset of X st (for n be Nat holds (A . n) = B) holds ( lim_inf A) = B

    proof

      let X be set, A be SetSequence of X, B be Subset of X;

      assume

       A1: for n be Nat holds (A . n) = B;

      thus ( lim_inf A) c= B

      proof

        let x be object;

        assume x in ( lim_inf A);

        then

        consider m be Nat such that

         A2: for k be Nat holds x in (A . (m + k)) by Th4;

        x in (A . (m + 0 qua Nat)) by A2;

        hence thesis by A1;

      end;

      thus B c= ( lim_inf A)

      proof

        let x be object;

        assume

         A3: x in B;

        ex m be Nat st for k be Nat holds x in (A . (m + k))

        proof

          take 0 ;

          let k be Nat;

          thus thesis by A1, A3;

        end;

        hence thesis by Th4;

      end;

    end;

    theorem :: KURATO_0:16

    for X be set, A,B be SetSequence of X, C be Subset of X st (for n be Nat holds (B . n) = (C \+\ (A . n))) holds (C \+\ ( lim_inf A)) c= ( lim_sup B)

    proof

      let X be set, A,B be SetSequence of X, C be Subset of X;

      assume

       A1: for n be Nat holds (B . n) = (C \+\ (A . n));

      let x be object;

      assume

       A2: x in (C \+\ ( lim_inf A));

      per cases by A2, XBOOLE_0: 1;

        suppose

         A3: x in C & not x in ( lim_inf A);

        for n be Nat holds ex k be Nat st x in (B . (n + k))

        proof

          let n be Nat;

          consider k be Nat such that

           A4: not x in (A . (n + k)) by A3, Th4;

          take k;

          x in (C \+\ (A . (n + k))) by A3, A4, XBOOLE_0: 1;

          hence thesis by A1;

        end;

        hence thesis by Th5;

      end;

        suppose

         A5: not x in C & x in ( lim_inf A);

        then

        consider n be Nat such that

         A6: for k be Nat holds x in (A . (n + k)) by Th4;

        for m be Nat holds ex k be Nat st x in (B . (m + k))

        proof

          let m be Nat;

          take k = n;

          x in (A . (m + k)) by A6;

          then x in (C \+\ (A . (m + k))) by A5, XBOOLE_0: 1;

          hence thesis by A1;

        end;

        hence thesis by Th5;

      end;

    end;

    theorem :: KURATO_0:17

    for X be set, A,B be SetSequence of X, C be Subset of X st (for n be Nat holds (B . n) = (C \+\ (A . n))) holds (C \+\ ( lim_sup A)) c= ( lim_sup B)

    proof

      let X be set, A,B be SetSequence of X, C be Subset of X;

      assume

       A1: for n be Nat holds (B . n) = (C \+\ (A . n));

      let x be object;

      assume

       A2: x in (C \+\ ( lim_sup A));

      per cases by A2, XBOOLE_0: 1;

        suppose

         A3: x in C & not x in ( lim_sup A);

        then

        consider n be Nat such that

         A4: for k be Nat holds not x in (A . (n + k)) by Th5;

        for m be Nat holds ex k be Nat st x in (B . (m + k))

        proof

          let m be Nat;

          take k = n;

           not x in (A . (m + k)) by A4;

          then x in (C \+\ (A . (m + k))) by A3, XBOOLE_0: 1;

          hence thesis by A1;

        end;

        hence thesis by Th5;

      end;

        suppose

         A5: not x in C & x in ( lim_sup A);

        for m be Nat holds ex k be Nat st x in (B . (m + k))

        proof

          let m be Nat;

          consider k be Nat such that

           A6: x in (A . (m + k)) by A5, Th5;

          take k;

          x in (C \+\ (A . (m + k))) by A5, A6, XBOOLE_0: 1;

          hence thesis by A1;

        end;

        hence thesis by Th5;

      end;

    end;

    begin

    theorem :: KURATO_0:18



     Th18: for f be Function st (for i be Nat holds (f . (i + 1)) c= (f . i)) holds for i,j be Nat st i <= j holds (f . j) c= (f . i)

    proof

      let f be Function;

      assume

       A1: for i be Nat holds (f . (i + 1)) c= (f . i);

      let i,j be Nat;

      defpred P[ Nat] means (i + $1) <= j implies (f . (i + $1)) c= (f . i);

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];



         A4: ((i + k) + 1) = (i + (k + 1));

        then (f . (i + (k + 1))) c= (f . (i + k)) by A1;

        hence P[(k + 1)] by A4, A3, NAT_1: 13, XBOOLE_1: 1;

      end;



       A5: P[ 0 ];



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

      assume i <= j;

      then

      consider k be Nat such that

       A7: (i + k) = j by NAT_1: 10;

      thus thesis by A6, A7;

    end;

    definition

      let T be set, S be SetSequence of T;

      :: original: non-ascending

      redefine

      :: KURATO_0:def3

      attr S is non-ascending means for i be Nat holds (S . (i + 1)) c= (S . i);

      compatibility

      proof

        thus S is non-ascending implies for i be Nat holds (S . (i + 1)) c= (S . i)

        proof

          assume

           A1: S is non-ascending;

          let i be Nat;

          i <= (i + 1) by NAT_1: 13;

          hence thesis by A1, PROB_1:def 4;

        end;

        assume for i be Nat holds (S . (i + 1)) c= (S . i);

        then

         A2: for i,j be Nat st i <= j holds (S . j) c= (S . i) by Th18;

        for i,j be Nat st i <= j holds (S . j) c= (S . i) by A2;

        hence thesis by PROB_1:def 4;

      end;

      :: original: non-descending

      redefine

      :: KURATO_0:def4

      attr S is non-descending means for i be Nat holds (S . i) c= (S . (i + 1));

      compatibility

      proof

        thus S is non-descending implies for i be Nat holds (S . i) c= (S . (i + 1))

        proof

          assume

           A3: S is non-descending;

          let i be Nat;

          i <= (i + 1) by NAT_1: 13;

          hence thesis by A3, PROB_1:def 5;

        end;

        assume for i be Nat holds (S . i) c= (S . (i + 1));

        then

         A4: for i,j be Nat st i <= j holds (S . i) c= (S . j) by MEASURE2: 18;

        for i,j be Nat st i <= j holds (S . i) c= (S . j) by A4;

        hence thesis by PROB_1:def 5;

      end;

    end

    theorem :: KURATO_0:19



     Th19: for T be set, F be SetSequence of T, x be object st F is non-ascending & ex k be Nat st for n be Nat st n > k holds x in (F . n) holds x in ( meet F)

    proof

      let T be set, F be SetSequence of T, x be object;

      assume

       A1: F is non-ascending;

      given k be Nat such that

       A2: for n be Nat st n > k holds x in (F . n);

      (k + 1) > k by NAT_1: 13;

      then

       A3: x in (F . (k + 1)) by A2;

      assume not x in ( meet F);

      then not x in ( meet ( rng F)) by FUNCT_6:def 4;

      then

      consider Y be set such that

       A4: Y in ( rng F) and

       A5: not x in Y by SETFAM_1:def 1;

      consider y be object such that

       A6: y in ( dom F) and

       A7: Y = (F . y) by A4, FUNCT_1:def 3;

      reconsider y as Nat by A6;

      per cases ;

        suppose y > k;

        hence thesis by A2, A5, A7;

      end;

        suppose y <= k;

        then (F . k) c= (F . y) by A1, PROB_1:def 4;

        then

         A8: not x in (F . k) by A5, A7;

        (F . (k + 1)) c= (F . k) by A1;

        hence thesis by A3, A8;

      end;

    end;

    theorem :: KURATO_0:20

    for T be set, F be SetSequence of T st F is non-ascending holds ( lim_inf F) = ( meet F)

    proof

      let T be set, F be SetSequence of T;

      assume

       A1: F is non-ascending;

      thus ( lim_inf F) c= ( meet F)

      proof

        let x be object;

        assume x in ( lim_inf F);

        then

        consider n be Nat such that

         A2: for k be Nat holds x in (F . (n + k)) by Th4;

        for k be Nat st k > n holds x in (F . k)

        proof

          let k be Nat;

          assume k > n;

          then

          consider h be Nat such that

           A3: k = (n + h) by NAT_1: 10;

          thus thesis by A2, A3;

        end;

        hence thesis by A1, Th19;

      end;

      thus thesis by Th7;

    end;

    theorem :: KURATO_0:21

    for T be set, F be SetSequence of T st F is non-descending holds ( lim_sup F) = ( Union F)

    proof

      let T be set, F be SetSequence of T;

      assume

       A1: F is non-descending;

      thus ( lim_sup F) c= ( Union F) by Th8;

      let x be object;

      assume x in ( Union F);

      then

      consider n be Nat such that

       A2: x in (F . n) by PROB_1: 12;

      assume not x in ( lim_sup F);

      then

      consider m be Nat such that

       A3: for k be Nat holds not x in (F . (m + k)) by Th5;



       A4: not x in (F . (m + 0 qua Nat)) by A3;

      per cases ;

        suppose n <= m;

        then (F . n) c= (F . m) by A1, PROB_1:def 5;

        hence thesis by A2, A4;

      end;

        suppose n > m;

        then

        consider h be Nat such that

         A5: n = (m + h) by NAT_1: 10;

        thus thesis by A2, A3, A5;

      end;

    end;

    begin

    definition

      let T be set, S be SetSequence of T;

      :: KURATO_0:def5

      attr S is convergent means

      : Def5: ( lim_sup S) = ( lim_inf S);

    end

    theorem :: KURATO_0:22

    for T be set, S be SetSequence of T st S is constant holds ( the_value_of S) is Subset of T

    proof

      let T be set, S be SetSequence of T;

      assume S is constant;

      then

      consider x be set such that

       A1: x in ( dom S) and

       A2: ( the_value_of S) = (S . x) by FUNCT_1:def 12;

      reconsider n = x as Element of NAT by A1;

      (S . n) in ( bool T);

      hence thesis by A2;

    end;

    registration

      let T be set;

      cluster constant -> convergent non-descending non-ascending for SetSequence of T;

      coherence

      proof

        let S be SetSequence of T;

        assume S is constant;

        then

        consider A be Subset of T such that

         A1: for n be Nat holds (S . n) = A by VALUED_0:def 18;

         A2:

        now

          let n be Nat;

          (S . n) = A by A1;

          hence (S . (n + 1)) c= (S . n) by A1;

        end;

         A3:

        now

          let n be Nat;

          (S . n) = A by A1;

          hence (S . n) c= (S . (n + 1)) by A1;

        end;

        ( lim_sup S) = A & ( lim_inf S) = A by A1, Th14, Th15;

        hence thesis by A3, A2;

      end;

    end

    registration

      let T be set;

      cluster constant non empty for SetSequence of T;

      existence

      proof

        reconsider E = ( NAT --> ( {} T)) as SetSequence of T;

        E is constant;

        hence thesis;

      end;

    end

    notation

      let T be set, S be convergent SetSequence of T;

      synonym Lim_K S for lim_sup S;

    end

    theorem :: KURATO_0:23

    for X be set, F be convergent SetSequence of X, x be set holds x in ( Lim_K F) iff ex n be Nat st for k be Nat holds x in (F . (n + k))

    proof

      let X be set, F be convergent SetSequence of X, x be set;

      ( Lim_K F) = ( lim_inf F) by Def5;

      hence thesis by Th4;

    end;