The Mizar article:

On the Order-consistent Topology of Complete and Uncomplete Lattices

by
Ewa Gradzka

Received May 23, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: WAYBEL32
[ MML identifier index ]


environ

 vocabulary WAYBEL_9, WAYBEL_0, CANTOR_1, WAYBEL11, BHSP_3, PRELAMB, YELLOW_9,
      PRE_TOPC, RELAT_2, ORDINAL2, CONNSP_2, REALSET1, SETFAM_1, BOOLE,
      WAYBEL19, TARSKI, FINSET_1, SUBSET_1, YELLOW_2, RELAT_1, TOPS_1,
      QUANTAL1, LATTICE3, YELLOW_0, FUNCT_1, ORDERS_1, LATTICES, SEQM_3,
      YELLOW_6, PROB_1, T_0TOPSP, FUNCT_3, WAYBEL21, CAT_1, ARYTM_3, WAYBEL_7,
      WAYBEL32, RLVECT_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1,
      STRUCT_0, REALSET1, FUNCT_2, ORDERS_1, LATTICE3, PRE_TOPC, TOPS_1,
      TOPS_2, CONNSP_2, T_0TOPSP, GROUP_1, YELLOW_0, WAYBEL_0, CANTOR_1,
      YELLOW_2, WAYBEL_2, YELLOW_6, WAYBEL_9, RELSET_1, WAYBEL11, WAYBEL19,
      YELLOW_9, WAYBEL21;
 constructors WAYBEL_1, CANTOR_1, TOPS_1, TOPS_2, WAYBEL_3, TSP_1, WAYBEL11,
      YELLOW_9, GROUP_1, TOLER_1, WAYBEL_5, WAYBEL21, BORSUK_1, MEMBERED,
      PARTFUN1;
 clusters STRUCT_0, LATTICE3, WAYBEL_0, FINSET_1, YELLOW_6, WAYBEL_3, WAYBEL11,
      WAYBEL21, YELLOW_9, RELSET_1, SUBSET_1, YELLOW14, WAYBEL29, MEMBERED,
      ZFMISC_1, FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, WAYBEL_0, WAYBEL11, LATTICE3, WAYBEL_9, XBOOLE_0;
 theorems YELLOW_9, CANTOR_1, PRE_TOPC, WAYBEL_0, CONNSP_2, WAYBEL11, ZFMISC_1,
      TARSKI, REALSET1, YELLOW_6, ORDERS_1, TOPS_2, TOPS_1, YELLOW_8, YELLOW_0,
      RELAT_1, FUNCT_1, YELLOW_2, SUBSET_1, LATTICE3, FINSET_1, WAYBEL_2,
      SETFAM_1, TSP_1, WAYBEL_9, WAYBEL21, WAYBEL_8, FUNCT_2, RELSET_1,
      XBOOLE_0, XBOOLE_1;
 schemes COMPLSP1, FRAENKEL, DOMAIN_1, COMPTS_1, FUNCT_2;

begin

definition
 let T be non empty TopRelStr;
 attr T is upper means
  :Def1:
  {(downarrow x)` where x is Element of T: not contradiction} is prebasis of T;
end;

definition
 cluster Scott up-complete strict TopLattice;
 existence
  proof consider R being complete LATTICE;
   consider T being strict Scott correct TopAugmentation of R;
   take T; thus thesis;
  end;
end;

definition
 let T be TopSpace-like non empty reflexive TopRelStr;
 attr T is order_consistent means
  :Def2:
  for x being Element of T holds downarrow x = Cl {x} &
  for N being eventually-directed net of T st x = sup N
  for V being a_neighborhood of x holds N is_eventually_in V;
end;

definition
cluster trivial -> upper (non empty reflexive TopSpace-like TopRelStr);
 coherence
  proof let T be non empty reflexive TopSpace-like TopRelStr;
   assume
A1:  T is trivial;
   set BB = {(downarrow x)` where x is Element of T: not contradiction};
      BB c= bool the carrier of T
     proof let a be set; assume a in BB;
       then ex x being Element of T st a = (downarrow x)`;
      hence thesis;
     end;
   then reconsider C = BB as Subset-Family of T by SETFAM_1:def
7;
   reconsider C as Subset-Family of T;
A2: BB c= the topology of T
     proof let a be set; assume a in BB;
      then consider x being Element of T such that
A3:    a = (downarrow x)`;
         a c= {}
        proof let y be set; assume
A4:       y in a;
          then y in the carrier of T & x <= x by A3;
          then y = x & x in downarrow x by A1,REALSET1:def 20,WAYBEL_0:17;
          then x in (downarrow x) /\ a & (downarrow x) misses a
           by A3,A4,PRE_TOPC:26,XBOOLE_0:def 3;
         hence thesis by XBOOLE_0:def 7;
        end;
       then a = {} by XBOOLE_1:3;
      hence thesis by PRE_TOPC:5;
     end;
   reconsider F = {the carrier of T} as Basis of T by A1,YELLOW_9:10;
      BB = {{}}
     proof
      thus BB c= {{}}
       proof let a be set; assume a in BB;
        then consider x being Element of T such that
A5:      a = (downarrow x)`;
           x <= x;
         then the carrier of T = {x} & x in downarrow x
          by A1,WAYBEL_0:17,YELLOW_9:9;
         then a = {} or a = the carrier of T & not x in a
          by A5,YELLOW_6:10,ZFMISC_1:39;
        hence thesis by TARSKI:def 1;
       end;
      consider x being Element of T;
         x <= x;
       then the carrier of T = {x} & x in downarrow x by A1,WAYBEL_0:17,
YELLOW_9:9;
       then (downarrow x)` = {} or (downarrow x)` = the carrier of T &
       not x in (downarrow x)` by YELLOW_6:10,ZFMISC_1:39;
       then {} in BB;
      hence thesis by ZFMISC_1:37;
     end;
    then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11;
    then F c= FinMeetCl C by ZFMISC_1:12;
   hence BB is prebasis of T by A2,CANTOR_1:def 5;
 end;
end;

definition
 cluster upper trivial up-complete strict TopLattice;
  existence
   proof
    consider T being trivial up-complete strict TopLattice;
     take T;
    thus thesis;
   end;
  end;

theorem Th1:
 for T being upper up-complete (non empty TopPoset)
 for A being Subset of T st A is open holds A is upper
  proof let T be upper up-complete (non empty TopPoset);
   let A be Subset of T such that
