waybel28.miz

    begin

    theorem :: WAYBEL28:1



     Th1: for L be complete LATTICE, N be net of L holds ( inf N) <= ( lim_inf N)

    proof

      let L be complete LATTICE, N be net of L;

      set X = the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j1 },L)) where j1 be Element of N;

      X c= the carrier of L

      proof

        let x be object;

        assume x in X;

        then ex j1 be Element of N st x = ( "/\" ({ (N . i) where i be Element of N : i >= j1 },L));

        hence thesis;

      end;

      then

      reconsider X as Subset of L;

      set j = the Element of N;



       A1: { (N . i) where i be Element of N : i >= j } c= ( rng the mapping of N)

      proof

        let x be object;



         A2: ( dom the mapping of N) = the carrier of N by FUNCT_2:def 1;

        assume x in { (N . i) where i be Element of N : i >= j };

        then

        consider i be Element of N such that

         A3: x = (N . i) and i >= j;

        x = (the mapping of N . i) by A3, WAYBEL_0:def 8;

        hence thesis by A2, FUNCT_1:def 3;

      end;

      reconsider X as Subset of L;

      set x = ( "/\" ({ (N . i) where i be Element of N : i >= j },L));

       ex_inf_of ({ (N . i) where i be Element of N : i >= j },L) & ex_inf_of (( rng the mapping of N),L) by YELLOW_0: 17;

      then ( "/\" ({ (N . i) where i be Element of N : i >= j },L)) >= ( "/\" (( rng the mapping of N),L)) by A1, YELLOW_0: 35;

      then x >= ( Inf the mapping of N) by YELLOW_2:def 6;

      then

       A4: ( inf N) <= x by WAYBEL_9:def 2;

       ex_sup_of (X,L) by YELLOW_0: 17;

      then x in X & X is_<=_than ( "\/" (X,L)) by YELLOW_0:def 9;

      then x <= ( "\/" (X,L)) by LATTICE3:def 9;

      hence thesis by A4, YELLOW_0:def 2;

    end;

    theorem :: WAYBEL28:2

    for L be complete LATTICE, N be net of L, x be Element of L holds (for M be subnet of N holds x = ( lim_inf M)) implies (x = ( lim_inf N) & for M be subnet of N holds x >= ( inf M))

    proof

      let L be complete LATTICE, N be net of L, x be Element of L;

      assume

       A1: for M be subnet of N holds x = ( lim_inf M);

      N is subnet of N by YELLOW_6: 14;

      hence x = ( lim_inf N) by A1;

      let M be subnet of N;

      x = ( lim_inf M) by A1;

      hence thesis by Th1;

    end;

    theorem :: WAYBEL28:3



     Th3: for L be complete LATTICE, N be net of L, x be Element of L st N in ( NetUniv L) holds (for M be subnet of N st M in ( NetUniv L) holds x = ( lim_inf M)) implies (x = ( lim_inf N) & for M be subnet of N st M in ( NetUniv L) holds x >= ( inf M))

    proof

      let L be complete LATTICE, N be net of L, x be Element of L;

      assume

       A1: N in ( NetUniv L);

      assume

       A2: for M be subnet of N st M in ( NetUniv L) holds x = ( lim_inf M);

      N is subnet of N by YELLOW_6: 14;

      hence x = ( lim_inf N) by A1, A2;

      let M be subnet of N;

      assume M in ( NetUniv L);

      then x = ( lim_inf M) by A2;

      hence thesis by Th1;

    end;

    definition

      let N be non empty RelStr;

      let f be Function of N, N;

      :: WAYBEL28:def1

      attr f is greater_or_equal_to_id means

      : Def1: for j be Element of N holds j <= (f . j);

    end

    theorem :: WAYBEL28:4



     Th4: for N be reflexive non empty RelStr holds ( id N) is greater_or_equal_to_id

    proof

      let N be reflexive non empty RelStr;

      let j be Element of N;

      reconsider n = j as Element of N;

      n <= (( id N) . n);

      hence thesis;

    end;

    theorem :: WAYBEL28:5



     Th5: for N be directed non empty RelStr, x,y be Element of N holds ex z be Element of N st x <= z & y <= z

    proof

      let N be directed non empty RelStr, x,y be Element of N;

      ( [#] N) is directed by WAYBEL_0:def 6;

      then ex z be Element of N st z in ( [#] N) & x <= z & y <= z by WAYBEL_0:def 1;

      hence thesis;

    end;

    registration

      let N be directed non empty RelStr;

      cluster greater_or_equal_to_id for Function of N, N;

      existence

      proof

        defpred P[ object, object] means for n,m be Element of N st $1 = n & $2 = m holds n <= m;



         A1: for e be object st e in the carrier of N holds ex u be object st u in the carrier of N & P[e, u]

        proof

          let e be object;

          assume e in the carrier of N;

          then

          reconsider e9 = e as Element of N;

          consider u9 be Element of N such that

           A2: e9 <= u9 and e9 <= u9 by Th5;

          take u9;

          thus u9 in the carrier of N;

          let n,m be Element of N;

          assume e = n & u9 = m;

          hence thesis by A2;

        end;

        consider p be Function such that

         A3: ( dom p) = the carrier of N & ( rng p) c= the carrier of N and

         A4: for e be object st e in the carrier of N holds P[e, (p . e)] from FUNCT_1:sch 6( A1);

        reconsider p as Function of N, N by A3, FUNCT_2: 2;

        take p;

        let j be Element of N;

        thus thesis by A4;

      end;

    end

    registration

      let N be reflexive non empty RelStr;

      cluster greater_or_equal_to_id for Function of N, N;

      existence

      proof

        take ( id N);

        thus thesis by Th4;

      end;

    end

    definition

      let L be non empty 1-sorted;

      let N be non empty NetStr over L;

      let f be Function of N, N;

      :: WAYBEL28:def2

      func N * f -> strict non empty NetStr over L means

      : Def2: the RelStr of it = the RelStr of N & the mapping of it = (the mapping of N * f);

      existence

      proof

        take NetStr (# the carrier of N, the InternalRel of N, (the mapping of N * f) #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: WAYBEL28:6



     Th6: for L be non empty 1-sorted, N be non empty NetStr over L, f be Function of N, N holds the carrier of (N * f) = the carrier of N

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L, f be Function of N, N;

       the RelStr of (N * f) = the RelStr of N by Def2;

      hence thesis;

    end;

    theorem :: WAYBEL28:7



     Th7: for L be non empty 1-sorted, N be non empty NetStr over L, f be Function of N, N holds (N * f) = NetStr (# the carrier of N, the InternalRel of N, (the mapping of N * f) #)

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L, f be Function of N, N;

       the RelStr of (N * f) = the RelStr of N by Def2;

      hence thesis by Def2;

    end;

    theorem :: WAYBEL28:8



     Th8: for L be non empty 1-sorted, N be transitive directed non empty RelStr, f be Function of the carrier of N, the carrier of L holds NetStr (# the carrier of N, the InternalRel of N, f #) is net of L

    proof

      let L be non empty 1-sorted, N be transitive directed non empty RelStr, f be Function of the carrier of N, the carrier of L;

      set N2 = NetStr (# the carrier of N, the InternalRel of N, f #);



       A1: the RelStr of N = the RelStr of N2;

      ( [#] N) is directed by WAYBEL_0:def 6;

      then ( [#] N2) is directed by A1, WAYBEL_0: 3;

      hence thesis by A1, WAYBEL_0:def 6, WAYBEL_8: 13;

    end;

    registration

      let L be non empty 1-sorted, N be transitive directed non empty RelStr, f be Function of the carrier of N, the carrier of L;

      cluster NetStr (# the carrier of N, the InternalRel of N, f #) -> transitive directed non empty;

      correctness by Th8;

    end

    theorem :: WAYBEL28:9



     Th9: for L be non empty 1-sorted, N be net of L, p be Function of N, N holds (N * p) is net of L

    proof

      let L be non empty 1-sorted, N be net of L, p be Function of N, N;

      (N * p) = NetStr (# the carrier of N, the InternalRel of N, (the mapping of N * p) #) by Th7;

      hence thesis;

    end;

    registration

      let L be non empty 1-sorted, N be net of L;

      let p be Function of N, N;

      cluster (N * p) -> transitive directed;

      correctness by Th9;

    end

    theorem :: WAYBEL28:10



     Th10: for L be non empty 1-sorted, N be net of L, p be Function of N, N st N in ( NetUniv L) holds (N * p) in ( NetUniv L)

    proof

      let L be non empty 1-sorted, N be net of L, p be Function of N, N;

      assume N in ( NetUniv L);

      then

       A1: ex N1 be strict net of L st N1 = N & the carrier of N1 in ( the_universe_of the carrier of L) by YELLOW_6:def 11;

      the carrier of (N * p) = the carrier of N by Th6;

      hence thesis by A1, YELLOW_6:def 11;

    end;

    theorem :: WAYBEL28:11

    for L be non empty 1-sorted, N,M be net of L st the NetStr of N = the NetStr of M holds M is subnet of N

    proof

      let L be non empty 1-sorted, N,M be net of L;

      assume

       A1: the NetStr of N = the NetStr of M;



       A2: N is subnet of N by YELLOW_6: 14;

      ex f be Function of M, N st the mapping of M = (the mapping of N * f) & for m be Element of N holds ex n be Element of M st for p be Element of M st n <= p holds m <= (f . p)

      proof

        consider f be Function of N, N such that

         A3: the mapping of N = (the mapping of N * f) and

         A4: for m be Element of N holds ex n be Element of N st for p be Element of N st n <= p holds m <= (f . p) by A2, YELLOW_6:def 9;

        reconsider f2 = f as Function of M, N by A1;

        take f2;

        thus the mapping of M = (the mapping of N * f2) by A1, A3;

        let m be Element of N;

        consider n be Element of N such that

         A5: for p be Element of N st n <= p holds m <= (f . p) by A4;

        reconsider n2 = n as Element of M by A1;

        take n2;

        let p be Element of M;

        reconsider p1 = p as Element of N by A1;

        assume n2 <= p;

        then [n2, p] in the InternalRel of M by ORDERS_2:def 5;

        then n <= p1 by A1, ORDERS_2:def 5;

        hence thesis by A5;

      end;

      hence thesis by YELLOW_6:def 9;

    end;

    theorem :: WAYBEL28:12



     Th12: for L be non empty 1-sorted, N be net of L, p be greater_or_equal_to_id Function of N, N holds (N * p) is subnet of N

    proof

      let L be non empty 1-sorted;

      let N be net of L;

      let p be greater_or_equal_to_id Function of N, N;

      ex f be Function of (N * p), N st the mapping of (N * p) = (the mapping of N * f) & for m be Element of N holds ex n be Element of (N * p) st for k be Element of (N * p) st n <= k holds m <= (f . k)

      proof

        the carrier of (N * p) = the carrier of N by Th6;

        then

        reconsider f = p as Function of (N * p), N;

        take f;

        thus the mapping of (N * p) = (the mapping of N * f) by Def2;

        let m be Element of N;

        reconsider n = m as Element of (N * p) by Th6;

        take n;

        let k be Element of (N * p);

        assume

         A1: n <= k;

        reconsider k1 = k as Element of N by Th6;



         A2: k1 <= (p . k1) by Def1;

         the RelStr of (N * p) = the RelStr of N by Def2;

        then m <= k1 by A1, YELLOW_0: 1;

        hence thesis by A2, YELLOW_0:def 2;

      end;

      hence thesis by YELLOW_6:def 9;

    end;

    definition

      let L be non empty 1-sorted;

      let N be net of L;

      let p be greater_or_equal_to_id Function of N, N;

      :: original: *

      redefine

      func N * p -> strict subnet of N ;

      correctness by Th12;

    end

    theorem :: WAYBEL28:13

    for L be complete LATTICE, N be net of L, x be Element of L st N in ( NetUniv L) holds (x = ( lim_inf N) & for M be subnet of N st M in ( NetUniv L) holds x >= ( inf M)) implies x = ( lim_inf N) & for p be greater_or_equal_to_id Function of N, N holds x >= ( inf (N * p)) by Th10;

    theorem :: WAYBEL28:14



     Th14: for L be complete LATTICE, N be net of L, x be Element of L holds (x = ( lim_inf N) & for p be greater_or_equal_to_id Function of N, N holds x >= ( inf (N * p))) implies for M be subnet of N holds x = ( lim_inf M)

    proof

      let L be complete LATTICE, N be net of L, x be Element of L;

      assume that

       A1: x = ( lim_inf N) and

       A2: for p be greater_or_equal_to_id Function of N, N holds x >= ( inf (N * p));

      let M be subnet of N;

      consider f be Function of M, N such that

       A3: the mapping of M = (the mapping of N * f) and

       A4: for j be Element of N holds ex k be Element of M st for m be Element of M st k <= m holds j <= (f . m) by YELLOW_6:def 9;



       A5: x <= ( lim_inf M) by A1, WAYBEL21: 37;



       A6: for k0 be Element of M holds ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L)) <= x

      proof

        let k0 be Element of M;

        defpred P[ object, object] means for j be Element of N, v,v9 be Element of M st $1 = j & $2 = v & v9 >= v holds v >= k0 & (f . v9) >= j & (f . v) >= j;



         A7: for j be Element of N holds ex v be Element of M st v >= k0 & for v9 be Element of M st v9 >= v holds (f . v9) >= j & (f . v) >= j

        proof

          let j be Element of N;

          consider w be Element of M such that

           A8: for w9 be Element of M st w <= w9 holds j <= (f . w9) by A4;

          consider v be Element of M such that

           A9: v >= k0 and

           A10: v >= w by Th5;

          take v;

          thus v >= k0 by A9;

          let v9 be Element of M;

          assume v9 >= v;

          then v9 >= w by A10, YELLOW_0:def 2;

          hence (f . v9) >= j by A8;

          thus thesis by A8, A10;

        end;



         A11: for e be object st e in the carrier of N holds ex u be object st u in the carrier of M & P[e, u]

        proof

          let e be object;

          assume e in the carrier of N;

          then

          reconsider e9 = e as Element of N;

          consider u be Element of M such that

           A12: u >= k0 and

           A13: for v9 be Element of M st v9 >= u holds (f . v9) >= e9 & (f . u) >= e9 by A7;

          take u;

          thus u in the carrier of M;

          let j be Element of N, v,v9 be Element of M;

          assume that

           A14: e = j and

           A15: u = v and

           A16: v9 >= v;

          thus v >= k0 by A12, A15;

          thus (f . v9) >= j by A13, A14, A15, A16;

          thus thesis by A13, A14, A15, A16;

        end;

        consider g be Function such that

         A17: ( dom g) = the carrier of N and

         A18: ( rng g) c= the carrier of M and

         A19: for e be object st e in the carrier of N holds P[e, (g . e)] from FUNCT_1:sch 6( A11);

        reconsider g as Function of the carrier of N, the carrier of M by A17, A18, FUNCT_2: 2;



         A20: for j be Element of N holds (g . j) >= k0

        proof

          let j be Element of N;

          reconsider v = (g . j) as Element of M;

          ex v9 be Element of M st v9 >= v & v9 >= v by Th5;

          hence thesis by A19;

        end;

        reconsider g as Function of N, M;

        reconsider p = (f * g) as Function of N, N;

        for j be Element of N holds j <= (p . j)

        proof

          let j be Element of N;

          reconsider v = (g . j) as Element of M;

          ( [#] M) is directed by WAYBEL_0:def 6;

          then ex v9 be Element of M st v9 in ( [#] M) & v <= v9 & v <= v9 by WAYBEL_0:def 1;

          then j <= (f . (g . j)) by A19;

          hence thesis by A17, FUNCT_1: 13;

        end;

        then

        reconsider p as greater_or_equal_to_id Function of N, N by Def1;



         A21: the set of all ((N * p) . j) where j be Element of (N * p) c= { (M . k) where k be Element of M : k >= k0 }

        proof

          let y be object;

          assume y in the set of all ((N * p) . j) where j be Element of (N * p);

          then

          consider j be Element of (N * p) such that

           A22: y = ((N * p) . j);

          reconsider j9 = j as Element of N by Th6;



           A23: the carrier of (N * p) = the carrier of N by Th6;

          y = (the mapping of (N * p) . j) by A22, WAYBEL_0:def 8

          .= ((the mapping of N * (f * g)) . j) by Def2

          .= ((the mapping of M * g) . j) by A3, RELAT_1: 36

          .= (the mapping of M . (g . j)) by A17, A23, FUNCT_1: 13;

          then

           A24: y = (M . (g . j9)) by WAYBEL_0:def 8;

          (g . j9) >= k0 by A20;

          hence thesis by A24;

        end;



         A25: ex_inf_of ( the set of all ((N * p) . j) where j be Element of (N * p),L) & ex_inf_of ({ (M . k) where k be Element of M : k >= k0 },L) by YELLOW_0: 17;



         A26: ( dom the mapping of (N * p)) = the carrier of (N * p) by FUNCT_2:def 1;



         A27: ( rng the mapping of (N * p)) = the set of all ((N * p) . j) where j be Element of (N * p)

        proof

          thus ( rng the mapping of (N * p)) c= the set of all ((N * p) . j) where j be Element of (N * p)

          proof

            let y be object;

            assume y in ( rng the mapping of (N * p));

            then

            consider j1 be object such that

             A28: j1 in ( dom the mapping of (N * p)) and

             A29: (the mapping of (N * p) . j1) = y by FUNCT_1:def 3;

            reconsider j1 as Element of (N * p) by A28;

            y = ((N * p) . j1) by A29, WAYBEL_0:def 8;

            hence thesis;

          end;

          let y be object;

          assume y in the set of all ((N * p) . j) where j be Element of (N * p);

          then

          consider j be Element of (N * p) such that

           A30: y = ((N * p) . j);

          y = (the mapping of (N * p) . j) by A30, WAYBEL_0:def 8;

          hence thesis by A26, FUNCT_1:def 3;

        end;



         A31: ( inf (N * p)) <= x by A2;

        ( inf (N * p)) = ( Inf the mapping of (N * p)) by WAYBEL_9:def 2

        .= ( "/\" ( the set of all ((N * p) . j) where j be Element of (N * p),L)) by A27, YELLOW_2:def 6;

        then ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L)) <= ( inf (N * p)) by A25, A21, YELLOW_0: 35;

        hence thesis by A31, YELLOW_0:def 2;

      end;

      for b be Element of L st b in the set of all ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L)) where k0 be Element of M holds b <= x

      proof

        let b be Element of L;

        assume b in the set of all ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L)) where k0 be Element of M;

        then ex k0 be Element of M st b = ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L));

        hence thesis by A6;

      end;

      then

       A32: x is_>=_than the set of all ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L)) where k0 be Element of M by LATTICE3:def 9;

       ex_sup_of ( the set of all ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L)) where k0 be Element of M,L) by YELLOW_0: 17;

      then ( "\/" ( the set of all ( "/\" ({ (M . k) where k be Element of M : k >= k0 },L)) where k0 be Element of M,L)) <= x by A32, YELLOW_0:def 9;

      hence thesis by A5, ORDERS_2: 2;

    end;

    definition

      let L be non empty RelStr;

      :: WAYBEL28:def3

      func lim_inf-Convergence L -> Convergence-Class of L means

      : Def3: for N be net of L st N in ( NetUniv L) holds for x be Element of L holds [N, x] in it iff for M be subnet of N holds x = ( lim_inf M);

      existence

      proof

        defpred P[ set, set] means ex N be strict net of L st $1 = N & for M be subnet of N holds $2 = ( lim_inf M);

        consider C be Relation of ( NetUniv L), the carrier of L such that

         A1: for N9 be Element of ( NetUniv L), x be Element of L holds [N9, x] in C iff P[N9, x] from RELSET_1:sch 2;

        reconsider C as Convergence-Class of L by YELLOW_6:def 18;

        take C;

        let N be net of L;

        assume N in ( NetUniv L);

        then

        reconsider N1 = N as Element of ( NetUniv L);

        let x be Element of L;

        thus [N, x] in C implies for M be subnet of N holds x = ( lim_inf M)

        proof

          assume

           A2: [N, x] in C;

          let M be subnet of N;

          ex N2 be strict net of L st N1 = N2 & for M be subnet of N2 holds x = ( lim_inf M) by A1, A2;

          hence thesis;

        end;



         A3: ex N2 be strict net of L st N2 = N1 & the carrier of N2 in ( the_universe_of the carrier of L) by YELLOW_6:def 11;

        assume for M be subnet of N holds x = ( lim_inf M);

        hence thesis by A1, A3;

      end;

      uniqueness

      proof

        let C1,C2 be Convergence-Class of L such that

         A4: for N be net of L st N in ( NetUniv L) holds for x be Element of L holds [N, x] in C1 iff for M be subnet of N holds x = ( lim_inf M) and

         A5: for N be net of L st N in ( NetUniv L) holds for x be Element of L holds [N, x] in C2 iff for M be subnet of N holds x = ( lim_inf M);

        let Ns,xs be object;



         A6: C1 c= [:( NetUniv L), the carrier of L:] by YELLOW_6:def 18;

        thus [Ns, xs] in C1 implies [Ns, xs] in C2

        proof

          assume

           A7: [Ns, xs] in C1;

          then

          reconsider x = xs as Element of L by A6, ZFMISC_1: 87;

          Ns in ( NetUniv L) by A6, A7, ZFMISC_1: 87;

          then

          consider N be strict net of L such that

           A8: N = Ns and the carrier of N in ( the_universe_of the carrier of L) by YELLOW_6:def 11;



           A9: N in ( NetUniv L) by A6, A7, A8, ZFMISC_1: 87;

          then for M be subnet of N holds x = ( lim_inf M) by A4, A7, A8;

          hence thesis by A5, A8, A9;

        end;

        assume

         A10: [Ns, xs] in C2;



         A11: C2 c= [:( NetUniv L), the carrier of L:] by YELLOW_6:def 18;

        then

        reconsider x = xs as Element of L by A10, ZFMISC_1: 87;

        Ns in ( NetUniv L) by A11, A10, ZFMISC_1: 87;

        then

        consider N be strict net of L such that

         A12: N = Ns and the carrier of N in ( the_universe_of the carrier of L) by YELLOW_6:def 11;



         A13: N in ( NetUniv L) by A11, A10, A12, ZFMISC_1: 87;

        then for M be subnet of N holds x = ( lim_inf M) by A5, A10, A12;

        hence thesis by A4, A12, A13;

      end;

    end

    theorem :: WAYBEL28:15

    for L be complete LATTICE, N be net of L, x be Element of L st N in ( NetUniv L) holds [N, x] in ( lim_inf-Convergence L) iff for M be subnet of N st M in ( NetUniv L) holds x = ( lim_inf M)

    proof

      let L be complete LATTICE;

      let N be net of L;

      let x be Element of L;

      assume

       A1: N in ( NetUniv L);

      hence [N, x] in ( lim_inf-Convergence L) implies for M be subnet of N st M in ( NetUniv L) holds x = ( lim_inf M) by Def3;

      assume

       A2: for M be subnet of N st M in ( NetUniv L) holds x = ( lim_inf M);

      then for M be subnet of N st M in ( NetUniv L) holds x >= ( inf M) by A1, Th3;

      then

       A3: for p be greater_or_equal_to_id Function of N, N holds x >= ( inf (N * p)) by A1, Th10;

      x = ( lim_inf N) by A1, A2, Th3;

      then for M be subnet of N holds x = ( lim_inf M) by A3, Th14;

      hence thesis by A1, Def3;

    end;

    theorem :: WAYBEL28:16



     Th16: for L be non empty RelStr, N be constant net of L, M be subnet of N holds M is constant & ( the_value_of N) = ( the_value_of M)

    proof

      let L be non empty RelStr, N be constant net of L, M be subnet of N;

      consider f be Function of M, N such that

       A1: the mapping of M = (the mapping of N * f) and for m be Element of N holds ex n be Element of M st for p be Element of M st n <= p holds m <= (f . p) by YELLOW_6:def 9;

      set y = the Element of ( dom the mapping of M);



       A2: ( dom the mapping of N) = the carrier of N by FUNCT_2:def 1;



      then

       A3: ( the_value_of the mapping of N) = (the mapping of N . (f . y)) by FUNCT_1:def 12

      .= (the mapping of M . y) by A1, FUNCT_1: 12;



       A4: ( dom f) = the carrier of M by FUNCT_2:def 1;

      for n1,n2 be object st n1 in ( dom the mapping of M) & n2 in ( dom the mapping of M) holds (the mapping of M . n1) = (the mapping of M . n2)

      proof

        let n1,n2 be object;

        assume that

         A5: n1 in ( dom the mapping of M) and

         A6: n2 in ( dom the mapping of M);



         A7: (f . n1) in ( rng f) & (f . n2) in ( rng f) by A4, A5, A6, FUNCT_1:def 3;



        thus (the mapping of M . n1) = (the mapping of N . (f . n1)) by A1, A4, A5, FUNCT_1: 13

        .= (the mapping of N . (f . n2)) by A2, A7, FUNCT_1:def 10

        .= (the mapping of M . n2) by A1, A4, A6, FUNCT_1: 13;

      end;

      then

       A8: the mapping of M is constant by FUNCT_1:def 10;

      hence

       A9: M is constant;



      thus ( the_value_of N) = ( the_value_of the mapping of N) by YELLOW_6:def 8

      .= ( the_value_of the mapping of M) by A8, A3, FUNCT_1:def 12

      .= ( the_value_of M) by A9, YELLOW_6:def 8;

    end;

    definition

      let L be non empty RelStr;

      :: WAYBEL28:def4

      func xi L -> Subset-Family of L equals the topology of ( ConvergenceSpace ( lim_inf-Convergence L));

      correctness by YELLOW_6:def 24;

    end

    theorem :: WAYBEL28:17

    for L be complete LATTICE holds ( lim_inf-Convergence L) is (CONSTANTS)

    proof

      let L be complete LATTICE;

      let N be constant net of L;



       A1: for M be subnet of N holds ( the_value_of N) = ( lim_inf M)

      proof

        let M be subnet of N;



         A2: M is constant by Th16;



        thus ( the_value_of N) = ( the_value_of M) by Th16

        .= ( lim_inf M) by A2, WAYBEL11: 23;

      end;

      assume N in ( NetUniv L);

      hence thesis by A1, Def3;

    end;

    theorem :: WAYBEL28:18

    for L be non empty RelStr holds ( lim_inf-Convergence L) is (SUBNETS)

    proof

      let L be non empty RelStr;

      let N be net of L, M be subnet of N;

      assume

       A1: M in ( NetUniv L);

      let x be Element of L;

      assume

       A2: [N, x] in ( lim_inf-Convergence L);

      ( lim_inf-Convergence L) c= [:( NetUniv L), the carrier of L:] by YELLOW_6:def 18;

      then

       A3: N in ( NetUniv L) by A2, ZFMISC_1: 87;

      for M1 be subnet of M holds x = ( lim_inf M1)

      proof

        let M1 be subnet of M;

        reconsider M19 = M1 as subnet of N by YELLOW_6: 15;

        x = ( lim_inf M19) by A2, A3, Def3;

        hence thesis;

      end;

      hence thesis by A1, Def3;

    end;

    theorem :: WAYBEL28:19

    for L be continuous complete LATTICE holds ( lim_inf-Convergence L) is (DIVERGENCE)

    proof

      let L be continuous complete LATTICE;

      let N be net of L, x be Element of L;

      assume that

       A1: N in ( NetUniv L) and

       A2: not [N, x] in ( lim_inf-Convergence L);



       A3: ex N1 be strict net of L st N1 = N & the carrier of N1 in ( the_universe_of the carrier of L) by A1, YELLOW_6:def 11;

       not for M be subnet of N holds x = ( lim_inf M) by A1, A2, Def3;

      then

       A4: not (x = ( lim_inf N) & for p be greater_or_equal_to_id Function of N, N holds x >= ( inf (N * p))) by Th14;



       A5: ( lim_inf-Convergence L) c= [:( NetUniv L), the carrier of L:] by YELLOW_6:def 18;

      per cases by A1, A4, Th10;

        suppose

         A6: not x = ( lim_inf N) & x <= ( lim_inf N);

        reconsider N9 = N as subnet of N by YELLOW_6: 14;

        take N9;

        thus N9 in ( NetUniv L) by A1;

        given M2 be subnet of N9 such that

         A7: [M2, x] in ( lim_inf-Convergence L);



         A8: ( lim_inf N) <= ( lim_inf M2) by WAYBEL21: 37;



         A9: M2 is subnet of M2 by YELLOW_6: 14;

        M2 in ( NetUniv L) by A5, A7, ZFMISC_1: 87;

        then ( lim_inf M2) = x by A7, A9, Def3;

        hence contradiction by A6, A8, YELLOW_0:def 3;

      end;

        suppose not x = ( lim_inf N) & not x <= ( lim_inf N);

        then not x is_S-limit_of N;

        then not [N, x] in ( Scott-Convergence L) by A1, A3, WAYBEL11:def 8;

        then

        consider M be subnet of N such that

         A10: M in ( NetUniv L) and

         A11: not ex M1 be subnet of M st [M1, x] in ( Scott-Convergence L) by A1, YELLOW_6:def 22;

        take M;

        thus M in ( NetUniv L) by A10;

        for M1 be subnet of M holds not [M1, x] in ( lim_inf-Convergence L)

        proof

          let M1 be subnet of M;



           A12: not [M1, x] in ( Scott-Convergence L) by A11;

          assume

           A13: [M1, x] in ( lim_inf-Convergence L);

          then

           A14: M1 in ( NetUniv L) by A5, ZFMISC_1: 87;

          then ex M11 be strict net of L st M11 = M1 & the carrier of M11 in ( the_universe_of the carrier of L) by YELLOW_6:def 11;

          then

           A15: not x is_S-limit_of M1 by A14, A12, WAYBEL11:def 8;

          M1 is subnet of M1 by YELLOW_6: 14;

          then x = ( lim_inf M1) by A13, A14, Def3;

          hence contradiction by A15;

        end;

        hence thesis;

      end;

        suppose not (for M be subnet of N st M in ( NetUniv L) holds x >= ( inf M));

        then

        consider M be subnet of N such that

         A16: M in ( NetUniv L) and

         A17: not x >= ( inf M);

        take M;

        thus M in ( NetUniv L) by A16;

        for M1 be subnet of M holds not [M1, x] in ( lim_inf-Convergence L)

        proof

          let M1 be subnet of M;



           A18: M1 is subnet of M1 by YELLOW_6: 14;



           A19: ( lim_inf M1) >= ( lim_inf M) & ( lim_inf M) >= ( inf M) by Th1, WAYBEL21: 37;

          assume

           A20: [M1, x] in ( lim_inf-Convergence L);

          then M1 in ( NetUniv L) by A5, ZFMISC_1: 87;

          then x = ( lim_inf M1) by A20, A18, Def3;

          hence contradiction by A17, A19, YELLOW_0:def 2;

        end;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL28:20

    for L be non empty RelStr, N,x be set holds [N, x] in ( lim_inf-Convergence L) implies N in ( NetUniv L)

    proof

      let L be non empty RelStr, N,x be set;



       A1: ( lim_inf-Convergence L) c= [:( NetUniv L), the carrier of L:] by YELLOW_6:def 18;

      assume [N, x] in ( lim_inf-Convergence L);

      hence thesis by A1, ZFMISC_1: 87;

    end;

    theorem :: WAYBEL28:21



     Th21: for L be non empty 1-sorted, C1,C2 be Convergence-Class of L holds C1 c= C2 implies the topology of ( ConvergenceSpace C2) c= the topology of ( ConvergenceSpace C1)

    proof

      let L be non empty 1-sorted, C1,C2 be Convergence-Class of L;

      assume

       A1: C1 c= C2;

      let A be object;

      assume A in the topology of ( ConvergenceSpace C2);

      then A in { V where V be Subset of L : for p be Element of L st p in V holds for N be net of L st [N, p] in C2 holds N is_eventually_in V } by YELLOW_6:def 24;

      then

      consider V1 be Subset of L such that

       A2: A = V1 and

       A3: for p be Element of L st p in V1 holds for N be net of L st [N, p] in C2 holds N is_eventually_in V1;

      ex V be Subset of L st A = V & for p be Element of L st p in V holds for N be net of L st [N, p] in C1 holds N is_eventually_in V

      proof

        take V1;

        thus A = V1 by A2;

        let p be Element of L;

        assume

         A4: p in V1;

        let N be net of L;

        assume [N, p] in C1;

        hence thesis by A1, A3, A4;

      end;

      then A in { V where V be Subset of L : for p be Element of L st p in V holds for N be net of L st [N, p] in C1 holds N is_eventually_in V };

      hence thesis by YELLOW_6:def 24;

    end;

    theorem :: WAYBEL28:22



     Th22: for L be non empty reflexive RelStr holds ( lim_inf-Convergence L) c= ( Scott-Convergence L)

    proof

      let L be non empty reflexive RelStr;

      let Ns,xs be object;

      assume

       A1: [Ns, xs] in ( lim_inf-Convergence L);



       A2: ( lim_inf-Convergence L) c= [:( NetUniv L), the carrier of L:] by YELLOW_6:def 18;

      then

      reconsider x = xs as Element of L by A1, ZFMISC_1: 87;

      Ns in ( NetUniv L) by A2, A1, ZFMISC_1: 87;

      then

      consider N be strict net of L such that

       A3: N = Ns and the carrier of N in ( the_universe_of the carrier of L) by YELLOW_6:def 11;



       A4: N in ( NetUniv L) by A2, A1, A3, ZFMISC_1: 87;

      N is subnet of N by YELLOW_6: 14;

      then x = ( lim_inf N) by A1, A3, A4, Def3;

      then x is_S-limit_of N;

      hence thesis by A3, A4, WAYBEL11:def 8;

    end;

    theorem :: WAYBEL28:23



     Th23: for X,Y be set holds X c= Y implies X in ( the_universe_of Y)

    proof

      let X,Y be set;



       A1: Y c= ( the_transitive-closure_of Y) by CLASSES1: 52;

      ( Tarski-Class ( the_transitive-closure_of Y)) is_Tarski-Class_of ( the_transitive-closure_of Y) by CLASSES1:def 4;

      then

       A2: ( the_transitive-closure_of Y) in ( Tarski-Class ( the_transitive-closure_of Y)) by CLASSES1:def 3;

      assume X c= Y;

      then X c= ( the_transitive-closure_of Y) by A1;

      hence thesis by A2, CLASSES1:def 1;

    end;

    theorem :: WAYBEL28:24



     Th24: for L be non empty transitive reflexive RelStr, D be directed non empty Subset of L holds ( Net-Str D) in ( NetUniv L)

    proof

      let L be non empty transitive reflexive RelStr;

      let D be directed non empty Subset of L;

      D in ( the_universe_of the carrier of L) & the carrier of ( Net-Str D) = D by Th23, WAYBEL21: 32;

      hence thesis by YELLOW_6:def 11;

    end;

    theorem :: WAYBEL28:25



     Th25: for L be complete LATTICE, D be directed non empty Subset of L holds for M be subnet of ( Net-Str D) holds ( lim_inf M) = ( sup D)

    proof

      let L be complete LATTICE;

      let D be directed non empty Subset of L;

      for M be subnet of ( Net-Str D) holds ( sup D) >= ( inf M)

      proof

        let M be subnet of ( Net-Str D);

        set i = the Element of M;

        set f = the mapping of M;

        consider g be Function of M, ( Net-Str D) such that

         A1: the mapping of M = (the mapping of ( Net-Str D) * g) and for m be Element of ( Net-Str D) holds ex n be Element of M st for p be Element of M st n <= p holds m <= (g . p) by YELLOW_6:def 9;



         A2: ( dom f) = the carrier of M by FUNCT_2:def 1;

        then (f . i) in ( rng f) by FUNCT_1:def 3;

        then

         A3: ( "/\" (( rng f),L)) <= (f . i) by YELLOW_0: 17, YELLOW_4: 2;

        (g . i) in the carrier of ( Net-Str D);

        then

         A4: (g . i) in D by WAYBEL21: 32;



        then (g . i) = (( id D) . (g . i)) by FUNCT_1: 18

        .= (the mapping of ( Net-Str D) . (g . i)) by WAYBEL21: 32

        .= (f . i) by A1, A2, FUNCT_1: 12;

        then (f . i) <= ( sup D) by A4, YELLOW_2: 22;

        then ( sup D) >= ( "/\" (( rng f),L)) by A3, YELLOW_0:def 2;

        then ( sup D) >= ( Inf the mapping of M) by YELLOW_2:def 6;

        hence thesis by WAYBEL_9:def 2;

      end;

      then ( lim_inf ( Net-Str D)) = ( sup D) & for p be greater_or_equal_to_id Function of ( Net-Str D), ( Net-Str D) holds ( sup D) >= ( inf (( Net-Str D) * p)) by WAYBEL17: 10;

      hence thesis by Th14;

    end;

    theorem :: WAYBEL28:26



     Th26: for L be non empty complete LATTICE, D be directed non empty Subset of L holds [( Net-Str D), ( sup D)] in ( lim_inf-Convergence L)

    proof

      let L be non empty complete LATTICE;

      let D be directed non empty Subset of L;

      ( Net-Str D) in ( NetUniv L) & for M be subnet of ( Net-Str D) holds ( lim_inf M) = ( sup D) by Th24, Th25;

      hence thesis by Def3;

    end;

    theorem :: WAYBEL28:27



     Th27: for L be complete LATTICE, U1 be Subset of L holds U1 in ( xi L) implies U1 is property(S)

    proof

      let L be complete LATTICE;

      let U1 be Subset of L;

      assume U1 in ( xi L);

      then U1 in { V where V be Subset of L : for p be Element of L st p in V holds for N be net of L st [N, p] in ( lim_inf-Convergence L) holds N is_eventually_in V } by YELLOW_6:def 24;

      then

       A1: ex V be Subset of L st U1 = V & for p be Element of L st p in V holds for N be net of L st [N, p] in ( lim_inf-Convergence L) holds N is_eventually_in V;

      let D be non empty directed Subset of L;

      assume

       A2: ( sup D) in U1;

       [( Net-Str D), ( sup D)] in ( lim_inf-Convergence L) by Th26;

      then ( Net-Str D) is_eventually_in U1 by A1, A2;

      then

      consider y be Element of ( Net-Str D) such that

       A3: for x be Element of ( Net-Str D) st y <= x holds (( Net-Str D) . x) in U1 by WAYBEL_0:def 11;



       A4: y in the carrier of ( Net-Str D);

      then y in D by WAYBEL21: 32;

      then

      reconsider y1 = y as Element of L;

      reconsider y1 as Element of L;

      take y1;

      thus y1 in D by A4, WAYBEL21: 32;

      let x1 be Element of L;

      assume that

       A5: x1 in D and

       A6: x1 >= y1;



       A7: ( Net-Str D) is full SubRelStr of L by WAYBEL21: 32;

      reconsider x = x1 as Element of ( Net-Str D) by A5, WAYBEL21: 32;

      reconsider x as Element of ( Net-Str D);

      (( Net-Str D) . x) = (the mapping of ( Net-Str D) . x) by WAYBEL_0:def 8

      .= (( id D) . x) by WAYBEL21: 32

      .= x by A5, FUNCT_1: 18;

      hence thesis by A3, A6, A7, YELLOW_0: 60;

    end;

    theorem :: WAYBEL28:28



     Th28: for L be non empty reflexive RelStr, A be Subset of L holds A in ( sigma L) implies A in ( xi L)

    proof

      let L be non empty reflexive RelStr, A be Subset of L;

      assume

       A1: A in ( sigma L);

      the topology of ( ConvergenceSpace ( Scott-Convergence L)) c= the topology of ( ConvergenceSpace ( lim_inf-Convergence L)) by Th21, Th22;

      hence thesis by A1;

    end;

    theorem :: WAYBEL28:29



     Th29: for L be complete LATTICE, A be Subset of L st A is upper holds A in ( xi L) implies A in ( sigma L)

    proof

      let L be complete LATTICE, A be Subset of L;

      set T = the Scott TopAugmentation of L;



       A1: the RelStr of T = the RelStr of L by YELLOW_9:def 4;

      then

      reconsider A9 = A as Subset of T;

      reconsider A9 as Subset of T;

      assume A is upper;

      then

       A2: A9 is upper by A1, WAYBEL_0: 25;

      assume A in ( xi L);

      then A9 is property(S) by A1, Th27, YELLOW12: 19;

      then A9 is open by A2, WAYBEL11: 15;

      then A9 in the topology of T by PRE_TOPC:def 2;

      hence thesis by YELLOW_9: 51;

    end;

    theorem :: WAYBEL28:30

    for L be complete LATTICE, A be Subset of L st A is lower holds (A ` ) in ( xi L) iff A is closed_under_directed_sups

    proof

      let L be complete LATTICE, A be Subset of L;

      set T = the Scott TopAugmentation of L;

      assume

       A1: A is lower;

      then

      reconsider A1 = A as lower Subset of L;



       A2: the RelStr of L = the RelStr of T by YELLOW_9:def 4;

      then

      reconsider A9 = A as Subset of T;

      reconsider A9 as Subset of T;



       A3: (A1 ` ) is upper;

      thus (A ` ) in ( xi L) implies A is closed_under_directed_sups

      proof

        assume (A ` ) in ( xi L);

        then (A9 ` ) in ( sigma L) by A3, A2, Th29;

        then (A9 ` ) in the topology of T by YELLOW_9: 51;

        then (A9 ` ) is open by PRE_TOPC:def 2;

        then A9 is closed by TOPS_1: 3;

        then A9 is directly_closed by WAYBEL11: 7;

        hence thesis by A2, YELLOW12: 20;

      end;

      assume A is closed_under_directed_sups;

      then

       A4: A9 is directly_closed by A2, YELLOW12: 20;

      A9 is lower by A1, A2, WAYBEL_0: 25;

      then A9 is closed by A4, WAYBEL11: 7;

      then (A9 ` ) is open by TOPS_1: 3;

      then (A9 ` ) in the topology of T by PRE_TOPC:def 2;

      then (A ` ) in ( sigma L) by A2, YELLOW_9: 51;

      hence thesis by Th28;

    end;