waybel17.miz



    begin

    definition

      let S be non empty set;

      let a,b be Element of S;

      :: WAYBEL17:def1

      func (a,b) ,... -> sequence of S means

      : Def1: for i be Element of NAT holds ((ex k be Element of NAT st i = (2 * k)) implies (it . i) = a) & (( not ex k be Element of NAT st i = (2 * k)) implies (it . i) = b);

      existence

      proof

        defpred C[ object] means ex k be Element of NAT st $1 = (2 * k);

        deffunc G( object) = b;

        deffunc F( object) = a;

        consider f be Function such that

         A1: ( dom f) = NAT & for x be object st x in NAT holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from PARTFUN1:sch 1;

        

         A2: ( rng f) c= {a, b}

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider y be object such that

           A3: y in ( dom f) and

           A4: x = (f . y) by FUNCT_1:def 3;

          per cases ;

            suppose C[y];

            then (f . y) = a by A1;

            hence thesis by A4, TARSKI:def 2;

          end;

            suppose not C[y];

            then (f . y) = b by A1, A3;

            hence thesis by A4, TARSKI:def 2;

          end;

        end;

        for y be object st y in {a, b} holds ex x be object st x in ( dom f) & y = (f . x)

        proof

          let y be object;

          assume

           A5: y in {a, b};

          per cases by A5, TARSKI:def 2;

            suppose

             A6: y = a;

            take 2;

             C[2]

            proof

              take 1;

              thus thesis;

            end;

            hence thesis by A1, A6;

          end;

            suppose

             A7: y = b;

            take 1;

            for k be Element of NAT holds 1 <> (2 * k) by NAT_1: 15;

            hence thesis by A1, A7;

          end;

        end;

        then {a, b} c= ( rng f) by FUNCT_1: 9;

        then ( rng f) = {a, b} by A2;

        then

        reconsider f as sequence of S by A1, FUNCT_2:def 1, RELSET_1: 4;

        take f;

        let i be Element of NAT ;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of S;

        

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

        

         A9: ( dom f2) = NAT by FUNCT_2:def 1;

        assume that

         A10: for i be Element of NAT holds ((ex k be Element of NAT st i = (2 * k)) implies (f1 . i) = a) & (( not ex k be Element of NAT st i = (2 * k)) implies (f1 . i) = b) and

         A11: for i be Element of NAT holds ((ex k be Element of NAT st i = (2 * k)) implies (f2 . i) = a) & (( not ex k be Element of NAT st i = (2 * k)) implies (f2 . i) = b);

        for k be object st k in NAT holds (f1 . k) = (f2 . k)

        proof

          let k be object;

          assume k in NAT ;

          then

          reconsider k9 = k as Element of NAT ;

          per cases ;

            suppose

             A12: ex l be Element of NAT st k = (2 * l);

            

            then (f1 . k) = a by A10

            .= (f2 . k) by A11, A12;

            hence thesis;

          end;

            suppose

             A13: not ex l be Element of NAT st k = (2 * l);

            

            then (f1 . k9) = b by A10

            .= (f2 . k9) by A11, A13;

            hence thesis;

          end;

        end;

        hence thesis by A8, A9, FUNCT_1: 2;

      end;

    end

    scheme :: WAYBEL17:sch1

    FuncFraenkelS { B,C() -> non empty TopRelStr , A( set) -> Element of C() , f() -> Function , P[ set] } :

(f() .: { A(x) where x be Element of B() : P[x] }) = { (f() . A(x)) where x be Element of B() : P[x] }

      provided

       A1: the carrier of C() c= ( dom f());

      set f = f();

      thus (f .: { A(x) where x be Element of B() : P[x] }) c= { (f . A(x)) where x be Element of B() : P[x] }

      proof

        let y be object;

        assume y in (f .: { A(x) where x be Element of B() : P[x] });

        then

        consider z be object such that z in ( dom f) and

         A2: z in { A(x) where x be Element of B() : P[x] } and

         A3: y = (f . z) by FUNCT_1:def 6;

        ex x be Element of B() st z = A(x) & P[x] by A2;

        hence thesis by A3;

      end;

      let y be object;

      assume y in { (f . A(x)) where x be Element of B() : P[x] };

      then

      consider x be Element of B() such that

       A4: y = (f . A(x)) and

       A5: P[x];

      

       A6: A(x) in the carrier of C();

      A(x) in { A(z) where z be Element of B() : P[z] } by A5;

      hence thesis by A1, A4, A6, FUNCT_1:def 6;

    end;

    scheme :: WAYBEL17:sch2

    FuncFraenkelSL { B,C() -> LATTICE , A( set) -> Element of C() , f() -> Function , P[ set] } :