A1: A is open;
A2:  A in the topology of T by A1,PRE_TOPC:def 5;
   reconsider BB = {(downarrow x)` where x is Element of T: not contradiction}
     as prebasis of T by Def1;
    consider F being Basis of T such that
A3:  F c= FinMeetCl BB by CANTOR_1:def 5;
       the topology of T c= UniCl F by CANTOR_1:def 2;
    then consider Y being Subset-Family of T such that
A4:  Y c= F & A = union Y by A2,CANTOR_1:def 1;
   let x,y be Element of T; assume x in A;
    then consider Z being set such that
A5:  x in Z & Z in Y by A4,TARSKI:def 4;
       Z in F by A4,A5;
    then consider X being Subset-Family of T such that
A6:  X c= BB & X is finite & Z = Intersect X by A3,CANTOR_1:def 4;
    assume
A7:  x <= y;
        now let Q be set; assume
A8:    Q in X;
        then Q in BB by A6;
        then consider z being Element of T such that
A9:      Q = (downarrow z)`;
            x in Q & (downarrow z) misses Q by A5,A6,A8,A9,CANTOR_1:10,PRE_TOPC
:26;
            then not x in downarrow z by XBOOLE_0:3;
           then not x <= z by WAYBEL_0:17;
          then not y <= z by A7,ORDERS_1:26;
         then not y in downarrow z by WAYBEL_0:17;
        then y in (the carrier of T) \ downarrow z & the carrier of T = [#]T
         by PRE_TOPC:12,XBOOLE_0:def 4;
       hence y in Q by A9,PRE_TOPC:17;
      end;
    then y in Z by A6,CANTOR_1:10;
   hence thesis by A4,A5,TARSKI:def 4;
  end;

theorem
   for T being up-complete (non empty TopPoset) holds
 T is upper implies T is order_consistent
  proof
   let T be up-complete (non empty TopPoset);
    assume
A1:  T is upper;
     then reconsider BB = {(downarrow x)` where x is Element of T: not
contradiction}
      as prebasis of T by Def1;

  for x being Element of T holds downarrow x = Cl {x} &
    for N being eventually-directed net of T st x = sup N
    for V being a_neighborhood of x holds N is_eventually_in V
     proof
      let x be Element of T;

     thus downarrow x = Cl {x}
      proof
       thus downarrow x c= Cl {x}
        proof
         let a be set;
          assume A2:a in downarrow x;
             then reconsider a' = a as Point of T;
                for G being Subset of T st G is open holds
               a' in G implies {x} meets G
                proof
                 let G be Subset of T such that
A3:               G is open;assume
A4:                a' in G;
                    reconsider v = a' as Element of T;
A5:                  v <= x by A2,WAYBEL_0:17;
                       G is upper by A1,A3,Th1;
then A6:                 x in G by A4,A5,WAYBEL_0:def 20;
                     x in {x} by TARSKI:def 1;
                 hence {x} meets G by A6,XBOOLE_0:3;
                end;
         hence a in Cl {x} by PRE_TOPC:54;
        end;
       thus Cl {x} c= downarrow x
        proof
         let a be set;assume
A7:       a in Cl{x};
              reconsider BB as Subset-Family of T;
A8:             (downarrow x)` in BB;
                 BB is open by YELLOW_9:28;
then A9:           (downarrow x)` is open by A8,TOPS_2:def 1;
               (downarrow x)` = [#]T\downarrow x by PRE_TOPC:17;
then A10:         downarrow x is closed by A9,PRE_TOPC:def 6;
            x <= x;
          then x in downarrow x by WAYBEL_0:17;
          then {x} c= downarrow x by ZFMISC_1:37;
          hence a in downarrow x by A7,A10,PRE_TOPC:45;
        end;
      end;

     thus for N being eventually-directed net of T st x = sup N
          for V being a_neighborhood of x holds N is_eventually_in V
      proof
       let N be eventually-directed net of T such that
A11:     x = sup N;
A12:      x = Sup the mapping of N by A11,WAYBEL_2:def 1
          .= sup rng the mapping of N by YELLOW_2:def 5
          .= sup rng netmap (N,T) by WAYBEL_0:def 7;
       let V be a_neighborhood of x;
A13:      x in Int V by CONNSP_2:def 1;
            FinMeetCl BB is Basis of T by YELLOW_9:23;
then A14:        the topology of T = UniCl FinMeetCl BB by YELLOW_9:22;
              Int V is open by TOPS_1:51;
           then Int V in the topology of T by PRE_TOPC:def 5;
          then consider Y being Subset-Family of T such that
A15:        Y c= FinMeetCl BB & Int V = union Y by A14,CANTOR_1:def 1;
          consider Y1 being set such that
A16:        x in Y1 & Y1 in Y by A13,A15,TARSKI:def 4;
          consider Z being Subset-Family of T such that
A17:        Z c= BB & Z is finite & Y1 = Intersect Z by A15,A16,CANTOR_1:def 4;
          reconsider rngN = rng netmap (N,T) as Subset of T;
             rngN is directed by WAYBEL_2:18;
            then ex a being Element of T st a is_>=_than rngN &
             for b being Element of T st b is_>=_than rngN holds a <= b
              by WAYBEL_0:def 39;
then A18:         ex_sup_of rngN,T by YELLOW_0:15;
A19:      rngN = rng the mapping of N by WAYBEL_0:def 7;
         defpred P[set,set] means
         for i,j being Element of N st i = $2 & j >= i holds N.j in $1;
A20:     for Q being set st Q in Z ex b being set st b in the carrier of N &
           P[Q,b]
          proof let Q be set; assume
A21:      Q in Z;
            then Q in BB by A17;
             then consider v1 being Element of T such that
A22:          Q = (downarrow v1)`;
                 x in (downarrow v1)` by A16,A17,A21,A22,CANTOR_1:10;
                then x in [#]T\downarrow v1 by PRE_TOPC:17;
                 then x in [#]T & not x in downarrow v1 by XBOOLE_0:def 4;
then A23:             x in [#]T & not x <= v1 by WAYBEL_0:17;
                   not (rngN c= downarrow v1)
                  proof
                   assume
A24:               rngN c= downarrow v1;
                       ex_sup_of downarrow v1,T by WAYBEL_0:34;
                      then sup rngN <= sup downarrow v1 by A18,A24,YELLOW_0:34
;
                   hence contradiction by A12,A23,WAYBEL_0:34;
                  end;
                  then consider w be set such that
A25:                w in rngN & not w in downarrow v1 by TARSKI:def 3;
                  reconsider w' = w as Element of T by A25;
                  w' in the carrier of T;
               then w' in [#]T by PRE_TOPC:12;
             then w' in [#]T\downarrow v1 by A25,XBOOLE_0:def 4;
then A26:         w' in Q by A22,PRE_TOPC:17;
           consider i being set such that
A27:        i in dom the mapping of N and
A28:       w' = (the mapping of N).i by A19,A25,FUNCT_1:def 5;
         reconsider i as Element of N by A27;
A29:   i in the carrier of N & N.i in Q by A26,A28,WAYBEL_0:def 8;
      consider b being Element of N such that
A30:    for l being Element of N st b <= l holds N.i <= N.l by WAYBEL_0:11;
        take b;
         thus b in the carrier of N;
         thus for j,k being Element of N st j = b & k >= j holds N.k in Q
          proof
           let j,k be Element of N such that
A31:         j = b & k >= j;
A32:          N.i <= N.k by A30,A31;
                  N.k in the carrier of T;
then A33:              N.k in [#]T by PRE_TOPC:12;
                   N.i in [#]T\downarrow v1 by A22,A29,PRE_TOPC:17;
                then N.i in [#]T & not N.i in downarrow v1 by XBOOLE_0:def 4;
               then N.i in [#]T & not N.i <= v1 by WAYBEL_0:17;
              then not N.k <= v1 by A32,ORDERS_1:26;
             then not N.k in downarrow v1 by WAYBEL_0:17;
            then N.k in [#]T\downarrow v1 by A33,XBOOLE_0:def 4;
           hence N.k in Q by A22,PRE_TOPC:17;
          end;
         end;
       consider f be Function such that
A34:    dom f = Z & rng f c= the carrier of N and
A35:    for Q being set st Q in Z holds P[Q,f.Q] from NonUniqBoundFuncEx(A20);
       reconsider rngf = rng f as finite Subset of [#]N by A17,A34,FINSET_1:26,
PRE_TOPC:12;
          [#]N is directed by WAYBEL_0:def 6;
       then consider k being Element of N such that
A36:     k in [#]N & k is_>=_than rngf by WAYBEL_0:1;
       take k;
        let k1 be Element of N such that
A37:     k <= k1;
            now let Q be set; assume
A38:       Q in Z;
then A39:        f.Q in rngf by A34,FUNCT_1:def 5;
             then reconsider j = f.Q as Element of N by A34;
               j <= k by A36,A39,LATTICE3:def 9;
            then j <= k1 by A37,ORDERS_1:26;
           hence N.k1 in Q by A35,A38;
          end;
         then N.k1 in Y1 & Y1 c= union Y by A16,A17,CANTOR_1:10,ZFMISC_1:92;
         then N.k1 in Int V & Int V c= V by A15,TOPS_1:44;
        hence N.k1 in V;
      end;
     end;
   hence T is order_consistent by Def2;
  end;

canceled 4;

theorem Th7:
for R being up-complete (non empty reflexive transitive antisymmetric
     RelStr)
 ex T being TopAugmentation of R st T is Scott
  proof let R be up-complete (non empty reflexive transitive antisymmetric
     RelStr);
   set To = {A where A is Subset of R:A is inaccessible upper};
     To c= bool the carrier of R
    proof
     let a be set; assume a in To;
      then ex y being Subset of R st a = y & y is inaccessible upper;
     hence thesis;
    end;
   then reconsider top = To as Subset-Family of R
     by SETFAM_1:def 7;
   reconsider top as Subset-Family of R;
     TopRelStr(#the carrier of R, the InternalRel of R, top#) is
    TopAugmentation of R
     proof
         the RelStr of TopRelStr(#the carrier of R, the InternalRel of R, top#)
         = the RelStr of R;
      hence thesis by YELLOW_9:def 4;
     end;
   then reconsider T=TopRelStr(#the carrier of R, the InternalRel of R, top#)
    as TopAugmentation of R;
   take T;
   thus T is Scott
    proof
     let S be Subset of T;
    thus S is open implies S is inaccessible upper
     proof
      assume S is open;
       then S in the topology of T by PRE_TOPC:def 5;
        then consider Y being Subset of R such that
A1:      S = Y & Y is inaccessible upper;
          the RelStr of R = the RelStr of T;
       hence S is inaccessible upper by A1,WAYBEL_0:25,YELLOW_9:47;
      end;
     assume A2: S is inaccessible upper;
A3:   the RelStr of R = the RelStr of T;
      reconsider S' = S as Subset of R;
        S' is inaccessible
       proof
        let D be non empty directed Subset of R such that
A4:      sup D in S';
       reconsider E = D as Subset of T;
          ex a being Element of R st a is_>=_than D &
         for b being Element of R st b is_>=_than D holds a <= b
          by WAYBEL_0:def 39;
           then ex_sup_of D,R by YELLOW_0:15;
         then E is directed & sup D = sup E by A3,WAYBEL_0:3,YELLOW_0:26;
        hence D meets S' by A2,A4,WAYBEL11:def 1;
       end;
      then S' is inaccessible upper by A2,A3,WAYBEL_0:25;
      then S' in top;
     hence S is open by PRE_TOPC:def 5;
    end;
  end;

theorem Th8:
 for R being up-complete (non empty Poset)
  for T being TopAugmentation of R holds T is Scott implies T is correct
proof
 let R be up-complete (non empty Poset),
     T be TopAugmentation of R;
  assume T is Scott;
  then reconsider T as Scott TopAugmentation of R;
    T is correct;
  hence thesis;
end;

definition
 let R be up-complete (non empty reflexive transitive antisymmetric
     RelStr);
 cluster Scott -> correct TopAugmentation of R;
 coherence by Th8;
end;

definition
 let R be up-complete (non empty reflexive transitive antisymmetric
     RelStr);
 cluster Scott correct TopAugmentation of R;
 existence
  proof
   consider T being TopAugmentation of R such that A1: T is Scott by Th7;
   take T;
   thus thesis by A1,Th8;
  end;
end;

theorem Th9:  :: Remark 1.4 (ii)
 for T being Scott up-complete (non empty reflexive transitive antisymmetric
     TopRelStr), x being Element of T
  holds Cl {x} = downarrow x
proof let T be Scott up-complete (non empty reflexive transitive
             antisymmetric TopRelStr), x be Element of T;
  reconsider T' = T as Scott TopAugmentation of T by YELLOW_9:44;
  reconsider dx = downarrow x as Subset of T';
  reconsider A = {x} as Subset of T';
A1: downarrow x is closed by WAYBEL11:11;
     x <= x;
   then x in downarrow x by WAYBEL_0:17;
then A2: {x} c= downarrow x by ZFMISC_1:37;
     now let C be Subset of T' such that
A3:  A 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:37;
    hence dx c= C by A4,WAYBEL11:6;
   end;
 hence Cl {x} = downarrow x by A1,A2,YELLOW_8:17;
end;

theorem Th10:
 for T being up-complete Scott (non empty TopPoset) holds
  T is order_consistent
  proof let T be up-complete Scott (non empty TopPoset);
      for x being Element of T holds downarrow x = Cl {x} &
    for N being eventually-directed net of T st x = sup N
    for V being a_neighborhood of x holds N is_eventually_in V
    proof
     let x be Element of T;
        for N being eventually-directed net of T st x = sup N
          for V being a_neighborhood of x holds N is_eventually_in V
       proof
        let N be eventually-directed net of T such that
A1:      x = sup N;
            x = Sup the mapping of N by A1,WAYBEL_2:def 1;
          then x = sup rng the mapping of N by YELLOW_2:def 5;
then A2:      x = sup rng netmap (N,T) by WAYBEL_0:def 7;
        let V be a_neighborhood of x;
A3:      x in Int V by CONNSP_2:def 1;
A4:       Int V is open by TOPS_1:51;
then A5:        Int V is inaccessible by WAYBEL11:def 4;
A6:       Int V is upper Subset of T by A4,WAYBEL11:def 4;
         reconsider rngN = rng netmap (N,T) as Subset of T;
           rngN is directed by WAYBEL_2:18;
         then Int V meets rngN by A2,A3,A5,WAYBEL11:def 1;
        then consider z being set such that
A7:      z in Int V & z in rngN by XBOOLE_0:3;
        reconsider z' = z as Element of T by A7;
            rngN = rng the mapping of N by WAYBEL_0:def 7;
           then consider i being set such that
A8:      i in dom the mapping of N and
A9:     z' = (the mapping of N).i by A7,FUNCT_1:def 5;
        reconsider i as Element of N by A8;
A10:     z' = N.i by A9,WAYBEL_0:def 8;
        consider j being Element of N such that
A11:     for k being Element of N st j <= k holds N.i <= N.k by WAYBEL_0:11;
       take j;
        let l be Element of N such that A12: j <= l;
           N.i <= N.l by A11,A12;
then A13:      N.l in Int V by A6,A7,A10,WAYBEL_0:def 20;
           Int V c= V by TOPS_1:44;
        hence N.l in V by A13;
       end;
      hence thesis by Th9;
    end;
   hence T is order_consistent by Def2;
  end;

theorem Th11:
 for R being /\-complete Semilattice, Z be net of R,
     D be Subset of R st
  D = {"/\"({Z.k where k is Element of Z: k >= j},R)
            where j is Element of Z: not contradiction}
  holds D is non empty directed
proof let R be /\-complete Semilattice, Z be net of R, D be Subset of R;
 assume
A1: D = {"/\"({Z.k where k is Element of Z: k >= j},R)
            where j is Element of Z: not contradiction};
  consider j being Element of Z;
    "/\"({Z.k where k is Element of Z: k >= j},R) in D by A1;
 hence D is non empty;
 let x,y be Element of R;
 assume x in D;
  then consider jx being Element of Z such that
A2: x = "/\"({Z.k where k is Element of Z: k >= jx},R) by A1;
 assume y in D;
  then consider jy being Element of Z such that
A3: y = "/\"({Z.k where k is Element of Z: k >= jy},R) by A1;
  reconsider jx, jy as Element of Z;
  consider j being Element of Z such that
A4: j >= jx and
A5: j >= jy by YELLOW_6:def 5;
  consider j' being Element of Z such that
A6:  j' >= j & j' >= j by YELLOW_6:def 5;
  deffunc F(Element of Z) = Z.$1;
  defpred Px[Element of Z] means $1 >= jx;
  defpred Py[Element of Z] means $1 >= jy;
  defpred P[Element of Z] means $1 >= j;
  set Ex = {F(k) where k is Element of Z: Px[k]},
      Ey = {F(k) where k is Element of Z: Py[k]},
      E = {F(k) where k is Element of Z: P[k]};
A7: Z.j in Ex by A4;
A8: Z.j in Ey by A5;
A9: Z.j' in E by A6;
A10: Ex is Subset of R from SubsetFD;
A11: Ey is Subset of R from SubsetFD;
A12: E is Subset of R from SubsetFD;
 take z = "/\"({Z.k where k is Element of Z: k >= j},R);
 reconsider Ex'= Ex as non empty Subset of R by A7,A10;
 reconsider Ey' = Ey as non empty Subset of R by A8,A11;
 reconsider E' = E as non empty Subset of R by A9,A12;
A13: ex_inf_of E',R & ex_inf_of Ex',R & ex_inf_of Ey',R by WAYBEL_0:76;
 thus z in D by A1;
    E' c= Ex'
   proof let e be set;
    assume e in E';
     then consider k being Element of Z such that
A14:   e = Z.k and
A15:   k >= j;
     reconsider k as Element of Z;
       k >= jx by A4,A15,YELLOW_0:def 2;
    hence e in Ex' by A14;
   end;
 hence x <= z by A2,A13,YELLOW_0:35;
    E' c= Ey'
   proof let e be set;
    assume e in E';
     then consider k being Element of Z such that
A16:   e = Z.k and
A17:   k >= j;
     reconsider k as Element of Z;
       k >= jy by A5,A17,YELLOW_0:def 2;
    hence e in Ey' by A16;
   end;
 hence y <= z by A3,A13,YELLOW_0:35;
end;

theorem Th12:
 for R being /\-complete Semilattice,
     S being Subset of R,
     a being Element of R holds
  a in S implies "/\"(S,R) <= a
 proof let R be /\-complete Semilattice, S be Subset of R;
        let a be Element of R;
  assume A1: a in S;
then ex_inf_of S,R by WAYBEL_0:76;
   then S is_>=_than "/\"(S, R) by YELLOW_0:31;
  hence "/\"(S, R) <= a by A1,LATTICE3:def 8;
 end;

theorem Th13:
 for R being /\-complete Semilattice,
     N being monotone reflexive net of R
 holds lim_inf N = sup N
proof let R be /\-complete Semilattice, N be monotone reflexive net of R;
  deffunc F(Element of N)
   = "/\"({N.i where i is Element of N: i >= $1},R);
  deffunc G(Element of N) = N.$1;
  defpred P[set] means not contradiction;
  set X = {F(j) where j is Element of N: P[j]};
A1: for j being Element of N holds G(j) = F(j)
   proof let j be Element of N;
    defpred P[Element of N] means $1 >= j;
    set Y = {G(i) where i is Element of N: P[i]};
       j <= j;
    then
A2:  N.j in Y;
     Y is Subset of R from SubsetFD;
    then Y is non empty Subset of R by A2;
    then
A3:  ex_inf_of Y,R by WAYBEL_0:76;
A4:  N.j is_<=_than Y
      proof let y be Element of R;
       assume y in Y;
        then ex i being Element of N st
          y = N.i & j <= i;
       hence N.j <= y by WAYBEL11:def 9;
      end;
       for b being Element of R st b is_<=_than Y holds N.j >= b
      proof let b be Element of R;
       assume
A5:      b is_<=_than Y;
        reconsider j' = j as Element of N;
          j' <= j';
        then N.j' in Y;
       hence N.j >= b by A5,LATTICE3:def 8;
      end;
    hence N.j = "/\"(Y,R) by A3,A4,YELLOW_0:def 10;
   end;
    rng the mapping of N =
     {G(j) where j is Element of N: P[j]} by WAYBEL11:19
         .= X from FraenkelF'(A1);
 hence lim_inf N = "\/"(rng the mapping of N,R) by WAYBEL11:def 6
       .= Sup the mapping of N by YELLOW_2:def 5
       .= sup N by WAYBEL_2:def 1;
end;

theorem Th14:
 for R being /\-complete Semilattice
 for S being Subset of R
  holds S in the topology of ConvergenceSpace Scott-Convergence R
    iff S is inaccessible upper
  proof let R be /\-complete Semilattice;
    set SC = Scott-Convergence R, T = ConvergenceSpace SC;
A1:  the topology of T = { V where V is Subset of R:
      for p being Element of R st p in V
       for N being net of R st [N,p] in SC holds N is_eventually_in V}
         by YELLOW_6:def 27;
   let S be Subset of R;
   hereby assume S in the topology of T;
     then consider V being Subset of R such that
A2:   S = V and
A3:   for p being Element of R st p in V
       for N being net of R st [N,p] in SC holds N is_eventually_in V by A1;

    thus S is inaccessible
     proof let D be non empty directed Subset of R such that
A4:    sup D in S;
A5:     dom id D = D & rng id D = D by RELAT_1:71;
       then reconsider f = id D as Function of D, the carrier of R
                                       by FUNCT_2:def 1,RELSET_1:11;
       reconsider N = Net-Str(D,f) as strict monotone reflexive net of R
         by A5,WAYBEL11:20;
A6:     N in NetUniv R by WAYBEL11:21;
         lim_inf N = sup N by Th13
          .= Sup the mapping of N by WAYBEL_2:def 1
          .= "\/"(rng the mapping of N,R) by YELLOW_2:def 5
          .= "\/"(rng f,R) by WAYBEL11:def 10
          .= sup D by RELAT_1:71;
       then sup D is_S-limit_of N by WAYBEL11:def 7;
       then [N,sup D] in SC by A6,WAYBEL11:def 8;
       then N is_eventually_in S by A2,A3,A4;
       then consider i0 being Element of N such that
A7:     for j being Element of N st i0 <= j holds N.j in S by WAYBEL_0:def 11;
       consider j0 being Element of N such that
A8:     j0 >= i0 and j0 >= i0 by YELLOW_6:def 5;
A9:    N.j0 in S by A7,A8;
A10:     D = the carrier of N by WAYBEL11:def 10;
         N.j0 = (the mapping of N).j0 by WAYBEL_0:def 8
           .= (id D).j0 by WAYBEL11:def 10
           .= j0 by A10,FUNCT_1:35;
      hence D meets S by A9,A10,XBOOLE_0:3;
     end;
    thus S is upper
     proof let x,y be Element of R such that
A11:    x in S and
A12:    x <= y;
A13:     Net-Str y in NetUniv R by WAYBEL11:29;
         y = lim_inf Net-Str y by WAYBEL11:28;
       then x is_S-limit_of Net-Str y by A12,WAYBEL11:def 7;
       then [Net-Str y,x] in SC by A13,WAYBEL11:def 8;
       then Net-Str y is_eventually_in S by A2,A3,A11;
      hence y in S by WAYBEL11:27;
     end;
   end;
   assume that
A14: S is inaccessible and
A15: S is upper;
      for p being Element of R st p in S
     for N being net of R st [N,p] in SC holds N is_eventually_in S
     proof let p be Element of R such that
A16:    p in S;
      reconsider p' = p as Element of R;
      let N be net of R;
      assume
A17:    [N,p] in SC;
         SC c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 21;
       then A18:     N in NetUniv R by A17,ZFMISC_1:106;
     then ex N' being strict net of R st N' = N &
       the carrier of N' in the_universe_of the carrier of R by YELLOW_6:def 14
;
       then p is_S-limit_of N by A17,A18,WAYBEL11:def 8;
       then A19:      p' <= lim_inf N by WAYBEL11:def 7;
       deffunc F(Element of N)
         = "/\"({N.i where i is Element of N: i >= $1},R);
       defpred P[set] means not contradiction;
       set X ={F(j) where j is Element of N: P[j]};
         X is Subset of R from SubsetFD;
       then reconsider D = X as Subset of R;
       reconsider D as non empty directed Subset of R by Th11;
         lim_inf N = sup D by WAYBEL11:def 6;
       then sup D in S by A15,A16,A19,WAYBEL_0:def 20;
       then D meets S by A14,WAYBEL11:def 1;
       then D /\ S <> {} by XBOOLE_0:def 7;
       then consider d being Element of R such that
A20:     d in D /\ S by SUBSET_1:10;
       reconsider d as Element of R;
         d in D by A20,XBOOLE_0:def 3;
       then consider j being Element of N such that
A21:   d = "/\"({N.i where i is Element of N: i >= j},R);
       defpred P[Element of N] means $1 >= j;
       deffunc F(Element of N) = N.$1;
         {F(i) where i is Element of N: P[i]}
              is Subset of R from SubsetFD;
       then reconsider Y = {N.i where i is Element of N: i >= j}
as
       Subset of R;
       reconsider j as Element of N;
      take j;
      let i0 be Element of N;
A22:    d in S by A20,XBOOLE_0:def 3;
      assume j <= i0;
       then N.i0 in Y;
       then d <= N.i0 by A21,Th12;
      hence N.i0 in S by A15,A22,WAYBEL_0:def 20;
     end;
   hence S in the topology of T by A1;
  end;

theorem Th15:
 for R being /\-complete up-complete Semilattice,
  T being TopAugmentation of R
  st the topology of T = sigma R
  holds T is Scott
  proof let R be /\-complete up-complete Semilattice;
  let T be TopAugmentation of R such that
A1:  the topology of T = sigma R;
A2:  the RelStr of T = the RelStr of R by YELLOW_9:def 4;
A3:  sigma R = the topology of ConvergenceSpace Scott-Convergence R
    by WAYBEL11:def 12;
      T is Scott
     proof let S be Subset of T;
      reconsider A = S as Subset of R by A2;
      thus S is open implies S is inaccessible upper
        proof assume S is open;
          then S in the topology of T by PRE_TOPC:def 5;
          then A is inaccessible upper by A1,A3,Th14;
         hence thesis by A2,WAYBEL_0:25,YELLOW_9:47;
        end;
      assume A4:S is inaccessible upper;
         A is inaccessible
        proof
         let D be non empty directed Subset of R such that
A5:       sup D in A;
         reconsider E = D as Subset of T by A2;
            ex a being Element of R st a is_>=_than D &
           for b being Element of R st b is_>=_than D holds a <= b
            by WAYBEL_0:def 39;
            then ex_sup_of D,R by YELLOW_0:15;
          then E is directed & sup D = sup E by A2,WAYBEL_0:3,YELLOW_0:26;
         hence D meets A by A4,A5,WAYBEL11:def 1;
        end;
then A is inaccessible upper by A2,A4,WAYBEL_0:25;
       then A in the topology of T by A1,A3,Th14;
      hence S is open by PRE_TOPC:def 5;
     end;
   hence thesis;
  end;

definition
 let R be /\-complete up-complete Semilattice;
 cluster strict Scott correct TopAugmentation of R;
  existence
   proof
    set T = TopRelStr(#the carrier of R, the InternalRel of R, sigma R#);
       the RelStr of T = the RelStr of R;
     then reconsider T as TopAugmentation of R by YELLOW_9:def 4;
     take T;
    thus thesis by Th15,YELLOW_9:48;
  end;
end;

theorem
  for S being up-complete /\-complete Semilattice,
    T being Scott TopAugmentation of S holds
  sigma S = the topology of T
proof
  let S be up-complete /\-complete Semilattice;
  let T be Scott TopAugmentation of S;
  set CSC = ConvergenceSpace Scott-Convergence S;
  thus sigma S c= the topology of T
   proof
    let e be set;
     assume A1: e in sigma S;
then A2:   e in the topology of CSC by WAYBEL11:def 12;
      reconsider A = e as Subset of S by A1;
A3:  the RelStr of S = the RelStr of T by YELLOW_9:def 4;
      then reconsider A' = A as Subset of T;
        A is inaccessible upper by A2,Th14;
      then A' is inaccessible upper by A3,WAYBEL_0:25,YELLOW_9:47;
      then A' is open by WAYBEL11:def 4;
     hence e in the topology of T by PRE_TOPC:def 5;
   end;
  let e be set;assume
A4:   e in the topology of T;
      then reconsider A = e as Subset of T;
        A is open by A4,PRE_TOPC:def 5;
then A5:   A is inaccessible upper by WAYBEL11:def 4;
A6:   the RelStr of S = the RelStr of T by YELLOW_9:def 4;
   then reconsider A' = A as Subset of S;
        A' is inaccessible
       proof
        let D be non empty directed Subset of S such that
A7:      sup D in A';
       reconsider E = D as Subset of T by A6;
          ex a being Element of S st a is_>=_than D &
         for b being Element of S st b is_>=_than D holds a <= b
          by WAYBEL_0:def 39;
           then ex_sup_of D,S by YELLOW_0:15;
         then E is directed & sup D = sup E by A6,WAYBEL_0:3,YELLOW_0:26;
        hence D meets A' by A5,A7,WAYBEL11:def 1;
       end;
      then A' is inaccessible upper by A5,A6,WAYBEL_0:25;
       then A' in the topology of CSC by Th14;
    hence thesis by WAYBEL11:def 12;
 end;

theorem     :: Remark 1.4 (iii)
   for T being Scott up-complete (non empty reflexive transitive antisymmetric
     TopRelStr)
 holds T is T_0-TopSpace
proof let T be Scott up-complete
      (non empty reflexive transitive antisymmetric TopRelStr);
   reconsider T' = T as Scott TopAugmentation of T by YELLOW_9:44;
    now let x,y be Point of T';
     reconsider x' = x, y' = y as Element of T';
A1:  Cl {x'} = downarrow x' & Cl {y'} = downarrow y' by Th9;
    assume x <> y;
    hence Cl {x} <> Cl {y} by A1,WAYBEL_0:19;
  end;
 hence thesis by TSP_1:def 5;
end;

definition
let R be up-complete (non empty reflexive transitive antisymmetric RelStr);
cluster -> up-complete TopAugmentation of R;
coherence;
end;

theorem Th18:
 for R being up-complete (non empty reflexive transitive antisymmetric
     RelStr)
  for T being Scott TopAugmentation of R,
   x being Element of T,
     A being upper Subset of T st not x in A
  holds (downarrow x)` is a_neighborhood of A
proof let R be up-complete (non empty reflexive transitive antisymmetric
     RelStr),
          T be Scott TopAugmentation of R, x be Element of T,
          A be upper Subset of T such that
A1: not x in A;
      downarrow x is closed by WAYBEL11:11;
   then (downarrow x)` is open by TOPS_1:29;
then A2: Int (downarrow x)` = (downarrow x)` by TOPS_1:55;
    A misses downarrow x by A1,WAYBEL11:5;
  then A c= (downarrow x)` by PRE_TOPC:21;
 hence (downarrow x)` is a_neighborhood of A by A2,CONNSP_2:def 2;
end;

theorem     ::Remark 1.4 (iv)
   for R being up-complete (non empty reflexive transitive antisymmetric
     TopRelStr)
 for T being Scott TopAugmentation of R,
     S being upper Subset of T
  ex F being Subset-Family of T st S = meet F &
   for X being Subset of T st X in F holds X is a_neighborhood of S
proof let R be up-complete (non empty reflexive transitive antisymmetric
                             TopRelStr),
           T be Scott TopAugmentation of R,
           S be upper Subset of T;
  defpred P[set] means $1 is a_neighborhood of S;
  set F = { X where X is Subset of T: P[X]};
    F is Subset of bool the carrier of T from SubsetD;
  then F is Subset-Family of T by SETFAM_1:def 7;
  then reconsider F as Subset-Family of T;
 take F;
 thus S = meet F
  proof
     [#]T is a_neighborhood of S by YELLOW_6:7;
   then A1: [#]T in F;
      now let Z1 be set;
     assume Z1 in F;
      then ex X being Subset of T
         st Z1 = X & X is a_neighborhood of S;
     hence S c= Z1 by YELLOW_6:8;
    end;
   hence S c= meet F by A1,SETFAM_1:6;
   let x be set such that
A2: x in meet F and
A3: not x in S;
    reconsider p = x as Element of T by A2;
      (downarrow p)` is a_neighborhood of S by A3,Th18;
    then (downarrow p)` in F;
    then A4:   meet F c= (downarrow p)` by SETFAM_1:4;
       p <= p;
     then p in downarrow p by WAYBEL_0:17;
   hence contradiction by A2,A4,YELLOW_6:10;
  end;
 let X be Subset of T;
 assume X in F;
  then ex Y being Subset of T st X = Y & Y is a_neighborhood of
S;
 hence X is a_neighborhood of S;
end;

theorem    ::Remark 1.4 (v)
  for T being Scott up-complete (non empty reflexive transitive antisymmetric
     TopRelStr),
     S being Subset of T
  holds S is open iff S is upper property(S)
proof let T be Scott up-complete (non empty reflexive transitive antisymmetric
                                   TopRelStr),
           S be Subset of T;
 hereby assume
A1: S is open;
  hence
A2: S is upper by WAYBEL11:def 4;
  thus S has_the_property_(S)
   proof
    let D be non empty directed Subset of T such that
A3:  sup D in S;
       S is inaccessible by A1,WAYBEL11:def 4;
     then S meets D by A3,WAYBEL11:def 1;
     then consider y being set such that
A4:   y in S and
A5:   y in D by XBOOLE_0:3;
     reconsider y as Element of T by A4;
    take y;
    thus thesis by A2,A4,A5,WAYBEL_0:def 20;
   end;
 end;
 assume that
A6: S is upper and
A7: S has_the_property_(S);
    S is inaccessible
   proof let D be non empty directed Subset of T;
    assume sup D in S;
     then consider y being Element of T such that
A8:    y in D and
A9:    for x being Element of T st x in D & x >= y holds x in S by A7,WAYBEL11:
def 3;
       y >= y by YELLOW_0:def 1;
     then y in S by A8,A9;
    hence D meets S by A8,XBOOLE_0:3;
   end;
 hence S is open by A6,WAYBEL11:def 4;
end;

theorem Th21:
 for R being up-complete (non empty reflexive transitive antisymmetric
     TopRelStr),
     S being non empty directed Subset of R,
     a being Element of R holds
  a in S implies a <= "\/"(S, R)
   proof
    let R be up-complete (non empty reflexive transitive antisymmetric
     TopRelStr);
    let S be non empty directed Subset of R, a be Element of R;
    assume A1: a in S;
       ex_sup_of S,R by WAYBEL_0:75;
     then S is_<=_than "\/"(S, R) by YELLOW_0:30;
    hence a <= "\/"(S, R) by A1,LATTICE3:def 9;
   end;

::Remark 1.4 (vi)
definition let T be up-complete (non empty reflexive transitive antisymmetric
     TopRelStr);
 cluster lower -> property(S) Subset of T;
 coherence
  proof
  let S be Subset of T;
   assume
A1: S is lower;
   let D be non empty directed Subset of T such that
A2:  sup D in S;
   consider y being Element of T such that
A3:  y in D by SUBSET_1:10;
   take y;
   thus y in D by A3;
   let x be Element of T such that
A4: x in D and x >= y;
      x <= sup D by A4,Th21;
   hence x in S by A1,A2,WAYBEL_0:def 19;
  end;
end;

theorem
   for T being finite up-complete (non empty Poset),
     S being Subset of T holds S is inaccessible
proof
 let T be finite up-complete (non empty Poset),
     S be Subset of T, D be non empty directed Subset of T such that
A1: sup D in S;
      sup D in D
     proof
      reconsider D' = D as finite Subset of T;
        D' c= D';
      then reconsider E = D' as finite Subset of D;
      consider x being Element of T such that
A2:   x in D and
A3:   x is_>=_than E by WAYBEL_0:1;
A4: for b being Element of T st D is_<=_than b holds b >= x by A2,LATTICE3:def
9;
       for c being Element of T st D is_<=_than c &
     for b being Element of T st D is_<=_than b holds b >= c
      holds c = x
       proof let c be Element of T such that
A5:      D is_<=_than c and
A6:      for b being Element of T st D is_<=_than b holds b >= c;
           x >= c & c >= x by A2,A3,A5,A6,LATTICE3:def 9;
        hence c = x by ORDERS_1:25;
       end;
      then ex_sup_of D,T by A3,A4,YELLOW_0:def 7;
      hence sup D in D by A2,A3,A4,YELLOW_0:def 9;
    end;
hence thesis by A1,XBOOLE_0:3;
 end;

theorem Th23:
 for R being complete connected LATTICE,
  T being Scott TopAugmentation of R, x being Element of T holds
   (downarrow x)` is open
proof
 let R be complete connected LATTICE,
  T be Scott TopAugmentation of R, x be Element of T;
   reconsider S = downarrow x as directly_closed lower Subset of T by WAYBEL11:
8;
     S` is open;
  hence thesis;
end;

theorem
   for R being complete connected LATTICE,
     T being Scott TopAugmentation of R, S being Subset of T holds
     S is open iff S = the carrier of T or S in {(downarrow x)`
                              where x is Element of T: not contradiction}
proof
 let R be complete connected LATTICE,
     T be Scott TopAugmentation of R, S be Subset of T;
 set DD = {(downarrow x)` where x is Element of T: not contradiction};
 thus S is open implies S = the carrier of T or S in DD
  proof
   assume S is open;
then A1: S is inaccessible upper by WAYBEL11:def 4;
   assume
A2:  S <> the carrier of T & not S in DD;
A3:  the carrier of T = [#]T by PRE_TOPC:12;
then A4:      [#]T\S <> {} by A2,PRE_TOPC:23;
A5:  the RelStr of T = the RelStr of R by YELLOW_9:def 4;
     then reconsider K = S` as Subset of R;
     reconsider D = K as non empty directed Subset of T by A4,A5,PRE_TOPC:17,
WAYBEL_0:3;
      A6: D misses S by PRE_TOPC:21;
     reconsider x = sup D as Element of T;
       S` = downarrow x
      proof
       thus S` c= downarrow x
        proof
         let a be set; assume
A7:       a in S`;
           then reconsider A = a as Element of T;
             x is_>=_than S` by YELLOW_0:32;
          then A <= x by A7,LATTICE3:def 9;
         hence thesis by WAYBEL_0:17;
        end;
       let a be set; assume
A8:     a in downarrow x;
         then reconsider A = a as Element of T;
            A <= x & not x in S by A1,A6,A8,WAYBEL11:def 1,WAYBEL_0:17;
          then not A in S by A1,WAYBEL_0:def 20;
        then A in [#]T\S by A3,XBOOLE_0:def 4;
       hence thesis by PRE_TOPC:17;
      end;
     then (downarrow x)` = ([#]T\S)` by PRE_TOPC:17
                 .= [#]T\([#]T\S) by PRE_TOPC:17
                 .= S by PRE_TOPC:22;
   hence contradiction by A2;
  end;
 assume A9: S = the carrier of T or S in DD;
  per cases by A9;
   suppose A10: S = the carrier of T;
A11:   the RelStr of T = the RelStr of R by YELLOW_9:def 4;
     then S = [#]R by A10,PRE_TOPC:12;
then A12:  S is inaccessible by A11,YELLOW_9:47;
      S is upper
     proof
      let x,y be Element of T;
      assume x in S & x <= y;
      thus y in S by A10;
     end;
   hence S is open by A12,WAYBEL11:def 4;
   suppose S in DD;
     then consider x being Element of T such that
A13:  S = (downarrow x)`;
   thus S is open by A13,Th23;
end;

definition
let R be up-complete (non empty Poset);
cluster order_consistent (correct TopAugmentation of R);
correctness
 proof
  consider T being Scott correct TopAugmentation of R;
  take T;
  thus T is order_consistent by Th10;
 end;
end;

definition
cluster order_consistent complete TopLattice;
correctness
proof
 consider T being Scott complete TopLattice;
 take T;
 thus thesis by Th10;
end;
end;

theorem Th25:
for R being non empty TopRelStr
for A being Subset of R holds
 (for x being Element of R holds downarrow x = Cl {x}) implies
  (A is open implies A is upper)
proof
 let R be non empty TopRelStr,
     A be Subset of R;
assume A1: for x being Element of R holds downarrow x = Cl {x};
   assume A2: A is open;
  let x,y be Element of R such that
A3: x in A and
A4: x <= y;
      x in downarrow y by A4,WAYBEL_0:17;
    then x in Cl {y} by A1;
    then A meets {y} by A2,A3,PRE_TOPC:54;
    then consider z be set such that
A5:  z in A /\ {y} by XBOOLE_0:4;
       z in A & z in {y} by A5,XBOOLE_0:def 3;
 hence y in A by TARSKI:def 1;
end;

theorem
  for R being non empty TopRelStr
for A being Subset of R holds
 (for x being Element of R holds downarrow x = Cl {x}) implies
for A being Subset of R st A is closed holds A is lower
proof
 let R be non empty TopRelStr,
     A be Subset of R;
assume A1: for x being Element of R holds downarrow x = Cl {x};
 let A be Subset of R such that
A2: A is closed;
  let x,y be Element of R such that
A3: x in A and
A4: y <= x;
      y in downarrow x by A4,WAYBEL_0:17;
then A5: y in Cl {x} by A1;
      {x} c= A
     proof
      let a be set;
      assume a in {x};
      hence a in A by A3,TARSKI:def 1;
     end;
 hence y in A by A2,A5,PRE_TOPC:45;
end;

theorem Th27:
 for T being up-complete /\-complete LATTICE, N being net of T
 for i being Element of N holds lim_inf (N|i) = lim_inf N
  proof let T be complete LATTICE, N be net of T;
   let i be Element of N;
   reconsider M = N|i as subnet of N;
   reconsider e = incl(M,N) as Embedding of M, N by WAYBEL21:40;
      M is full SubNetStr of N by WAYBEL_9:14;
then A1: M is full SubRelStr of N by YELLOW_6:def 9;
      the carrier of M c= the carrier of N by WAYBEL_9:13;
then A2:  incl(M,N) = id the carrier of M by YELLOW_9:def 1;
      now let k be Element of N, j be Element of M;
     consider j' being Element of N such that
A3:    j' = j & j' >= i by WAYBEL_9:def 7;
     assume e.j <= k;
then A4:    k >= j' by A2,A3,FUNCT_1:35;
      then k >= i by A3,YELLOW_0:def 2;
then     k in the carrier of M by WAYBEL_9:def 7;
     then reconsider k' = k as Element of M;
     take k'; thus k' >= j by A1,A3,A4,YELLOW_0:61;
        M.k' = N.(e.k') & M.k' <= M.k' by WAYBEL21:36;
     hence N.k >= M.k' by A2,FUNCT_1:35;
    end;
   hence lim_inf (N|i) = lim_inf N by WAYBEL21:38;
  end;

definition
let S be non empty 1-sorted,
    R be non empty RelStr,
    f be Function of the carrier of R,the carrier of S;
func R*'f -> strict non empty NetStr over S means
:Def3:
the RelStr of it = the RelStr of R &
the mapping of it = f;
 existence
  proof
   reconsider M = NetStr (# the carrier of R,the InternalRel of R, f #)
   as strict non empty NetStr over S;
   take M;
   thus thesis;
  end;
 uniqueness;
end;

definition
let S be non empty 1-sorted,
    R be non empty transitive RelStr,
    f be Function of the carrier of R,the carrier of S;
cluster R*'f -> transitive;
coherence
 proof
    the RelStr of R*'f = the RelStr of R & R is transitive by Def3;
  hence R*'f is transitive by WAYBEL_8:13;
 end;
end;

definition
let S be non empty 1-sorted,
    R be non empty directed RelStr,
    f be Function of the carrier of R,the carrier of S;
cluster R*'f -> directed;
coherence
proof
A1:  the RelStr of R*'f = the RelStr of R & R is directed by Def3;
  thus [#](R*'f) is directed
   proof
A2: [#]R is directed by WAYBEL_0:def 6;
      [#](R*'f) = the carrier of R*'f by PRE_TOPC:12
            .= [#]R by A1,PRE_TOPC:12;
      hence thesis by A1,A2,WAYBEL_0:3;
   end;
end;
end;

definition
 let R be non empty RelStr,
     N be prenet of R;
func inf_net N -> strict prenet of R means
:Def4:
ex f being map of N,R st
 it = N*'f & for i being Element of N holds
  f.i = "/\"({N.k where k is Element of N: k >= i},R);
 existence
  proof
    deffunc F(Element of N)
     = "/\"({N.k where k is Element of N: k >= $1},R);
     consider g being Function of the carrier of N, the carrier of R
       such that
A1:   for i being Element of N holds g.i = F(i) from LambdaD;
     reconsider f = g as map of N,R;
     reconsider M = N*'f as strict prenet of R;
    take M;
   thus thesis by A1;
  end;
 uniqueness
  proof
   let M, P be strict prenet of R such that
A2:  ex f being map of N,R st
      M = N*'f & for i being Element of N holds
      f.i = "/\"({N.k where k is Element of N: k >= i},R) and
A3:  ex f being map of N,R st
      P = N*'f & for i being Element of N holds
      f.i = "/\"({N.k where k is Element of N: k >= i},R);
    consider f1 being map of N,R such that
A4:   M = N*'f1 & for i being Element of N holds
      f1.i = "/\"
({N.k where k is Element of N: k >= i},R) by A2;
    consider f2 being map of N,R such that
A5:   P = N*'f2 & for i being Element of N holds
      f2.i = "/\"
({N.k where k is Element of N: k >= i},R) by A3;
  for i being set st i in the carrier of N holds f1.i = f2.i
     proof
      let i be set; assume i in the carrier of N;
      then reconsider i as Element of N;
         f1.i = "/\"
({N.k where k is Element of N: k >= i},R) by A4
           .= f2.i by A5;
      hence thesis;
     end;
    hence M = P by A4,A5,FUNCT_2:18;
  end;
end;

definition
let R be non empty RelStr,
    N be net of R;
cluster inf_net N -> transitive;
coherence
 proof
    ex f being map of N,R st inf_net N = N*'f &
      for i being Element of N holds
  f.i = "/\"({N.k where k is Element of N: k >= i},R) by Def4;
  hence thesis;
 end;
end;

definition
let R be non empty RelStr,
    N be net of R;
cluster inf_net N -> directed;
coherence;
end;

definition
let R be /\-complete (non empty reflexive antisymmetric RelStr),
    N be net of R;
cluster inf_net N -> monotone;
coherence
proof
 let i,j be Element of inf_net N such that A1: i <= j;
 consider f being map of N,R such that A2: inf_net N = N*'f &
      for i being Element of N holds
       f.i = "/\"({N.k where k is Element of N: k >= i},R)
        by Def4;
A3:   the RelStr of inf_net N = the RelStr of N by A2,Def3;
  then reconsider i'=i,j'=j as Element of N;
  deffunc F(Element of N) = N.$1;
  defpred P[Element of N] means $1 >= j';
  defpred Q[Element of N] means $1 >= i';
set J= {F(k) where k is Element of N: P[k]};
set I= {F(k) where k is Element of N: Q[k]};
A4:     J is Subset of R from SubsetFD;
        consider j0 being Element of N such that
A5:      j0 >= j' & j0 >= j' by YELLOW_6:def 5;
           N.j0 in J by A5;
        then reconsider J'= J as non empty Subset of R by A4;
A6:     I is Subset of R from SubsetFD;
        consider j1 being Element of N such that
A7:      j1 >= i' & j1 >= i' by YELLOW_6:def 5;
           N.j1 in I by A7;
        then reconsider I'= I as non empty Subset of R by A6;
A8: ex_inf_of J',R & ex_inf_of I',R by WAYBEL_0:76;
A9:J' c= I'
     proof
      let a be set; assume A10: a in J';
      then reconsider x = a as Element of R;
       consider k being Element of N such that
A11:     x = N.k and
A12:     k >= j' by A10;
       reconsider i0 = i,j0 = j as Element of inf_net N;
       reconsider k' = k as Element of N;
         i0 <= j0 & i' = i0 & j' = j0 by A1;
       then i' <= j' & j' <= k' by A3,A12,YELLOW_0:1;
       then i' <= k' by YELLOW_0:def 2;
      hence a in I' by A11;
     end;
A13:  f.i' = "/\"(I,R) & f.j' = "/\"(J,R) by A2;
    the mapping of (inf_net N) = f by A2,Def3;
  then (inf_net N).i = f.i' & (inf_net N).j = f.j' by WAYBEL_0:def 8;
 hence (inf_net N).i <= (inf_net N).j by A8,A9,A13,YELLOW_0:35;
end;
end;

definition
let R be /\-complete (non empty reflexive antisymmetric RelStr),
    N be net of R;
cluster inf_net N -> eventually-directed;
coherence;
end;

theorem Th28:
for R being non empty RelStr,
    N being net of R
    holds rng the mapping of (inf_net N) =
    {"/\"({N.i where i is Element of N: i >= j},R) where
         j is Element of N: not contradiction}
proof
let R be non empty RelStr, N be net of R;
set X = {"/\"({N.i where i is Element of N: i >= j},R) where
         j is Element of N: not contradiction};
 consider f being map of N,R such that
A1:  inf_net N = N*'f &
     for i being Element of N holds
      f.i = "/\"
({N.k where k is Element of N: k >= i},R) by Def4;
A2: the RelStr of inf_net N = the RelStr of N by A1,Def3;
A3: the mapping of (inf_net N) = f by A1,Def3;
then A4: the carrier of inf_net N = dom f by FUNCT_2:def 1;
thus rng the mapping of inf_net N c=
         {"/\"({N.i where i is Element of N: i >= j},R) where
            j is Element of N: not contradiction}
 proof
  let e be set; assume e in rng the mapping of inf_net N;
   then consider u being set such that
A5: u in dom f and
A6: e = f.u by A3,FUNCT_1:def 5;
   reconsider u as Element of N by A5;
     f.u = "/\"({N.k where k is Element of N: k >= u},R) by A1;
  hence e in X by A6;
 end;
let e be set; assume
     e in {"/\"({N.i where i is Element of N: i >= j},R) where
            j is Element of N: not contradiction};
    then consider j being Element of N such that
A7:   e = "/\"({N.i where i is Element of N: i >= j},R);
        e = (the mapping of inf_net N).j by A1,A3,A7;
 hence e in rng the mapping of inf_net N by A2,A3,A4,FUNCT_1:def 5;
end;

theorem Th29:
for R being up-complete /\-complete LATTICE,
    N being net of R holds
sup inf_net N = lim_inf N
proof
let R be up-complete /\-complete LATTICE,
    N be net of R;
 defpred P[set] means not contradiction;
 deffunc F(Element of N)
  = "/\"({N.l where l is Element of N: l >= $1},R);
 set X = {F(j) where j is Element of N: P[j]};
     X is Subset of R from SubsetFD;
   then reconsider D = X as Subset of R;
   reconsider D as non empty directed Subset of R by Th11;
      sup inf_net N = Sup the mapping of (inf_net N) by WAYBEL_2:def 1
              .= sup rng the mapping of (inf_net N) by YELLOW_2:def 5
              .= sup D by Th28
              .= lim_inf N by WAYBEL11:def 6;
 hence thesis;
end;

theorem
  for R being up-complete /\-complete LATTICE,
    N being net of R,
    i being Element of N holds
sup inf_net N = lim_inf (N|i)
proof
let R be up-complete /\-complete LATTICE,
    N be net of R,
    i be Element of N;
   sup inf_net N = lim_inf N by Th29;
 hence thesis by Th27;
end;

theorem Th31:
for R being /\-complete Semilattice,
    N being net of R,
    V being upper Subset of R holds
inf_net N is_eventually_in V implies N is_eventually_in V
proof
 let R be /\-complete Semilattice, N be net of R,
     V be upper Subset of R;
  consider f being map of N,R such that
A1:  inf_net N = N*'f &
     for i being Element of N holds
      f.i = "/\"
({N.k where k is Element of N: k >= i},R) by Def4;
A2: the RelStr of inf_net N = the RelStr of N by A1,Def3;
 assume inf_net N is_eventually_in V;
 then consider i being Element of inf_net N such that
A3: for j being Element of inf_net N st i <= j holds (inf_net N).j in V
      by WAYBEL_0:def 11;
 consider j0 being Element of inf_net N such that
A4: i <= j0 & i <= j0 by YELLOW_6:def 5;
A5: (inf_net N).j0 in V by A3,A4;
 reconsider j' = j0 as Element of N by A2;
 take j';
  let j be Element of N such that A6: j' <= j;
  defpred P[Element of N] means $1 >= j';
  deffunc F(Element of N) = N.$1;
   set E = {F(k) where k is Element of N: P[k]};
      E is Subset of R from SubsetFD;
    then reconsider E as Subset of R;
       the mapping of (inf_net N) = f by A1,Def3;
then A7: (inf_net N).j0 = f.j' by WAYBEL_0:def 8
                 .= "/\"(E,R) by A1;
       N.j in E by A6;
    then "/\"(E,R) <= N.j by Th12;
   hence N.j in V by A5,A7,WAYBEL_0:def 20;
end;

theorem
  for R being /\-complete Semilattice,
    N being net of R,
    V being lower Subset of R holds
 N is_eventually_in V implies inf_net N is_eventually_in V
proof
let R be /\-complete Semilattice, N be net of R,
    V be lower Subset of R;
  consider f being map of N,R such that
A1:  inf_net N = N*'f &
     for i being Element of N holds
      f.i = "/\"
({N.k where k is Element of N: k >= i},R) by Def4;
A2: the RelStr of inf_net N = the RelStr of N by A1,Def3;
 assume N is_eventually_in V;
 then consider i being Element of N such that
A3: for j being Element of N st i <= j holds N.j in V by WAYBEL_0:def 11;
 reconsider i' = i as Element of inf_net N by A2;
 take i';
   let j be Element of inf_net N such that A4: i' <= j;
    reconsider j0 = j as Element of N by A2;
    defpred P[Element of N] means $1 >= j0;
    deffunc F(Element of N) = N.$1;
     set E = {F(k) where k is Element of N: P[k]};
    consider j1 being Element of N such that
A5:  j1 >= j0 & j1 >= j0 by YELLOW_6:def 5;
       E is Subset of R from SubsetFD;
     then reconsider E as Subset of R;
        i <= j0 & j0 <= j1 by A2,A4,A5,YELLOW_0:1;
      then i <= j1 by YELLOW_0:def 2;
then A6:   N.j1 in V by A3;
        N.j1 in E by A5;
then A7:   "/\"(E,R) <= N.j1 by Th12;
       the mapping of (inf_net N) = f by A1,Def3;
      then (inf_net N).j = f.j0 by WAYBEL_0:def 8
                   .= "/\"(E,R) by A1;
 hence (inf_net N).j in V by A6,A7,WAYBEL_0:def 19;
end;

theorem Th33:
for R being order_consistent up-complete /\-complete (non empty TopLattice)
for N being net of R,
    x being Element of R holds
    x <= lim_inf N implies x is_a_cluster_point_of N
proof
 let R be order_consistent up-complete /\-complete (non empty TopLattice),
    N be net of R,
    x be Element of R;
 assume A1:    x <= lim_inf N;
  defpred P[Element of N] means not contradiction;
  deffunc F(Element of N) =
    "/\"({N.i where i is Element of N:i >= $1}, R);
  set X = {F(j) where j is Element of N: P[j]};
    X is Subset of R from SubsetFD;
  then reconsider D = X as Subset of R;
   reconsider D as non empty directed Subset of R by Th11;
A2:  sup D = lim_inf N by WAYBEL11:def 6;
A3:  x <= sup D by A1,WAYBEL11:def 6;
A4:  sup D = sup inf_net N by A2,Th29;
  let V be a_neighborhood of x;
A5: for a being Element of R holds downarrow a = Cl {a} by Def2;
A6:  Int V is open by TOPS_1:51;
then A7:   Int V is upper by A5,Th25;
        x in Int V by CONNSP_2:def 1;
      then sup D in Int V by A3,A7,WAYBEL_0:def 20;
     then reconsider W = Int V as a_neighborhood of (sup D) by A6,CONNSP_2:5;
A8:   Int V c= V by TOPS_1:44;
       inf_net N is_eventually_in W by A4,Def2;
    then N is_eventually_in W by A7,Th31;
   then N is_eventually_in V by A8,WAYBEL_0:8;
  hence N is_often_in V by YELLOW_6:28;
end;

theorem
  for R being order_consistent up-complete /\-complete (non empty TopLattice)
for N being eventually-directed net of R,
    x being Element of R holds
    x <= lim_inf N iff x is_a_cluster_point_of N
 proof
  let R be order_consistent up-complete /\-complete (non empty TopLattice),
      N be eventually-directed net of R,
      x be Element of R;
  thus x <= lim_inf N implies x is_a_cluster_point_of N by Th33;
  thus x is_a_cluster_point_of N implies x <= lim_inf N
   proof
    assume
A1:  x is_a_cluster_point_of N;
  defpred P[Element of N] means not contradiction;
  deffunc F(Element of N) =
    "/\"({N.i where i is Element of N:i >= $1}, R);
set X = {F(j) where j is Element of N: P[j]};
     X is Subset of R from SubsetFD;
   then reconsider D = X as Subset of R;
   reconsider D as non empty directed Subset of R by Th11;
A2: lim_inf N = sup D by WAYBEL11:def 6;
      for G being Subset of R st G is open holds
    x in G implies {sup D} meets G
     proof
      let G be Subset of R such that A3: G is open;
      assume x in G;
      then reconsider G as a_neighborhood of x by A3,CONNSP_2:5;
A4:   N is_often_in G by A1,WAYBEL_9:def 9;
         now let i be Element of N;
        consider j1 being Element of N such that A5: i <= j1 & N.j1 in G by A4,
WAYBEL_0:def 12;
        consider j2 being Element of N such that
A6:      for k being Element of N st j2 <= k holds N.j1 <= N.k by WAYBEL_0:11;
        defpred P[Element of N] means $1 >= j2;
        deffunc F(Element of N) = N.$1;
         set E = {F(k) where k is Element of N: P[k]};
A7:      E is Subset of R from SubsetFD;
        consider j' being Element of N such that
A8:      j' >= j2 & j' >= j2 by YELLOW_6:def 5;
           N.j' in E by A8;
        then reconsider E' = E as non empty Subset of R by A7;
A9:     ex_inf_of E',R by WAYBEL_0:76;
       N.j1 is_<=_than E'
      proof
       let b be Element of R such that A10: b in E';
       consider k being Element of N such that
A11:     b = N.k and
A12:     k >= j2 by A10;
       reconsider k' = k as Element of N;
          N.j1 <= N.k' by A6,A12;
       hence N.j1 <= b by A11;
      end;
then A13:    N.j1 <= "/\"(E',R) by A9,YELLOW_0:31;
         for a being Element of R holds downarrow a = Cl {a} by Def2;
then A14:     G is upper by A3,Th25;
then A15:     "/\"(E',R) in G by A5,A13,WAYBEL_0:def 20;
           "/\"(E',R) in D;
        then "/\"(E',R) <= sup D by Th21;
       hence sup D in G by A14,A15,WAYBEL_0:def 20;
      end;
      then sup D in G & sup D in {sup D} by TARSKI:def 1;
      hence thesis by XBOOLE_0:3;
     end;
    then x in Cl {sup D} by PRE_TOPC:54;
     then x in downarrow sup D by Def2;
    hence x <= lim_inf N by A2,WAYBEL_0:17;
   end;
 end;


Back to top