The abstract of the Mizar article:

On the Order-consistent Topology of Complete and Uncomplete Lattices

by

Ewa Gradzka

Received May 23, 2000

MML identifier: WAYBEL32

[ Mizar article, 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;


begin

definition
 let T be non empty TopRelStr;
 attr T is upper means
:: WAYBEL32:def 1

  {(downarrow x)` where x is Element of T: not contradiction} is prebasis of T;
end;

definition
 cluster Scott up-complete strict TopLattice;
end;

definition
 let T be TopSpace-like non empty reflexive TopRelStr;
 attr T is order_consistent means
:: WAYBEL32:def 2

  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);
end;

definition
 cluster upper trivial up-complete strict TopLattice;
  end;

theorem :: WAYBEL32:1
 for T being upper up-complete (non empty TopPoset)
 for A being Subset of T st A is open holds A is upper;

theorem :: WAYBEL32:2
   for T being up-complete (non empty TopPoset) holds
 T is upper implies T is order_consistent;

canceled 4;

theorem :: WAYBEL32:7
for R being up-complete (non empty reflexive transitive antisymmetric
     RelStr)
 ex T being TopAugmentation of R st T is Scott;

theorem :: WAYBEL32:8
 for R being up-complete (non empty Poset)
  for T being TopAugmentation of R holds T is Scott implies T is correct;

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

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

theorem :: WAYBEL32:9   :: 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;

theorem :: WAYBEL32:10
 for T being up-complete Scott (non empty TopPoset) holds
  T is order_consistent;

theorem :: WAYBEL32:11
 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;

theorem :: WAYBEL32:12
 for R being /\-complete Semilattice,
     S being Subset of R,
     a being Element of R holds
  a in S implies "/\"(S,R) <= a;

theorem :: WAYBEL32:13
 for R being /\-complete Semilattice,
     N being monotone reflexive net of R
 holds lim_inf N = sup N;

theorem :: WAYBEL32:14
 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;

theorem :: WAYBEL32:15
 for R being /\-complete up-complete Semilattice,
  T being TopAugmentation of R
  st the topology of T = sigma R
  holds T is Scott;

definition
 let R be /\-complete up-complete Semilattice;
 cluster strict Scott correct TopAugmentation of R;
end;

theorem :: WAYBEL32:16
  for S being up-complete /\-complete Semilattice,
    T being Scott TopAugmentation of S holds
  sigma S = the topology of T;

theorem :: WAYBEL32:17     :: Remark 1.4 (iii)
   for T being Scott up-complete (non empty reflexive transitive antisymmetric
     TopRelStr)
 holds T is T_0-TopSpace;

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

theorem :: WAYBEL32:18
 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;

theorem :: WAYBEL32:19     ::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;

theorem :: WAYBEL32:20    ::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);

theorem :: WAYBEL32:21
 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);

::Remark 1.4 (vi)
definition let T be up-complete (non empty reflexive transitive antisymmetric
     TopRelStr);
 cluster lower -> property(S) Subset of T;
end;

theorem :: WAYBEL32:22
   for T being finite up-complete (non empty Poset),
     S being Subset of T holds S is inaccessible;

theorem :: WAYBEL32:23
 for R being complete connected LATTICE,
  T being Scott TopAugmentation of R, x being Element of T holds
   (downarrow x)` is open;

theorem :: WAYBEL32:24
   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};

definition
let R be up-complete (non empty Poset);
cluster order_consistent (correct TopAugmentation of R);
end;

definition
cluster order_consistent complete TopLattice;
end;

theorem :: WAYBEL32:25
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);

theorem :: WAYBEL32:26
  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;

theorem :: WAYBEL32:27
 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;

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
:: WAYBEL32:def 3

the RelStr of it = the RelStr of R &
the mapping of it = f;
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;
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;
end;

definition
 let R be non empty RelStr,
     N be prenet of R;
func inf_net N -> strict prenet of R means
:: WAYBEL32:def 4

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);
end;

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

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

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

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

theorem :: WAYBEL32:28
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};

theorem :: WAYBEL32:29
for R being up-complete /\-complete LATTICE,
    N being net of R holds
sup inf_net N = lim_inf N;

theorem :: WAYBEL32:30
  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);

theorem :: WAYBEL32:31
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;

theorem :: WAYBEL32:32
  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;

theorem :: WAYBEL32:33
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;

theorem :: WAYBEL32:34
  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;