(f() .: { A(x) where x be Element of B() : P[x] }) = { (f() . A(x)) where x be Element of B() : P[x] }

      provided

       A1: the carrier of C() c= ( dom f());

      set f = f();

      thus (f .: { A(x) where x be Element of B() : P[x] }) c= { (f . A(x)) where x be Element of B() : P[x] }

      proof

        let y be object;

        assume y in (f .: { A(x) where x be Element of B() : P[x] });

        then

        consider z be object such that z in ( dom f) and

         A2: z in { A(x) where x be Element of B() : P[x] } and

         A3: y = (f . z) by FUNCT_1:def 6;

        ex x be Element of B() st z = A(x) & P[x] by A2;

        hence thesis by A3;

      end;

      let y be object;

      assume y in { (f . A(x)) where x be Element of B() : P[x] };

      then

      consider x be Element of B() such that

       A4: y = (f . A(x)) and

       A5: P[x];

      

       A6: A(x) in the carrier of C();

      A(x) in { A(z) where z be Element of B() : P[z] } by A5;

      hence thesis by A1, A4, A6, FUNCT_1:def 6;

    end;

    theorem :: WAYBEL17:1

    

     Th1: for S,T be non empty reflexive RelStr, f be Function of S, T, P be lower Subset of T st f is monotone holds (f " P) is lower

    proof

      let S,T be non empty reflexive RelStr;

      let f be Function of S, T;

      let P be lower Subset of T;

      assume

       A1: f is monotone;

      for x,y be Element of S st x in (f " P) & y <= x holds y in (f " P)

      proof

        let x,y be Element of S;

        assume that

         A2: x in (f " P) and

         A3: y <= x;

        

         A4: (f . y) <= (f . x) by A1, A3;

        reconsider fy = (f . y), fx = (f . x) as Element of T;

        fx in P by A2, FUNCT_2: 38;

        then fy in P by A4, WAYBEL_0:def 19;

        hence thesis by FUNCT_2: 38;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL17:2

    for S,T be non empty reflexive RelStr, f be Function of S, T, P be upper Subset of T st f is monotone holds (f " P) is upper

    proof

      let S,T be non empty reflexive RelStr;

      let f be Function of S, T;

      let P be upper Subset of T;

      assume

       A1: f is monotone;

      for x,y be Element of S st x in (f " P) & y >= x holds y in (f " P)

      proof

        let x,y be Element of S;

        assume that

         A2: x in (f " P) and

         A3: y >= x;

        

         A4: (f . y) >= (f . x) by A1, A3;

        reconsider fy = (f . y), fx = (f . x) as Element of T;

        fx in P by A2, FUNCT_2: 38;

        then fy in P by A4, WAYBEL_0:def 20;

        hence thesis by FUNCT_2: 38;

      end;

      hence thesis;

    end;

    

     Lm1: for T be up-complete LATTICE, x be Element of T holds ( downarrow x) is directly_closed

    proof

      let T be up-complete LATTICE, x be Element of T;

      let D be non empty directed Subset of T;

      assume

       A1: D c= ( downarrow x);

      

       A2: ex_sup_of (D,T) by WAYBEL_0: 75;

      x is_>=_than D by A1, WAYBEL_0: 17;

      then ( sup D) <= x by A2, YELLOW_0: 30;

      hence thesis by WAYBEL_0: 17;

    end;

    

     Lm2: for T be up-complete Scott TopLattice, x be Element of T holds ( Cl {x}) = ( downarrow x)

    proof

      let T be up-complete Scott TopLattice, x be Element of T;

      ( downarrow x) is directly_closed by Lm1;

      then

       A1: ( downarrow x) is closed by WAYBEL11: 7;

      x <= x;

      then x in ( downarrow x) by WAYBEL_0: 17;

      then

       A2: {x} c= ( downarrow x) by ZFMISC_1: 31;

      now

        let C be Subset of T such that

         A3: {x} c= C;

        reconsider D = C as Subset of T;

        assume C is closed;

        then

         A4: D is lower by WAYBEL11: 7;

        x in C by A3, ZFMISC_1: 31;

        hence ( downarrow x) c= C by A4, WAYBEL11: 6;

      end;

      hence thesis by A1, A2, YELLOW_8: 8;

    end;

    

     Lm3: for T be up-complete Scott TopLattice, x be Element of T holds ( downarrow x) is closed

    proof

      let T be up-complete Scott TopLattice, x be Element of T;

      ( Cl {x}) = ( downarrow x) by Lm2;

      hence thesis;

    end;

    theorem :: WAYBEL17:3

    

     Th3: for S,T be reflexive antisymmetric non empty RelStr, f be Function of S, T st f is directed-sups-preserving holds f is monotone

    proof

      let S,T be reflexive antisymmetric non empty RelStr, f be Function of S, T;

      assume

       A1: f is directed-sups-preserving;

      let x,y be Element of S such that

       A2: x <= y;

      y <= y;

      then

       A3: {x, y} is_<=_than y by A2, YELLOW_0: 8;

      

       A4: for b be Element of S st {x, y} is_<=_than b holds y <= b by YELLOW_0: 8;

      then

       A5: y = ( sup {x, y}) by A3, YELLOW_0: 30;

      

       A6: ex_sup_of ( {x, y},S) by A3, A4, YELLOW_0: 30;

      for a,b be Element of S st a in {x, y} & b in {x, y} holds ex z be Element of S st z in {x, y} & a <= z & b <= z

      proof

        let a,b be Element of S such that

         A7: a in {x, y} and

         A8: b in {x, y};

        take y;

        thus y in {x, y} by TARSKI:def 2;

        thus thesis by A2, A7, A8, TARSKI:def 2;

      end;

      then {x, y} is directed non empty;

      then

       A9: f preserves_sup_of {x, y} by A1;

      then

       A10: ( sup (f .: {x, y})) = (f . y) by A5, A6;

      

       A11: ( dom f) = the carrier of S by FUNCT_2:def 1;

      then

       A12: (f . y) = ( sup {(f . x), (f . y)}) by A10, FUNCT_1: 60;

      (f .: {x, y}) = {(f . x), (f . y)} by A11, FUNCT_1: 60;

      then ex_sup_of ( {(f . x), (f . y)},T) by A6, A9;

      then {(f . x), (f . y)} is_<=_than (f . y) by A12, YELLOW_0:def 9;

      hence (f . x) <= (f . y) by YELLOW_0: 8;

    end;

    registration

      let S,T be reflexive antisymmetric non empty RelStr;

      cluster directed-sups-preserving -> monotone for Function of S, T;

      coherence by Th3;

    end

    theorem :: WAYBEL17:4

    

     Th4: for S,T be up-complete Scott TopLattice, f be Function of S, T holds f is continuous implies f is monotone

    proof

      let S,T be up-complete Scott TopLattice;

      let f be Function of S, T;

      assume

       A1: f is continuous;

      let x,y be Element of S;

      

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

      assume

       A3: x <= y;

      (f . x) <= (f . y)

      proof

        set V = (( downarrow (f . y)) ` ), U1 = (f " V);

        assume not (f . x) <= (f . y);

        then not (f . x) in ( downarrow (f . y)) by WAYBEL_0: 17;

        then

         A4: (f . x) in V by XBOOLE_0:def 5;

        (f . y) <= (f . y);

        then

         A5: (f . y) in ( downarrow (f . y)) by WAYBEL_0: 17;

        ( downarrow (f . y)) is closed by Lm3;

        then U1 is open by A1, TOPS_2: 43;

        then

        reconsider U1 as upper Subset of S by WAYBEL11:def 4;

        x in U1 by A2, A4, FUNCT_1:def 7;

        then y in U1 by A3, WAYBEL_0:def 20;

        then (f . y) in V by FUNCT_1:def 7;

        hence contradiction by A5, XBOOLE_0:def 5;

      end;

      hence thesis;

    end;

    registration

      let S,T be up-complete Scott TopLattice;

      cluster continuous -> monotone for Function of S, T;

      correctness by Th4;

    end

    

     Lm4: for S,T be up-complete Scott non empty reflexive transitive antisymmetric TopSpace-like TopRelStr, f be Function of S, T holds f is directed-sups-preserving implies f is continuous

    proof

      let S,T be up-complete Scott non empty reflexive transitive antisymmetric TopSpace-like TopRelStr;

      let f be Function of S, T;

      assume

       A1: f is directed-sups-preserving;

      thus f is continuous

      proof

        let P1 be Subset of T;

        reconsider P19 = P1 as Subset of T;

        assume P1 is closed;

        then

         A2: P19 is directly_closed lower by WAYBEL11: 7;

        now

          let D be non empty directed Subset of S;

          assume

           A3: D c= (f " P1);

          

           A4: f preserves_sup_of D by A1;

           ex_sup_of (D,S) by WAYBEL_0: 75;

          then

           A5: ( sup (f .: D)) = (f . ( sup D)) by A4;

          reconsider fD = (f .: D) as directed Subset of T by A1, YELLOW_2: 15;

          fD c= P1 by A3, EQREL_1: 46;

          then ( sup fD) in P19 by A2;

          hence ( sup D) in (f " P1) by A5, FUNCT_2: 38;

        end;

        then (f " P1) is directly_closed lower by A1, A2, Th1;

        hence thesis by WAYBEL11: 7;

      end;

    end;

    begin

    registration

      let S be set;

      let T be reflexive RelStr;

      cluster (S --> T) -> reflexive-yielding;

      coherence

      proof

        set f = (S --> T);

        let W be RelStr;

        assume W in ( rng f);

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let S be non empty set, T be complete LATTICE;

      cluster (T |^ S) -> complete;

      coherence

      proof

        

         A1: (T |^ S) = ( product (S --> T)) by YELLOW_1:def 5;

        for i be Element of S holds ((S --> T) . i) is complete LATTICE;

        hence thesis by A1, WAYBEL_3: 31;

      end;

    end

    definition

      let S,T be up-complete Scott TopLattice;

      :: WAYBEL17:def2

      func SCMaps (S,T) -> strict full SubRelStr of ( MonMaps (S,T)) means

      : Def2: for f be Function of S, T holds f in the carrier of it iff f is continuous;

      existence

      proof

        defpred P[ object] means ex f be Function of S, T st $1 = f & f is continuous;

        consider X be set such that

         A1: for a be object holds a in X iff a in the carrier of ( MonMaps (S,T)) & P[a] from XBOOLE_0:sch 1;

        X c= the carrier of ( MonMaps (S,T)) by A1;

        then

        reconsider X as Subset of ( MonMaps (S,T));

        take SX = ( subrelstr X);

        let f be Function of S, T;

        hereby

          assume f in the carrier of SX;

          then f in X by YELLOW_0:def 15;

          then ex f9 be Function of S, T st (f9 = f) & (f9 is continuous) by A1;

          hence f is continuous;

        end;

        assume

         A2: f is continuous;

        f in ( Funcs (the carrier of S,the carrier of T)) by FUNCT_2: 8;

        then f in the carrier of ( MonMaps (S,T)) by A2, YELLOW_1:def 6;

        then f in X by A1, A2;

        hence thesis by YELLOW_0:def 15;

      end;

      uniqueness

      proof

        let A1,A2 be strict full SubRelStr of ( MonMaps (S,T));

        assume that

         A3: for f be Function of S, T holds f in the carrier of A1 iff f is continuous and

         A4: for f be Function of S, T holds f in the carrier of A2 iff f is continuous;

        

         A5: the carrier of A1 c= the carrier of ( MonMaps (S,T)) by YELLOW_0:def 13;

        

         A6: the carrier of A2 c= the carrier of ( MonMaps (S,T)) by YELLOW_0:def 13;

        the carrier of A1 = the carrier of A2

        proof

          hereby

            let x be object;

            assume

             A7: x in the carrier of A1;

            then

            reconsider y = x as Element of A1;

            reconsider y as Function of S, T by A5, A7, WAYBEL10: 9;

            y is continuous by A3, A7;

            hence x in the carrier of A2 by A4;

          end;

          let x be object;

          assume

           A8: x in the carrier of A2;

          then

          reconsider y = x as Element of A2;

          reconsider y as Function of S, T by A6, A8, WAYBEL10: 9;

          y is continuous by A4, A8;

          hence thesis by A3;

        end;

        hence thesis by YELLOW_0: 57;

      end;

    end

    registration

      let S,T be up-complete Scott TopLattice;

      cluster ( SCMaps (S,T)) -> non empty;

      coherence

      proof

        set f = the continuous Function of S, T;

        f in the carrier of ( SCMaps (S,T)) by Def2;

        hence thesis;

      end;

    end

    begin

    definition

      let S be non empty RelStr;

      let a,b be Element of S;

      :: WAYBEL17:def3

      func Net-Str (a,b) -> strict non empty NetStr over S means

      : Def3: the carrier of it = NAT & the mapping of it = ((a,b) ,... ) & for i,j be Element of it , i9,j9 be Element of NAT st i = i9 & j = j9 holds i <= j iff i9 <= j9;

      existence

      proof

        defpred P[ set, set] means for i,j be Element of NAT st i = $1 & j = $2 holds i <= j;

        consider R be Relation of NAT , NAT such that

         A1: for x,y be Element of NAT holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

        reconsider R as Relation of NAT ;

        take N = NetStr (# NAT , R, ((a,b) ,... ) #);

        thus the carrier of N = NAT ;

        thus the mapping of N = ((a,b) ,... );

        let i,j be Element of N, i9,j9 be Element of NAT such that

         A2: i = i9 and

         A3: j = j9;

        reconsider x = i, y = j as Element of NAT ;

         [x, y] in the InternalRel of N iff P[x, y] by A1;

        hence thesis by A2, A3, ORDERS_2:def 5;

      end;

      uniqueness

      proof

        let it1,it2 be strict non empty NetStr over S such that

         A4: the carrier of it1 = NAT and

         A5: the mapping of it1 = ((a,b) ,... ) and

         A6: for i,j be Element of it1, i9,j9 be Element of NAT st i = i9 & j = j9 holds i <= j iff i9 <= j9 and

         A7: the carrier of it2 = NAT and

         A8: the mapping of it2 = ((a,b) ,... ) and

         A9: for i,j be Element of it2, i9,j9 be Element of NAT st i = i9 & j = j9 holds i <= j iff i9 <= j9;

        the InternalRel of it1 = the InternalRel of it2

        proof

          let x,y be object;

          hereby

            assume

             A10: [x, y] in the InternalRel of it1;

            then

            reconsider i = x, j = y as Element of it1 by ZFMISC_1: 87;

            reconsider i1 = i, i2 = j as Element of NAT by A4;

            reconsider i9 = x, j9 = y as Element of it2 by A4, A7, A10, ZFMISC_1: 87;

            i <= j by A10, ORDERS_2:def 5;

            then i1 <= i2 by A6;

            then i9 <= j9 by A9;

            hence [x, y] in the InternalRel of it2 by ORDERS_2:def 5;

          end;

          assume

           A11: [x, y] in the InternalRel of it2;

          then

          reconsider i = x, j = y as Element of it2 by ZFMISC_1: 87;

          reconsider i9 = x, j9 = y as Element of it1 by A4, A7, A11, ZFMISC_1: 87;

          reconsider i1 = i, i2 = j as Element of NAT by A7;

          i <= j by A11, ORDERS_2:def 5;

          then i1 <= i2 by A9;

          then i9 <= j9 by A6;

          hence thesis by ORDERS_2:def 5;

        end;

        hence thesis by A4, A5, A7, A8;

      end;

    end

    registration

      let S be non empty RelStr;

      let a,b be Element of S;

      cluster ( Net-Str (a,b)) -> reflexive transitive directed antisymmetric;

      coherence

      proof

        set L = ( Net-Str (a,b));

        thus L is reflexive

        proof

          let x be Element of L;

          reconsider x9 = x as Element of NAT by Def3;

          x9 <= x9;

          hence thesis by Def3;

        end;

        thus L is transitive

        proof

          let x,y,z be Element of L;

          assume that

           A1: x <= y and

           A2: y <= z;

          reconsider x9 = x, y9 = y, z9 = z as Element of NAT by Def3;

          

           A3: x9 <= y9 by A1, Def3;

          y9 <= z9 by A2, Def3;

          then x9 <= z9 by A3, XXREAL_0: 2;

          hence thesis by Def3;

        end;

        ( [#] L) is directed

        proof

          let x,y be Element of L;

          assume that x in ( [#] L) and y in ( [#] L);

          reconsider x9 = x, y9 = y as Element of NAT by Def3;

          set z9 = (x9 + y9);

          reconsider z = z9 as Element of L by Def3;

          reconsider z as Element of L;

          take z;

          

           A4: x9 <= z9 by NAT_1: 11;

          y9 <= z9 by NAT_1: 11;

          hence thesis by A4, Def3;

        end;

        hence L is directed;

        thus L is antisymmetric

        proof

          let x,y be Element of L;

          reconsider x9 = x, y9 = y as Element of NAT by Def3;

          assume that

           A5: x <= y and

           A6: y <= x;

          

           A7: x9 <= y9 by A5, Def3;

          y9 <= x9 by A6, Def3;

          hence thesis by A7, XXREAL_0: 1;

        end;

      end;

    end

    theorem :: WAYBEL17:5

    

     Th5: for S be non empty RelStr, a,b be Element of S, i be Element of ( Net-Str (a,b)) holds (( Net-Str (a,b)) . i) = a or (( Net-Str (a,b)) . i) = b

    proof

      let S be non empty RelStr;

      let a,b be Element of S, i be Element of ( Net-Str (a,b));

      set N = ( Net-Str (a,b));

      reconsider I = i as Element of NAT by Def3;

      

       A1: (N . i) = (((a,b) ,... ) . i) by Def3;

      defpred C[ Element of NAT ] means ex k be Element of NAT st $1 = (2 * k);

      per cases ;

        suppose C[I];

        hence thesis by A1, Def1;

      end;

        suppose not C[I];

        hence thesis by A1, Def1;

      end;

    end;

    theorem :: WAYBEL17:6

    

     Th6: for S be non empty RelStr, a,b be Element of S, i,j be Element of ( Net-Str (a,b)), i9,j9 be Element of NAT st i9 = i & j9 = (i9 + 1) & j9 = j holds ((( Net-Str (a,b)) . i) = a implies (( Net-Str (a,b)) . j) = b) & ((( Net-Str (a,b)) . i) = b implies (( Net-Str (a,b)) . j) = a)

    proof

      let S be non empty RelStr;

      let a,b be Element of S, i,j be Element of ( Net-Str (a,b)), i9,j9 be Element of NAT ;

      assume that

       A1: i9 = i and

       A2: j9 = (i9 + 1) and

       A3: j9 = j;

      per cases ;

        suppose

         A4: a <> b;

        defpred C[ Element of NAT ] means ex k be Element of NAT st $1 = (2 * k);

        thus (( Net-Str (a,b)) . i) = a implies (( Net-Str (a,b)) . j) = b

        proof

          assume

           A5: (( Net-Str (a,b)) . i) = a;

           C[i9]

          proof

            assume

             A6: not C[i9];

            (( Net-Str (a,b)) . i) = (((a,b) ,... ) . i) by Def3

            .= b by A1, A6, Def1;

            hence thesis by A4, A5;

          end;

          then

           A7: for k be Element of NAT holds j9 <> (2 * k) by A2;

          (( Net-Str (a,b)) . j) = (((a,b) ,... ) . j) by Def3

          .= b by A3, A7, Def1;

          hence thesis;

        end;

        assume

         A8: (( Net-Str (a,b)) . i) = b;

        

         A9: not C[i9]

        proof

          assume

           A10: C[i9];

          (( Net-Str (a,b)) . i) = (((a,b) ,... ) . i) by Def3

          .= a by A1, A10, Def1;

          hence thesis by A4, A8;

        end;

        

         A11: C[j9]

        proof

          assume not C[j9];

          then ex kl be Element of NAT st (j9 = ((2 * kl) + 1)) by SCHEME1: 1;

          hence thesis by A2, A9;

        end;

        (( Net-Str (a,b)) . j) = (((a,b) ,... ) . j) by Def3

        .= a by A3, A11, Def1;

        hence thesis;

      end;

        suppose a = b;

        hence thesis by Th5;

      end;

    end;

    theorem :: WAYBEL17:7

    

     Th7: for S be with_infima Poset, a,b be Element of S holds ( lim_inf ( Net-Str (a,b))) = (a "/\" b)

    proof

      let S be with_infima Poset;

      let a,b be Element of S;

      set N = ( Net-Str (a,b));

      

       A1: for j be Element of N holds { (N . i) where i be Element of N : i >= j } = {a, b}

      proof

        let j be Element of N;

        thus { (N . i) where i be Element of N : i >= j } c= {a, b}

        proof

          let x be object;

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

          then

          consider i1 be Element of N such that

           A2: x = (N . i1) and i1 >= j;

          (N . i1) = a or (N . i1) = b by Th5;

          hence thesis by A2, TARSKI:def 2;

        end;

        thus {a, b} c= { (N . i) where i be Element of N : i >= j }

        proof

          let x be object;

          assume

           A3: x in {a, b};

          reconsider J = j as Element of NAT by Def3;

          defpred C[ Element of NAT ] means ex k be Element of NAT st $1 = (2 * k);

          per cases by A3, TARSKI:def 2;

            suppose

             A4: x = a;

            now

              per cases ;

                suppose

                 A5: C[J];

                

                 A6: (N . j) = (((a,b) ,... ) . j) by Def3

                .= a by A5, Def1;

                j <= j;

                hence thesis by A4, A6;

              end;

                suppose

                 A7: not C[J];

                

                 A8: (N . j) = (((a,b) ,... ) . j) by Def3

                .= b by A7, Def1;

                reconsider k = (J + 1) as Element of N by Def3;

                

                 A9: (N . k) = a by A8, Th6;

                (J + 1) >= J by NAT_1: 11;

                then k >= j by Def3;

                hence thesis by A4, A9;

              end;

            end;

            hence thesis;

          end;

            suppose

             A10: x = b;

            now

              per cases ;

                suppose

                 A11: not C[J];

                

                 A12: (N . j) = (((a,b) ,... ) . j) by Def3

                .= b by A11, Def1;

                j <= j;

                hence thesis by A10, A12;

              end;

                suppose

                 A13: C[J];

                

                 A14: (N . j) = (((a,b) ,... ) . j) by Def3

                .= a by A13, Def1;

                reconsider k = (J + 1) as Element of N by Def3;

                

                 A15: (N . k) = b by A14, Th6;

                (J + 1) >= J by NAT_1: 11;

                then k >= j by Def3;

                hence thesis by A10, A15;

              end;

            end;

            hence thesis;

          end;

        end;

      end;

      defpred P[ Element of N, Element of N] means $1 >= $2;

      deffunc F( Element of N) = { (N . i1) where i1 be Element of N : P[i1, $1] };

      defpred R[ set] means not contradiction;

      deffunc G( Element of N) = {a, b};

      deffunc Q1( Element of N) = ( "/\" ( F($1),S));

      deffunc Q2( Element of N) = ( "/\" ( G($1),S));

      deffunc F( set) = (a "/\" b);

      

       A16: for jj be Element of N holds Q1(jj) = F(jj)

      proof

        let jj be Element of N;

         Q1(jj) = Q2(jj) by A1

        .= (a "/\" b) by YELLOW_0: 40;

        hence thesis;

      end;

      

       A17: { Q1(j3) where j3 be Element of N : R[j3] } = { F(j4) where j4 be Element of N : R[j4] } from FRAENKEL:sch 5( A16);

      

       A18: { (a "/\" b) where j4 be Element of N : R[j4] } c= {(a "/\" b)}

      proof

        let x be object;

        assume x in { (a "/\" b) where j4 be Element of N : R[j4] };

        then ex q be Element of N st (x = (a "/\" b)) & R[q];

        hence thesis by TARSKI:def 1;

      end;

       {(a "/\" b)} c= { (a "/\" b) where j4 be Element of N : R[j4] }

      proof

        let x be object;

        assume x in {(a "/\" b)};

        then x = (a "/\" b) by TARSKI:def 1;

        hence thesis;

      end;

      then { (a "/\" b) where j4 be Element of N : R[j4] } = {(a "/\" b)} by A18;

      hence thesis by A17, YELLOW_0: 39;

    end;

    

     Lm5: for S be with_infima Poset, a,b be Element of S st a <= b holds ( lim_inf ( Net-Str (a,b))) = a

    proof

      let S be with_infima Poset;

      let a,b be Element of S such that

       A1: a <= b;

      reconsider a9 = a, b9 = b as Element of S;

      ( lim_inf ( Net-Str (a,b))) = (a9 "/\" b9) by Th7

      .= a9 by A1, YELLOW_0: 25;

      hence thesis;

    end;

    theorem :: WAYBEL17:8

    

     Th8: for S,T be with_infima Poset, a,b be Element of S, f be Function of S, T holds ( lim_inf (f * ( Net-Str (a,b)))) = ((f . a) "/\" (f . b))

    proof

      let S,T be with_infima Poset;

      let a,b be Element of S;

      let f be Function of S, T;

      set N = ( Net-Str (a,b));

      set fN = (f * N);

      

       A1: the RelStr of fN = the RelStr of N by WAYBEL_9:def 8;

      

       A2: for j be Element of fN holds { (fN . i) where i be Element of fN : i >= j } = {(f . a), (f . b)}

      proof

        let j be Element of fN;

        reconsider jj = j as Element of N by A1;

        thus { (fN . i) where i be Element of fN : i >= j } c= {(f . a), (f . b)}

        proof

          let x be object;

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

          then

          consider i1 be Element of fN such that

           A3: x = (fN . i1) and i1 >= j;

          reconsider I1 = i1 as Element of N by A1;

          i1 in the carrier of N by A1;

          then

           A4: i1 in ( dom the mapping of N) by FUNCT_2:def 1;

          (fN . i1) = ((f * the mapping of N) . i1) by WAYBEL_9:def 8

          .= (f . (N . I1)) by A4, FUNCT_1: 13;

          then (fN . i1) = (f . a) or (fN . i1) = (f . b) by Th5;

          hence thesis by A3, TARSKI:def 2;

        end;

        thus {(f . a), (f . b)} c= { (fN . i) where i be Element of fN : i >= j }

        proof

          let x be object;

          assume

           A5: x in {(f . a), (f . b)};

          

           A6: j in the carrier of N by A1;

          reconsider J = j as Element of NAT by A1, Def3;

          

           A7: j in ( dom the mapping of N) by A6, FUNCT_2:def 1;

          defpred C[ Element of NAT ] means ex k be Element of NAT st $1 = (2 * k);

          per cases by A5, TARSKI:def 2;

            suppose

             A8: x = (f . a);

            reconsider jj = j as Element of N by A1;

            now

              per cases ;

                suppose

                 A9: C[J];

                

                 A10: (fN . j) = ((f * the mapping of N) . j) by WAYBEL_9:def 8

                .= (f . (the mapping of N . j)) by A7, FUNCT_1: 13

                .= (f . (((a,b) ,... ) . j)) by Def3

                .= (f . a) by A9, Def1;

                j <= j;

                hence thesis by A8, A10;

              end;

                suppose

                 A11: not C[J];

                

                 A12: (N . jj) = (((a,b) ,... ) . jj) by Def3

                .= b by A11, Def1;

                reconsider k = (J + 1) as Element of fN by A1, Def3;

                reconsider kk = k as Element of N by A1;

                kk in the carrier of N;

                then

                 A13: kk in ( dom the mapping of N) by FUNCT_2:def 1;

                

                 A14: (fN . k) = ((f * the mapping of N) . k) by WAYBEL_9:def 8

                .= (f . (N . kk)) by A13, FUNCT_1: 13

                .= (f . a) by A12, Th6;

                (J + 1) >= J by NAT_1: 11;

                then kk >= jj by Def3;

                then [jj, kk] in the InternalRel of N by ORDERS_2:def 5;

                then k >= j by A1, ORDERS_2:def 5;

                hence thesis by A8, A14;

              end;

            end;

            hence thesis;

          end;

            suppose

             A15: x = (f . b);

            now

              per cases ;

                suppose

                 A16: not C[J];

                

                 A17: (fN . j) = ((f * the mapping of N) . j) by WAYBEL_9:def 8

                .= (f . (the mapping of N . j)) by A7, FUNCT_1: 13

                .= (f . (((a,b) ,... ) . j)) by Def3

                .= (f . b) by A16, Def1;

                j <= j;

                hence thesis by A15, A17;

              end;

                suppose

                 A18: C[J];

                

                 A19: (N . jj) = (((a,b) ,... ) . j) by Def3

                .= a by A18, Def1;

                reconsider k = (J + 1) as Element of fN by A1, Def3;

                reconsider kk = k as Element of N by Def3;

                kk in the carrier of N;

                then

                 A20: kk in ( dom the mapping of N) by FUNCT_2:def 1;

                

                 A21: (fN . k) = ((f * the mapping of N) . k) by WAYBEL_9:def 8

                .= (f . (N . kk)) by A20, FUNCT_1: 13

                .= (f . b) by A19, Th6;

                (J + 1) >= J by NAT_1: 11;

                then kk >= jj by Def3;

                then [jj, kk] in the InternalRel of N by ORDERS_2:def 5;

                then k >= j by A1, ORDERS_2:def 5;

                hence thesis by A15, A21;

              end;

            end;

            hence thesis;

          end;

        end;

      end;

      defpred P[ Element of fN, Element of fN] means $1 >= $2;

      deffunc F( Element of fN) = { (fN . i1) where i1 be Element of fN : P[i1, $1] };

      defpred R[ set] means not contradiction;

      deffunc G( Element of fN) = {(f . a), (f . b)};

      deffunc Q1( Element of fN) = ( "/\" ( F($1),T));

      deffunc Q2( Element of fN) = ( "/\" ( G($1),T));

      deffunc F( set) = ((f . a) "/\" (f . b));

      

       A22: for jj be Element of fN holds Q1(jj) = F(jj)

      proof

        let jj be Element of fN;

         Q1(jj) = Q2(jj) by A2

        .= ((f . a) "/\" (f . b)) by YELLOW_0: 40;

        hence thesis;

      end;

      

       A23: { Q1(j3) where j3 be Element of fN : R[j3] } = { F(j4) where j4 be Element of fN : R[j4] } from FRAENKEL:sch 5( A22);

      

       A24: { ((f . a) "/\" (f . b)) where j4 be Element of fN : R[j4] } c= {((f . a) "/\" (f . b))}

      proof

        let x be object;

        assume x in { ((f . a) "/\" (f . b)) where j4 be Element of fN : R[j4] };

        then ex q be Element of fN st (x = ((f . a) "/\" (f . b))) & R[q];

        hence thesis by TARSKI:def 1;

      end;

       {((f . a) "/\" (f . b))} c= { ((f . a) "/\" (f . b)) where j4 be Element of fN : R[j4] }

      proof

        let x be object;

        assume x in {((f . a) "/\" (f . b))};

        then x = ((f . a) "/\" (f . b)) by TARSKI:def 1;

        hence thesis;

      end;

      then { ((f . a) "/\" (f . b)) where j4 be Element of fN : R[j4] } = {((f . a) "/\" (f . b))} by A24;

      hence thesis by A23, YELLOW_0: 39;

    end;

    definition

      let S be non empty RelStr;

      let D be non empty Subset of S;

      :: WAYBEL17:def4

      func Net-Str D -> strict NetStr over S equals NetStr (# D, (the InternalRel of S |_2 D), (( id the carrier of S) | D) #);

      correctness ;

    end

    theorem :: WAYBEL17:9

    

     Th9: for S be non empty reflexive RelStr, D be non empty Subset of S holds ( Net-Str D) = ( Net-Str (D,(( id the carrier of S) | D)))

    proof

      let S be non empty reflexive RelStr;

      let D be non empty Subset of S;

      set M = ( Net-Str (D,(( id the carrier of S) | D)));

      

       A1: D = the carrier of M by WAYBEL11:def 10;

      

       A2: (( id the carrier of S) | D) = the mapping of M by WAYBEL11:def 10;

      

       A3: (( id the carrier of S) | D) = ( id D) by FUNCT_3: 1;

      

       A4: (the InternalRel of S |_2 D) c= the InternalRel of S by XBOOLE_1: 17;

      now

        let x,y be object;

        hereby

          assume

           A5: [x, y] in (the InternalRel of S |_2 D);

          then

           A6: x in D by ZFMISC_1: 87;

          

           A7: y in D by A5, ZFMISC_1: 87;

          reconsider x9 = x, y9 = y as Element of M by A1, A5, ZFMISC_1: 87;

          

           A8: x9 = ((( id the carrier of S) | D) . x9) by A3, A6, FUNCT_1: 18;

          y9 = ((( id the carrier of S) | D) . y9) by A3, A7, FUNCT_1: 18;

          then (M . x9) <= (M . y9) by A2, A4, A5, A8, ORDERS_2:def 5;

          then x9 <= y9 by WAYBEL11:def 10;

          hence [x, y] in the InternalRel of M by ORDERS_2:def 5;

        end;

        assume

         A9: [x, y] in the InternalRel of M;

        then

        reconsider x9 = x, y9 = y as Element of M by ZFMISC_1: 87;

        x9 <= y9 by A9, ORDERS_2:def 5;

        then (M . x9) <= (M . y9) by WAYBEL11:def 10;

        then

         A10: [(M . x9), (M . y9)] in the InternalRel of S by ORDERS_2:def 5;

        

         A11: x9 = ((( id the carrier of S) | D) . x9) by A1, A3;

        y9 = ((( id the carrier of S) | D) . y9) by A1, A3;

        hence [x, y] in (the InternalRel of S |_2 D) by A1, A2, A9, A10, A11, XBOOLE_0:def 4;

      end;

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

    end;

    registration

      let S be non empty reflexive RelStr;

      let D be directed non empty Subset of S;

      cluster ( Net-Str D) -> non empty directed reflexive;

      coherence

      proof

        ( Net-Str D) = ( Net-Str (D,(( id the carrier of S) | D))) by Th9;

        hence thesis;

      end;

    end

    registration

      let S be non empty reflexive transitive RelStr;

      let D be directed non empty Subset of S;

      cluster ( Net-Str D) -> transitive;

      coherence ;

    end

    registration

      let S be non empty reflexive RelStr;

      let D be directed non empty Subset of S;

      cluster ( Net-Str D) -> monotone;

      coherence

      proof

        ( Net-Str D) = ( Net-Str (D,(( id the carrier of S) | D))) by Th9;

        hence thesis;

      end;

    end

    

     Lm6: for R be up-complete LATTICE, N be monotone reflexive net of R holds ( lim_inf N) = ( sup N)

    proof

      let R be up-complete LATTICE, N be monotone reflexive net of R;

      defpred P[ set] means not contradiction;

      deffunc F( Element of N) = (N . $1);

      deffunc G( Element of N) = ( "/\" ({ (N . i) where i be Element of N : i >= $1 },R));

      

       A1: for j be Element of N holds F(j) = G(j)

      proof

        let j be Element of N;

        set Y = { (N . i) where i be Element of N : i >= j };

        

         A2: (N . j) is_<=_than Y

        proof

          let y be Element of R;

          assume y in Y;

          then ex i be Element of N st y = (N . i) & j <= i;

          hence (N . j) <= y by WAYBEL11:def 9;

        end;

        for b be Element of R st b is_<=_than Y holds (N . j) >= b

        proof

          let b be Element of R;

          assume

           A3: b is_<=_than Y;

          reconsider j9 = j as Element of N;

          j9 <= j9;

          then (N . j9) in Y;

          hence thesis by A3;

        end;

        hence thesis by A2, YELLOW_0: 31;

      end;

      ( rng the mapping of N) = { F(j) where j be Element of N : P[j] } by WAYBEL11: 19

      .= { G(j) where j be Element of N : P[j] } from FRAENKEL:sch 5( A1);

      

      hence ( lim_inf N) = ( Sup the mapping of N) by YELLOW_2:def 5

      .= ( sup N) by WAYBEL_2:def 1;

    end;

    theorem :: WAYBEL17:10

    

     Th10: for S be up-complete LATTICE, D be directed non empty Subset of S holds ( lim_inf ( Net-Str D)) = ( sup D)

    proof

      let S be up-complete LATTICE;

      let D be directed non empty Subset of S;

      set F = (( id the carrier of S) | D);

      

       A1: F = ( id D) by FUNCT_3: 1;

      ( lim_inf ( Net-Str D)) = ( sup ( Net-Str D)) by Lm6

      .= ( Sup F) by WAYBEL_2:def 1

      .= ( "\/" (( rng F),S)) by YELLOW_2:def 5

      .= ( sup D) by A1, RELAT_1: 45;

      hence thesis;

    end;

    begin

    theorem :: WAYBEL17:11

    

     Th11: for S,T be LATTICE, f be Function of S, T holds (for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N))) implies f is monotone

    proof

      let S,T be LATTICE;

      let f be Function of S, T;

      assume

       A1: for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N));

      now

        let a,b be Element of S;

        assume

         A2: a <= b;

        set N = ( Net-Str (a,b));

        

         A3: (f . ( lim_inf N)) = (f . a) by A2, Lm5;

        ( lim_inf (f * N)) = ((f . a) "/\" (f . b)) by Th8;

        then

         A4: (f . a) <= ((f . a) "/\" (f . b)) by A1, A3;

        (f . a) >= ((f . a) "/\" (f . b)) by YELLOW_0: 23;

        then (f . a) = ((f . a) "/\" (f . b)) by A4, ORDERS_2: 2;

        hence (f . a) <= (f . b) by YELLOW_0: 25;

      end;

      hence thesis;

    end;

    scheme :: WAYBEL17:sch3

    NetFraenkelS { B,B1,C() -> non empty TopRelStr , A( set) -> Element of C() , f() -> Function , P[ set] } :

(f() .: { A(x) where x be Element of B() : P[x] }) = { (f() . A(x)) where x be Element of B1() : P[x] }

      provided

       A1: the carrier of C() c= ( dom f())

       and

       A2: the carrier of B() = the carrier of B1();

      set f = f();

      thus (f .: { A(x) where x be Element of B() : P[x] }) c= { (f . A(x)) where x be Element of B1() : P[x] }

      proof

        let y be object;

        assume y in (f .: { A(x) where x be Element of B() : P[x] });

        then

        consider z be object such that z in ( dom f) and

         A3: z in { A(x) where x be Element of B() : P[x] } and

         A4: y = (f . z) by FUNCT_1:def 6;

        consider x be Element of B() such that

         A5: z = A(x) and

         A6: P[x] by A3;

        reconsider x as Element of B1() by A2;

        y = (f . A(x)) by A4, A5;

        hence thesis by A6;

      end;

      let y be object;

      assume y in { (f . A(x)) where x be Element of B1() : P[x] };

      then

      consider x be Element of B1() such that

       A7: y = (f . A(x)) and

       A8: P[x];

      reconsider x as Element of B() by A2;

      

       A9: A(x) in the carrier of C();

      A(x) in { A(z) where z be Element of B() : P[z] } by A8;

      hence thesis by A1, A7, A9, FUNCT_1:def 6;

    end;

    theorem :: WAYBEL17:12

    

     Th12: for S,T be continuous lower-bounded LATTICE, f be Function of S, T holds (f is directed-sups-preserving implies for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)))

    proof

      let S,T be continuous lower-bounded LATTICE;

      let f be Function of S, T;

      assume

       A1: f is directed-sups-preserving;

      let x be Element of S;

      defpred P[ Element of S] means $1 << x;

      deffunc A( Element of S) = $1;

      

       A2: f preserves_sup_of ( waybelow x) by A1;

      

       A3: ex_sup_of (( waybelow x),S) by YELLOW_0: 17;

      

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

      

       A5: (f .: { A(w) where w be Element of S : P[w] }) = { (f . A(w)) where w be Element of S : P[w] } from FuncFraenkelSL( A4);

      (f . x) = (f . ( sup ( waybelow x))) by WAYBEL_3:def 5

      .= ( "\/" ({ (f . w) where w be Element of S : w << x },T)) by A2, A3, A5;

      hence thesis;

    end;

    theorem :: WAYBEL17:13

    

     Th13: for S be LATTICE, T be up-complete lower-bounded LATTICE, f be Function of S, T holds ((for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T))) implies f is monotone)

    proof

      let S be LATTICE, T be up-complete lower-bounded LATTICE;

      let f be Function of S, T;

      assume

       A1: for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T));

      let X,Y be Element of S;

      deffunc A( Element of S) = $1;

      defpred P[ Element of S] means $1 << X;

      defpred Q[ Element of S] means $1 << Y;

      assume X <= Y;

      then

       A2: ( waybelow X) c= ( waybelow Y) by WAYBEL_3: 12;

      

       A3: (f . X) = ( "\/" ({ (f . w) where w be Element of S : w << X },T)) by A1;

      

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

      

       A5: (f .: { A(w) where w be Element of S : P[w] }) = { (f . A(w)) where w be Element of S : P[w] } from FuncFraenkelSL( A4);

      (f .: { A(w) where w be Element of S : Q[w] }) = { (f . A(w)) where w be Element of S : Q[w] } from FuncFraenkelSL( A4);

      then

       A6: (f . Y) = ( "\/" ((f .: ( waybelow Y)),T)) by A1;

      

       A7: ex_sup_of ((f .: ( waybelow X)),T) by YELLOW_0: 17;

       ex_sup_of ((f .: ( waybelow Y)),T) by YELLOW_0: 17;

      hence thesis by A2, A3, A5, A6, A7, RELAT_1: 123, YELLOW_0: 34;

    end;

    theorem :: WAYBEL17:14

    

     Th14: for S be up-complete lower-bounded LATTICE, T be continuous lower-bounded LATTICE, f be Function of S, T holds ((for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T))) implies for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w))

    proof

      let S be up-complete lower-bounded LATTICE;

      let T be continuous lower-bounded LATTICE;

      let f be Function of S, T;

      assume

       A1: for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T));

      then

       A2: f is monotone by Th13;

      let x be Element of S, y be Element of T;

      hereby

        assume

         A3: y << (f . x);

        reconsider D = (f .: ( waybelow x)) as non empty directed Subset of T by A1, Th13, YELLOW_2: 15;

        

         A4: (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)) by A1;

        

         A5: the carrier of S c= ( dom f) by FUNCT_2:def 1;

        defpred P[ Element of S] means $1 << x;

        deffunc A( Element of S) = $1;

        (f .: { A(w) where w be Element of S : P[w] }) = { (f . A(w)) where w be Element of S : P[w] } from FuncFraenkelSL( A5);

        then

        consider w be Element of T such that

         A6: w in D and

         A7: y << w by A3, A4, WAYBEL_4: 53;

        consider v be object such that

         A8: v in the carrier of S and

         A9: v in ( waybelow x) and

         A10: w = (f . v) by A6, FUNCT_2: 64;

        reconsider v as Element of S by A8;

        take v;

        thus v << x & y << (f . v) by A7, A9, A10, WAYBEL_3: 7;

      end;

      given w be Element of S such that

       A11: w << x and

       A12: y << (f . w);

      w <= x by A11, WAYBEL_3: 1;

      then (f . w) <= (f . x) by A2;

      hence thesis by A12, WAYBEL_3: 2;

    end;

    theorem :: WAYBEL17:15

    

     Th15: for S,T be non empty RelStr, D be Subset of S, f be Function of S, T st ex_sup_of (D,S) & ex_sup_of ((f .: D),T) or S is complete antisymmetric & T is complete antisymmetric holds f is monotone implies ( sup (f .: D)) <= (f . ( sup D))

    proof

      let S,T be non empty RelStr;

      let D be Subset of S;

      let f be Function of S, T;

      assume that

       A1: ex_sup_of (D,S) & ex_sup_of ((f .: D),T) or S is complete antisymmetric & T is complete antisymmetric;

      

       A2: ex_sup_of (D,S) by A1, YELLOW_0: 17;

      

       A3: ex_sup_of ((f .: D),T) by A1, YELLOW_0: 17;

      assume

       A4: f is monotone;

      D is_<=_than ( sup D) by A2, YELLOW_0:def 9;

      then (f .: D) is_<=_than (f . ( sup D)) by A4, YELLOW_2: 14;

      hence thesis by A3, YELLOW_0:def 9;

    end;

    theorem :: WAYBEL17:16

    

     Th16: for S,T be non empty reflexive antisymmetric RelStr, D be directed non empty Subset of S, f be Function of S, T st ex_sup_of (D,S) & ex_sup_of ((f .: D),T) or S is up-complete & T is up-complete holds f is monotone implies ( sup (f .: D)) <= (f . ( sup D))

    proof

      let S,T be non empty reflexive antisymmetric RelStr;

      let D be directed non empty Subset of S;

      let f be Function of S, T;

      assume that

       A1: ex_sup_of (D,S) & ex_sup_of ((f .: D),T) or S is up-complete & T is up-complete;

      assume

       A2: f is monotone;

      then

      reconsider fD = (f .: D) as directed non empty Subset of T by YELLOW_2: 15;

      

       A3: ex_sup_of (fD,T) by A1, WAYBEL_0: 75;

       ex_sup_of (D,S) by A1, WAYBEL_0: 75;

      then D is_<=_than ( sup D) by YELLOW_0: 30;

      then (f .: D) is_<=_than (f . ( sup D)) by A2, YELLOW_2: 14;

      hence thesis by A3, YELLOW_0: 30;

    end;

    theorem :: WAYBEL17:17

    for S,T be non empty RelStr, D be Subset of S, f be Function of S, T st ex_inf_of (D,S) & ex_inf_of ((f .: D),T) or S is complete antisymmetric & T is complete antisymmetric holds f is monotone implies (f . ( inf D)) <= ( inf (f .: D))

    proof

      let S,T be non empty RelStr;

      let D be Subset of S;

      let f be Function of S, T;

      assume that

       A1: ex_inf_of (D,S) & ex_inf_of ((f .: D),T) or S is complete antisymmetric & T is complete antisymmetric;

      

       A2: ex_inf_of (D,S) by A1, YELLOW_0: 17;

      

       A3: ex_inf_of ((f .: D),T) by A1, YELLOW_0: 17;

      assume

       A4: f is monotone;

      ( inf D) is_<=_than D by A2, YELLOW_0:def 10;

      then (f . ( inf D)) is_<=_than (f .: D) by A4, YELLOW_2: 13;

      hence thesis by A3, YELLOW_0:def 10;

    end;

    

     Lm7: for S,T be complete LATTICE, D be Subset of S, f be Function of S, T holds f is monotone implies (f . ( "/\" (D,S))) <= ( inf (f .: D))

    proof

      let S,T be complete LATTICE;

      let D be Subset of S;

      let f be Function of S, T;

      reconsider D9 = D as Subset of S;

      set infD = ( "/\" (D,S));

      assume

       A1: f is monotone;

      infD is_<=_than D by YELLOW_0: 33;

      then (f . infD) is_<=_than (f .: D9) by A1, YELLOW_2: 13;

      hence thesis by YELLOW_0: 33;

    end;

    theorem :: WAYBEL17:18

    

     Th18: for S,T be up-complete LATTICE, f be Function of S, T, N be monotone non empty NetStr over S holds f is monotone implies (f * N) is monotone

    proof

      let S,T be up-complete LATTICE, f be Function of S, T;

      let N be monotone non empty NetStr over S;

      assume

       A1: f is monotone;

      

       A2: ( netmap (N,S)) is monotone by WAYBEL_0:def 9;

      

       A3: ( netmap ((f * N),T)) = (f * ( netmap (N,S))) by WAYBEL_9:def 8;

      set g = ( netmap ((f * N),T));

      now

        let x,y be Element of (f * N);

        assume

         A4: x <= y;

        

         A5: the RelStr of N = the RelStr of (f * N) by WAYBEL_9:def 8;

        then

        reconsider x9 = x, y9 = y as Element of N;

        

         A6: ( dom ( netmap (N,S))) = the carrier of (f * N) by A5, FUNCT_2:def 1;

        then

         A7: (( netmap ((f * N),T)) . x) = (f . (( netmap (N,S)) . x)) by A3, FUNCT_1: 13;

        

         A8: (( netmap ((f * N),T)) . y) = (f . (( netmap (N,S)) . y)) by A3, A6, FUNCT_1: 13;

         [x, y] in the InternalRel of (f * N) by A4, ORDERS_2:def 5;

        then x9 <= y9 by A5, ORDERS_2:def 5;

        then (( netmap (N,S)) . x9) <= (( netmap (N,S)) . y9) by A2;

        hence (g . x) <= (g . y) by A1, A7, A8;

      end;

      then ( netmap ((f * N),T)) is monotone;

      hence thesis;

    end;

    registration

      let S,T be up-complete LATTICE;

      let f be monotone Function of S, T;

      let N be monotone non empty NetStr over S;

      cluster (f * N) -> monotone;

      coherence by Th18;

    end

    theorem :: WAYBEL17:19

    for S,T be up-complete LATTICE, f be Function of S, T holds (for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N))) implies for D be directed non empty Subset of S holds ( sup (f .: D)) = (f . ( sup D))

    proof

      let S,T be up-complete LATTICE, f be Function of S, T;

      assume

       A1: for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N));

      let D be directed non empty Subset of S;

      

       A2: f is monotone by A1, Th11;

      then

       A3: ( sup (f .: D)) <= (f . ( sup D)) by Th16;

      (f . ( sup D)) <= ( sup (f .: D))

      proof

        ( sup D) = ( lim_inf ( Net-Str D)) by Th10;

        then

         A4: (f . ( sup D)) <= ( lim_inf (f * ( Net-Str D))) by A1;

        reconsider fN = (f * ( Net-Str D)) as monotone reflexive net of T by A2;

        

         A5: ( sup fN) = ( Sup the mapping of fN) by WAYBEL_2:def 1

        .= ( Sup (f * (( id the carrier of S) | D))) by WAYBEL_9:def 8

        .= ( sup ( rng (f * (( id the carrier of S) | D)))) by YELLOW_2:def 5;

        ( rng (f * (( id the carrier of S) | D))) = ( rng (f * ( id D))) by FUNCT_3: 1

        .= ( rng (f | D)) by RELAT_1: 65

        .= (f .: D) by RELAT_1: 115;

        hence thesis by A4, A5, Lm6;

      end;

      hence thesis by A3, ORDERS_2: 2;

    end;

    

     Lm8: for S,T be complete LATTICE, f be Function of S, T holds (for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N))) implies f is directed-sups-preserving

    proof

      let S,T be complete LATTICE, f be Function of S, T;

      assume

       A1: for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N));

      thus f is directed-sups-preserving

      proof

        let D be Subset of S;

        assume D is non empty directed;

        then

        reconsider D as non empty directed Subset of S;

        

         A2: f is monotone by A1, Th11;

        then

         A3: ( sup (f .: D)) <= (f . ( sup D)) by Th15;

        

         A4: (f . ( sup D)) <= ( sup (f .: D))

        proof

          ( sup D) = ( lim_inf ( Net-Str D)) by Th10;

          then

           A5: (f . ( sup D)) <= ( lim_inf (f * ( Net-Str D))) by A1;

          reconsider fN = (f * ( Net-Str D)) as monotone reflexive net of T by A2;

          

           A6: ( sup fN) = ( Sup the mapping of fN) by WAYBEL_2:def 1

          .= ( Sup (f * (( id the carrier of S) | D))) by WAYBEL_9:def 8

          .= ( sup ( rng (f * (( id the carrier of S) | D)))) by YELLOW_2:def 5;

          ( rng (f * (( id the carrier of S) | D))) = ( rng (f * ( id D))) by FUNCT_3: 1

          .= ( rng (f | D)) by RELAT_1: 65

          .= (f .: D) by RELAT_1: 115;

          hence thesis by A5, A6, WAYBEL11: 22;

        end;

        f preserves_sup_of D by A3, A4, ORDERS_2: 2, YELLOW_0: 17;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL17:20

    

     Th20: for S,T be complete LATTICE, f be Function of S, T, N be net of S, j be Element of N, j9 be Element of (f * N) st j9 = j holds f is monotone implies (f . ( "/\" ({ (N . k) where k be Element of N : k >= j },S))) <= ( "/\" ({ ((f * N) . l) where l be Element of (f * N) : l >= j9 },T))

    proof

      let S,T be complete LATTICE, f be Function of S, T;

      let N be net of S;

      let j be Element of N, j9 be Element of (f * N);

      assume

       A1: j9 = j;

      assume

       A2: f is monotone;

      

       A3: ( dom f) = the carrier of S by FUNCT_2:def 1;

      

       A4: the RelStr of (f * N) = the RelStr of N by WAYBEL_9:def 8;

      

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

      

       A6: { ((f * N) . l) where l be Element of (f * N) : l >= j9 } c= (f .: { (N . l1) where l1 be Element of N : l1 >= j })

      proof

        let s be object;

        assume s in { ((f * N) . l) where l be Element of (f * N) : l >= j9 };

        then

        consider x be Element of (f * N) such that

         A7: s = ((f * N) . x) and

         A8: x >= j9;

        reconsider x as Element of N by A4;

         [j9, x] in the InternalRel of (f * N) by A8, ORDERS_2:def 5;

        then

         A9: x >= j by A1, A4, ORDERS_2:def 5;

        

         A10: s = ((f * the mapping of N) . x) by A7, WAYBEL_9:def 8

        .= (f . (N . x)) by A5, FUNCT_1: 13;

        (N . x) in { (N . z) where z be Element of N : z >= j } by A9;

        hence thesis by A3, A10, FUNCT_1:def 6;

      end;

      

       A11: (f .: { (N . l1) where l1 be Element of N : l1 >= j }) c= { ((f * N) . l) where l be Element of (f * N) : l >= j9 }

      proof

        let s be object;

        assume s in (f .: { (N . l1) where l1 be Element of N : l1 >= j });

        then

        consider x be object such that x in ( dom f) and

         A12: x in { (N . l1) where l1 be Element of N : l1 >= j } and

         A13: s = (f . x) by FUNCT_1:def 6;

        consider l2 be Element of N such that

         A14: x = (N . l2) and

         A15: l2 >= j by A12;

        reconsider l29 = l2 as Element of (f * N) by A4;

        

         A16: s = ((f * the mapping of N) . l2) by A5, A13, A14, FUNCT_1: 13

        .= ((f * N) . l29) by WAYBEL_9:def 8;

         [j, l2] in the InternalRel of N by A15, ORDERS_2:def 5;

        then l29 >= j9 by A1, A4, ORDERS_2:def 5;

        hence thesis by A16;

      end;

      set K = { (N . k) where k be Element of N : k >= j };

      K c= the carrier of S

      proof

        let r be object;

        assume r in K;

        then ex f be Element of N st (r = (N . f)) & (f >= j);

        hence thesis;

      end;

      then

      reconsider K as Subset of S;

      { ((f * N) . l) where l be Element of (f * N) : l >= j9 } = (f .: K) by A6, A11;

      hence thesis by A2, Lm7;

    end;

    

     Lm9: for S,T be complete Scott TopLattice, f be continuous Function of S, T holds for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N))

    proof

      let S,T be complete Scott TopLattice, f be continuous Function of S, T;

      let N be net of S;

      set x = ( lim_inf N);

      set t = ( lim_inf (f * N));

      assume not (f . x) <= t;

      then not (f . x) in ( downarrow t) by WAYBEL_0: 17;

      then

       A1: (f . x) in (( downarrow t) ` ) by XBOOLE_0:def 5;

      

       A2: ( downarrow t) is closed by Lm3;

      set U1 = (f " (( downarrow t) ` ));

      

       A3: U1 is open by A2, TOPS_2: 43;

      set D = the set of all ( "/\" ({ (N . k) where k be Element of N : k >= j },S)) where j be Element of N;

      now

        let f be object;

        assume f in D;

        then ex j be Element of N st (f = ( "/\" ({ (N . k) where k be Element of N : k >= j },S)));

        hence f in the carrier of S;

      end;

      then

      reconsider D as Subset of S by TARSKI:def 3;

      reconsider D as non empty directed Subset of S by WAYBEL11: 30;

      

       A4: x in U1 by A1, FUNCT_2: 38;

      U1 is property(S) by A3, WAYBEL11: 15;

      then

      consider y be Element of S such that

       A5: y in D and

       A6: for x be Element of S st x in D & x >= y holds x in U1 by A4;

      consider j be Element of N such that

       A7: y = ( "/\" ({ (N . k) where k be Element of N : k >= j },S)) by A5;

      y <= y;

      then

       A8: y in U1 by A5, A6;

       the RelStr of (f * N) = the RelStr of N by WAYBEL_9:def 8;

      then

      reconsider j9 = j as Element of (f * N);

      

       A9: ( dom f) = the carrier of S by FUNCT_2:def 1;

      set fy = ( "/\" ({ ((f * N) . k) where k be Element of (f * N) : k >= j9 },T));

      set fD = the set of all ( "/\" ({ ((f * N) . k) where k be Element of (f * N) : k >= j1 },T)) where j1 be Element of (f * N);

      now

        let g be object;

        assume g in fD;

        then ex j be Element of (f * N) st (g = ( "/\" ({ ((f * N) . k) where k be Element of (f * N) : k >= j },T)));

        hence g in the carrier of T;

      end;

      then

      reconsider fD as Subset of T by TARSKI:def 3;

      

       A10: (f . y) <= fy by A7, Th20;

      fy in fD;

      then fy <= ( sup fD) by YELLOW_2: 22;

      then (f . y) <= t by A10, ORDERS_2: 3;

      then (f . y) in ( downarrow t) by WAYBEL_0: 17;

      then

       A11: y in (f " ( downarrow t)) by A9, FUNCT_1:def 7;

      (f " (( downarrow t) ` )) = ((f " ( [#] T)) \ (f " ( downarrow t))) by FUNCT_1: 69

      .= (( [#] S) \ (f " ( downarrow t))) by TOPS_2: 41

      .= ((f " ( downarrow t)) ` );

      then

       A12: y in (U1 /\ (U1 ` )) by A8, A11, XBOOLE_0:def 4;

      U1 misses (U1 ` ) by XBOOLE_1: 79;

      hence contradiction by A12;

    end;

    

     Lm10: for L be continuous Scott TopLattice, p be Element of L, S be Subset of L st S is open & p in S holds ex q be Element of L st q << p & q in S

    proof

      let L be continuous Scott TopLattice, p be Element of L;

      let S be Subset of L such that

       A1: S is open and

       A2: p in S;

      

       A3: S is inaccessible by A1, WAYBEL11:def 4;

      ( sup ( waybelow p)) = p by WAYBEL_3:def 5;

      then ( waybelow p) meets S by A2, A3;

      then (( waybelow p) /\ S) <> {} ;

      then

      consider u be object such that

       A4: u in (( waybelow p) /\ S) by XBOOLE_0:def 1;

      

       A5: u in ( waybelow p) by A4, XBOOLE_0:def 4;

      reconsider u as Element of L by A4;

      take u;

      thus u << p by A5, WAYBEL_3: 7;

      thus thesis by A4, XBOOLE_0:def 4;

    end;

    

     Lm11: for L be continuous lower-bounded Scott TopLattice, x be Element of L holds ( wayabove x) is open

    proof

      let L be continuous lower-bounded Scott TopLattice, x be Element of L;

      set W = ( wayabove x);

      W is inaccessible

      proof

        let D be non empty directed Subset of L;

        assume ( sup D) in W;

        then x << ( sup D) by WAYBEL_3: 8;

        then

        consider d be Element of L such that

         A1: d in D and

         A2: x << d by WAYBEL_4: 53;

        d in W by A2;

        hence thesis by A1, XBOOLE_0: 3;

      end;

      hence thesis by WAYBEL11:def 4;

    end;

    

     Lm12: for L be lower-bounded continuous Scott TopLattice, p be Element of L holds { ( wayabove q) where q be Element of L : q << p } is Basis of p

    proof

      let L be lower-bounded continuous Scott TopLattice, p be Element of L;

      set X = { ( wayabove q) where q be Element of L : q << p };

      X c= ( bool the carrier of L)

      proof

        let e be object;

        assume e in X;

        then ex q be Element of L st e = ( wayabove q) & q << p;

        hence thesis;

      end;

      then

      reconsider X as Subset-Family of L;

      X is Basis of p

      proof

        

         A1: X is open

        proof

          let e be Subset of L;

          assume e in X;

          then

          consider q be Element of L such that

           A2: e = ( wayabove q) and q << p;

          ( wayabove q) is open by Lm11;

          hence thesis by A2;

        end;

        X is p -quasi_basis

        proof

          for Y be set st Y in X holds p in Y

          proof

            let e be set;

            assume e in X;

            then ex q be Element of L st e = ( wayabove q) & q << p;

            hence thesis;

          end;

          hence p in ( Intersect X) by SETFAM_1: 43;

          let S be Subset of L such that

           A3: S is open and

           A4: p in S;

          consider u be Element of L such that

           A5: u << p and

           A6: u in S by A3, A4, Lm10;

          take V = ( wayabove u);

          thus V in X by A5;

          

           A7: S is upper by A3, WAYBEL11:def 4;

          

           A8: ( wayabove u) c= ( uparrow u) by WAYBEL_3: 11;

          ( uparrow u) c= S by A6, A7, WAYBEL11: 42;

          hence thesis by A8;

        end;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    

     Lm13: for T be lower-bounded continuous Scott TopLattice holds the set of all ( wayabove x) where x be Element of T is Basis of T

    proof

      let T be lower-bounded continuous Scott TopLattice;

      set B = the set of all ( wayabove x) where x be Element of T;

      

       A1: B c= the topology of T

      proof

        let e be object;

        assume e in B;

        then

        consider x be Element of T such that

         A2: e = ( wayabove x);

        ( wayabove x) is open by Lm11;

        hence thesis by A2;

      end;

      then

      reconsider P = B as Subset-Family of T by XBOOLE_1: 1;

      for x be Point of T holds ex B be Basis of x st B c= P

      proof

        let x be Point of T;

        reconsider p = x as Element of T;

        reconsider A = { ( wayabove q) where q be Element of T : q << p } as Basis of x by Lm12;

        take A;

        let u be object;

        assume u in A;

        then ex q be Element of T st u = ( wayabove q) & q << p;

        hence thesis;

      end;

      hence thesis by A1, YELLOW_8: 14;

    end;

    

     Lm14: for T be lower-bounded continuous Scott TopLattice, S be Subset of T holds ( Int S) = ( union { ( wayabove x) where x be Element of T : ( wayabove x) c= S })

    proof

      let T be lower-bounded continuous Scott TopLattice, S be Subset of T;

      set B = the set of all ( wayabove x) where x be Element of T;

      set I = { G where G be Subset of T : G in B & G c= S };

      set P = { ( wayabove x) where x be Element of T : ( wayabove x) c= S };

      

       A1: I = P

      proof

        thus I c= P

        proof

          let e be object;

          assume e in I;

          then

          consider G be Subset of T such that

           A2: e = G and

           A3: G in B and

           A4: G c= S;

          ex x be Element of T st G = ( wayabove x) by A3;

          hence thesis by A2, A4;

        end;

        let e be object;

        assume e in P;

        then

        consider x be Element of T such that

         A5: e = ( wayabove x) and

         A6: ( wayabove x) c= S;

        ( wayabove x) in B;

        hence thesis by A5, A6;

      end;

      B is Basis of T by Lm13;

      hence thesis by A1, YELLOW_8: 11;

    end;

    

     Lm15: for S,T be continuous lower-bounded Scott TopLattice, f be Function of S, T holds ((for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w)) implies f is continuous)

    proof

      let S,T be continuous lower-bounded Scott TopLattice;

      let f be Function of S, T;

      assume

       A1: for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w);

      

       A2: ( [#] T) <> {} ;

      now

        let U1 be Subset of T;

        assume

         A3: U1 is open;

        set U19 = U1;

        

         A4: U19 is upper by A3, WAYBEL11:def 4;

        reconsider fU = (f " U1) as Subset of S;

        

         A5: ( Int fU) c= fU by TOPS_1: 16;

        fU c= ( Int fU)

        proof

          let xx be object;

          assume

           A6: xx in fU;

          then

          reconsider x = xx as Element of S;

          

           A7: (f . x) in U1 by A6, FUNCT_1:def 7;

          reconsider p = (f . x) as Element of T;

          consider u be Element of T such that

           A8: u << p and

           A9: u in U19 by A3, A7, Lm10;

          consider w be Element of S such that

           A10: w << x and

           A11: u << (f . w) by A1, A8;

          (f .: ( wayabove w)) c= U1

          proof

            let h be object;

            assume h in (f .: ( wayabove w));

            then

            consider z be object such that

             A12: z in ( dom f) and

             A13: z in ( wayabove w) and

             A14: h = (f . z) by FUNCT_1:def 6;

            reconsider z as Element of S by A12;

            w << z by A13, WAYBEL_3: 8;

            then u << (f . z) by A1, A11;

            then u <= (f . z) by WAYBEL_3: 1;

            hence thesis by A4, A9, A14;

          end;

          then

           A15: (f " (f .: ( wayabove w))) c= (f " U1) by RELAT_1: 143;

          ( wayabove w) c= (f " (f .: ( wayabove w))) by FUNCT_2: 42;

          then

           A16: ( wayabove w) c= (f " U1) by A15;

          

           A17: ( Int fU) = ( union { ( wayabove g) where g be Element of S : ( wayabove g) c= fU }) by Lm14;

          

           A18: x in ( wayabove w) by A10;

          ( wayabove w) in { ( wayabove g) where g be Element of S : ( wayabove g) c= fU } by A16;

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

        end;

        hence (f " U1) is open by A5, XBOOLE_0:def 10;

      end;

      hence f is continuous by A2, TOPS_2: 43;

    end;

    begin

    theorem :: WAYBEL17:21

    for S,T be complete Scott TopLattice, f be Function of S, T holds f is continuous iff for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N)) by Lm4, Lm8, Lm9;

    theorem :: WAYBEL17:22

    

     Th22: for S,T be complete Scott TopLattice, f be Function of S, T holds f is continuous iff f is directed-sups-preserving

    proof

      let S,T be complete Scott TopLattice, f be Function of S, T;

      thus f is continuous implies f is directed-sups-preserving

      proof

        assume f is continuous;

        then for N be net of S holds (f . ( lim_inf N)) <= ( lim_inf (f * N)) by Lm9;

        hence thesis by Lm8;

      end;

      thus thesis by Lm4;

    end;

    registration

      let S,T be complete Scott TopLattice;

      cluster continuous -> directed-sups-preserving for Function of S, T;

      coherence by Th22;

      cluster directed-sups-preserving -> continuous for Function of S, T;

      coherence by Th22;

    end

    

     Lm16: for S,T be continuous complete Scott TopLattice, f be Function of S, T holds ((for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T))) implies f is directed-sups-preserving)

    proof

      let S,T be continuous complete Scott TopLattice, f be Function of S, T;

      assume for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T));

      then for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w) by Th14;

      then f is continuous by Lm15;

      hence thesis;

    end;

    theorem :: WAYBEL17:23

    

     Th23: for S,T be continuous complete Scott TopLattice, f be Function of S, T holds (f is continuous iff for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w))

    proof

      let S,T be continuous complete Scott TopLattice, f be Function of S, T;

      hereby

        assume f is continuous;

        then for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)) by Th12;

        hence for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w) by Th14;

      end;

      thus thesis by Lm15;

    end;

    theorem :: WAYBEL17:24

    

     Th24: for S,T be continuous complete Scott TopLattice, f be Function of S, T holds (f is continuous iff for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)))

    proof

      let S,T be continuous complete Scott TopLattice, f be Function of S, T;

      thus f is continuous implies for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)) by Th12;

      assume for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T));

      then f is directed-sups-preserving by Lm16;

      hence thesis;

    end;

    

     Lm17: for S,T be complete Scott TopLattice, f be Function of S, T holds S is algebraic & T is algebraic implies ((for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w)) implies for x be Element of S, k be Element of T st k in the carrier of ( CompactSublatt T) holds (k <= (f . x) iff ex j be Element of S st j in the carrier of ( CompactSublatt S) & j <= x & k <= (f . j)))

    proof

      let S,T be complete Scott TopLattice, f be Function of S, T;

      assume that

       A1: S is algebraic and

       A2: T is algebraic;

      

       A3: S is continuous by A1, WAYBEL_8: 7;

      

       A4: T is continuous by A2, WAYBEL_8: 7;

      assume

       A5: for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w);

      then

       A6: f is continuous by A3, A4, Th23;

      let x be Element of S, k be Element of T;

      assume

       A7: k in the carrier of ( CompactSublatt T);

      hereby

        assume k <= (f . x);

        then k << (f . x) by A7, WAYBEL_8: 1;

        then

        consider w be Element of S such that

         A8: w << x and

         A9: k << (f . w) by A5;

        consider w1 be Element of S such that

         A10: w1 in the carrier of ( CompactSublatt S) and

         A11: w <= w1 and

         A12: w1 <= x by A1, A8, WAYBEL_8: 7;

        

         A13: k <= (f . w) by A9, WAYBEL_3: 1;

        take w1;

        thus w1 in the carrier of ( CompactSublatt S) by A10;

        thus w1 <= x by A12;

        (f . w) <= (f . w1) by A6, A11, WAYBEL_1:def 2;

        hence k <= (f . w1) by A13, ORDERS_2: 3;

      end;

      given j be Element of S such that j in the carrier of ( CompactSublatt S) and

       A14: j <= x and

       A15: k <= (f . j);

      f is continuous by A3, A4, A5, Lm15;

      then (f . j) <= (f . x) by A14, WAYBEL_1:def 2;

      hence thesis by A15, ORDERS_2: 3;

    end;

    

     Lm18: for S,T be complete Scott TopLattice, f be Function of S, T holds T is algebraic implies ((for x be Element of S, k be Element of T st k in the carrier of ( CompactSublatt T) holds (k <= (f . x) iff ex j be Element of S st j in the carrier of ( CompactSublatt S) & j <= x & k <= (f . j))) implies for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w))

    proof

      let S,T be complete Scott TopLattice, f be Function of S, T;

      assume that

       A1: T is algebraic;

      assume

       A2: for x be Element of S, k be Element of T st k in the carrier of ( CompactSublatt T) holds (k <= (f . x) iff ex j be Element of S st j in the carrier of ( CompactSublatt S) & j <= x & k <= (f . j));

      let x be Element of S, y be Element of T;

      hereby

        assume y << (f . x);

        then

        consider w be Element of T such that

         A3: w in the carrier of ( CompactSublatt T) and

         A4: y <= w and

         A5: w <= (f . x) by A1, WAYBEL_8: 7;

        consider j be Element of S such that

         A6: j in the carrier of ( CompactSublatt S) and

         A7: j <= x and

         A8: w <= (f . j) by A2, A3, A5;

        take j;

        thus j << x by A6, A7, WAYBEL_8: 1;

        thus y << (f . j) by A3, A4, A8, WAYBEL_8: 1;

      end;

      given w be Element of S such that

       A9: w << x and

       A10: y << (f . w);

      consider h be Element of T such that

       A11: h in the carrier of ( CompactSublatt T) and

       A12: y <= h and

       A13: h <= (f . w) by A1, A10, WAYBEL_8: 7;

      consider j be Element of S such that

       A14: j in the carrier of ( CompactSublatt S) and

       A15: j <= w and

       A16: h <= (f . j) by A2, A11, A13;

      j << x by A9, A15, WAYBEL_3: 2;

      then j <= x by WAYBEL_3: 1;

      then h <= (f . x) by A2, A11, A14, A16;

      hence thesis by A11, A12, WAYBEL_8: 1;

    end;

    

     Lm19: for S,T be complete Scott TopLattice, f be Function of S, T holds S is algebraic & T is algebraic implies ((for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T))) implies for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T)))

    proof

      let S,T be complete Scott TopLattice, f be Function of S, T;

      assume that

       A1: S is algebraic and

       A2: T is algebraic;

      

       A3: S is continuous by A1, WAYBEL_8: 7;

      

       A4: T is continuous by A2, WAYBEL_8: 7;

      assume

       A5: for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T));

      let x be Element of S;

      

       A6: the carrier of S c= ( dom f) by FUNCT_2:def 1;

      defpred P[ Element of S] means $1 <= x & $1 is compact;

      deffunc A( Element of S) = $1;

      

       A7: (f .: { A(w) where w be Element of S : P[w] }) = { (f . A(w)) where w be Element of S : P[w] } from FuncFraenkelS( A6);

      

       A8: (f .: { w where w be Element of S : w <= x & w is compact }) = (f .: ( compactbelow x)) by WAYBEL_8:def 2;

      reconsider D = ( compactbelow x) as non empty directed Subset of S by A1, WAYBEL_8:def 4;

      f is directed-sups-preserving by A3, A4, A5, Lm16;

      then

       A9: f preserves_sup_of D;

      

       A10: ex_sup_of (D,S) by YELLOW_0: 17;

      S is satisfying_axiom_K by A1, WAYBEL_8:def 4;

      

      then (f . x) = (f . ( sup D)) by WAYBEL_8:def 3

      .= ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T)) by A7, A8, A9, A10;

      hence thesis;

    end;

    theorem :: WAYBEL17:25

    

     Th25: for S be LATTICE, T be complete LATTICE, f be Function of S, T holds (for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T))) implies f is monotone

    proof

      let S be LATTICE, T be complete LATTICE, f be Function of S, T;

      assume

       A1: for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T));

      thus f is monotone

      proof

        let X,Y be Element of S;

        assume X <= Y;

        then

         A2: ( compactbelow X) c= ( compactbelow Y) by WAYBEL13: 1;

        

         A3: (f . X) = ( "\/" ({ (f . w) where w be Element of S : w <= X & w is compact },T)) by A1;

        

         A4: (f . Y) = ( "\/" ({ (f . w) where w be Element of S : w <= Y & w is compact },T)) by A1;

        

         A5: the carrier of S c= ( dom f) by FUNCT_2:def 1;

        defpred P[ Element of S] means $1 <= X & $1 is compact;

        defpred Q[ Element of S] means $1 <= Y & $1 is compact;

        deffunc A( Element of S) = $1;

        (f .: { A(w) where w be Element of S : P[w] }) = { (f . A(w)) where w be Element of S : P[w] } from FuncFraenkelSL( A5);

        then

         A6: (f . X) = ( "\/" ((f .: ( compactbelow X)),T)) by A3, WAYBEL_8:def 2;

        (f .: { A(w) where w be Element of S : Q[w] }) = { (f . A(w)) where w be Element of S : Q[w] } from FuncFraenkelSL( A5);

        then

         A7: (f . Y) = ( "\/" ((f .: ( compactbelow Y)),T)) by A4, WAYBEL_8:def 2;

        

         A8: ex_sup_of ((f .: ( compactbelow X)),T) by YELLOW_0: 17;

         ex_sup_of ((f .: ( compactbelow Y)),T) by YELLOW_0: 17;

        hence thesis by A2, A6, A7, A8, RELAT_1: 123, YELLOW_0: 34;

      end;

    end;

    theorem :: WAYBEL17:26

    

     Th26: for S,T be complete Scott TopLattice, f be Function of S, T holds ((for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T))) implies for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)))

    proof

      let S,T be complete Scott TopLattice, f be Function of S, T;

      assume

       A1: for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T));

      then

       A2: f is monotone by Th25;

      let x be Element of S;

      

       A3: (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T)) by A1;

      set FW = { (f . w) where w be Element of S : w <= x & w is compact };

      set FX = { (f . w) where w be Element of S : w << x };

      set fx = (f . x);

      

       A4: FW c= FX

      proof

        let a be object;

        assume a in { (f . w) where w be Element of S : w <= x & w is compact };

        then

        consider w be Element of S such that

         A5: a = (f . w) and

         A6: w <= x and

         A7: w is compact;

        w << w by A7;

        then w << x by A6, WAYBEL_3: 2;

        hence thesis by A5;

      end;

      

       A8: fx is_>=_than FX

      proof

        let b be Element of T;

        assume b in FX;

        then

        consider ww be Element of S such that

         A9: b = (f . ww) and

         A10: ww << x;

        ww <= x by A10, WAYBEL_3: 1;

        hence thesis by A2, A9;

      end;

      for b be Element of T st b is_>=_than FX holds fx <= b

      proof

        let b be Element of T;

        assume b is_>=_than FX;

        then b is_>=_than FW by A4;

        hence thesis by A3, YELLOW_0: 32;

      end;

      hence thesis by A8, YELLOW_0: 30;

    end;

    theorem :: WAYBEL17:27

    for S,T be complete Scott TopLattice, f be Function of S, T holds S is algebraic & T is algebraic implies (f is continuous iff for x be Element of S, k be Element of T st k in the carrier of ( CompactSublatt T) holds (k <= (f . x) iff ex j be Element of S st j in the carrier of ( CompactSublatt S) & j <= x & k <= (f . j)))

    proof

      let S,T be complete Scott TopLattice, f be Function of S, T;

      assume that

       A1: S is algebraic and

       A2: T is algebraic;

      

       A3: S is continuous by A1, WAYBEL_8: 7;

      

       A4: T is continuous by A2, WAYBEL_8: 7;

      hereby

        assume f is continuous;

        then for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w) by A3, A4, Th23;

        hence for x be Element of S, k be Element of T st k in the carrier of ( CompactSublatt T) holds (k <= (f . x) iff ex j be Element of S st j in the carrier of ( CompactSublatt S) & j <= x & k <= (f . j)) by A1, A2, Lm17;

      end;

      assume for x be Element of S, k be Element of T st k in the carrier of ( CompactSublatt T) holds (k <= (f . x) iff ex j be Element of S st j in the carrier of ( CompactSublatt S) & j <= x & k <= (f . j));

      then for x be Element of S, y be Element of T holds y << (f . x) iff ex w be Element of S st w << x & y << (f . w) by A2, Lm18;

      hence thesis by A3, A4, Th23;

    end;

    theorem :: WAYBEL17:28

    for S,T be complete Scott TopLattice, f be Function of S, T holds S is algebraic & T is algebraic implies (f is continuous iff for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T)))

    proof

      let S,T be complete Scott TopLattice, f be Function of S, T;

      assume that

       A1: S is algebraic and

       A2: T is algebraic;

      

       A3: S is continuous by A1, WAYBEL_8: 7;

      

       A4: T is continuous by A2, WAYBEL_8: 7;

      hereby

        assume f is continuous;

        then for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)) by A3, A4, Th24;

        hence for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T)) by A1, A2, Lm19;

      end;

      assume for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w <= x & w is compact },T));

      then for x be Element of S holds (f . x) = ( "\/" ({ (f . w) where w be Element of S : w << x },T)) by Th26;

      hence thesis by A3, A4, Th24;

    end;

    theorem :: WAYBEL17:29

    for S,T be up-complete Scott non empty reflexive transitive antisymmetric TopSpace-like TopRelStr, f be Function of S, T holds f is directed-sups-preserving implies f is continuous by Lm4;