The abstract of the Mizar article:

Directed Sets, Nets, Ideals, Filters, and Maps

by

Grzegorz Bancerek

Received September 12, 1996

MML identifier: WAYBEL_0

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, QUANTAL1, RELAT_2, FINSET_1, LATTICE3, BOOLE, SUBSET_1,
      LATTICES, YELLOW_0, CAT_1, PRE_TOPC, FUNCT_1, RELAT_1, SEQM_3, FUNCOP_1,
      TARSKI, SETFAM_1, ORDINAL2, FILTER_2, FILTER_0, BHSP_3, REALSET1,
      WAYBEL_0;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1,
      FINSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, REALSET1, PRE_TOPC,
      LATTICE3, YELLOW_0, ORDERS_1, ORDERS_3;
 constructors LATTICE3, YELLOW_0, ORDERS_3, MEMBERED, PRE_TOPC;
 clusters STRUCT_0, FINSET_1, RELSET_1, ORDERS_1, LATTICE3, YELLOW_0, FUNCOP_1,
      SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Directed subsets

definition
 let L be RelStr;
 let X be Subset of L;
 attr X is directed means
:: WAYBEL_0:def 1     :: Definition 1.1
  for x,y being Element of L st x in X & y in X
   ex z being Element of L st z in X & x <= z & y <= z;
 attr X is filtered means
:: WAYBEL_0:def 2     :: Definition 1.1
  for x,y being Element of L st x in X & y in X
   ex z being Element of L st z in X & z <= x & z <= y;
end;

:: Original "directed subset" is equivalent to "non empty directed subset"
:: in our terminology.  It is shown bellow.

theorem :: WAYBEL_0:1
 for L being non empty transitive RelStr, X being Subset of L holds
  X is non empty directed iff
  for Y being finite Subset of X
   ex x being Element of L st x in X & x is_>=_than Y;

:: Original "filtered subset" is equivalent to "non empty filtered subset"
:: in our terminology.  It is shown bellow.

theorem :: WAYBEL_0:2
 for L being non empty transitive RelStr, X being Subset of L holds
  X is non empty filtered iff
  for Y being finite Subset of X
   ex x being Element of L st x in X & x is_<=_than Y;

definition
 let L be RelStr;
 cluster {}L -> directed filtered;
end;

definition
 let L be RelStr;
 cluster directed filtered Subset of L;
end;

theorem :: WAYBEL_0:3
 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
 for X1 being Subset of L1, X2 being Subset of L2
  st X1 = X2 & X1 is directed
  holds X2 is directed;

theorem :: WAYBEL_0:4
   for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
 for X1 being Subset of L1, X2 being Subset of L2
  st X1 = X2 & X1 is filtered
  holds X2 is filtered;

theorem :: WAYBEL_0:5
 for L being non empty reflexive RelStr, x being Element of L
  holds {x} is directed filtered;

definition
 let L be non empty reflexive RelStr;
 cluster directed filtered non empty finite Subset of L;
end;

definition
 let L be with_suprema RelStr;
 cluster [#]L -> directed;
end;

definition
 let L be upper-bounded non empty RelStr;
 cluster [#]L -> directed;
end;

definition
 let L be with_infima RelStr;
 cluster [#]L -> filtered;
end;

definition
 let L be lower-bounded non empty RelStr;
 cluster [#]L -> filtered;
end;

definition
 let L be non empty RelStr;
 let S be SubRelStr of L;
 attr S is filtered-infs-inheriting means
:: WAYBEL_0:def 3
  for X being filtered Subset of S st X <> {} & ex_inf_of X,L
   holds "/\"(X,L) in the carrier of S;
 attr S is directed-sups-inheriting means
:: WAYBEL_0:def 4
  for X being directed Subset of S st X <> {} & ex_sup_of X,L
   holds "\/"(X,L) in the carrier of S;
end;

definition
 let L be non empty RelStr;
 cluster infs-inheriting -> filtered-infs-inheriting SubRelStr of L;
 cluster sups-inheriting -> directed-sups-inheriting SubRelStr of L;
end;

definition
 let L be non empty RelStr;
 cluster infs-inheriting sups-inheriting non empty full strict SubRelStr of L;
end;

theorem :: WAYBEL_0:6
   for L being non empty transitive RelStr
 for S being filtered-infs-inheriting non empty full SubRelStr of L
 for X being filtered Subset of S st X <> {} & ex_inf_of X,L
  holds ex_inf_of X,S & "/\"(X,S) = "/\"(X,L);

theorem :: WAYBEL_0:7
   for L being non empty transitive RelStr
 for S being directed-sups-inheriting non empty full SubRelStr of L
 for X being directed Subset of S st X <> {} & ex_sup_of X,L
  holds ex_sup_of X,S & "\/"(X,S) = "\/"(X,L);

begin :: Nets

definition
 let L1,L2 be non empty 1-sorted;
 let f be map of L1,L2;
 let x be Element of L1;
 redefine func f.x -> Element of L2;
end;

definition
 let L1,L2 be RelStr;
 let f be map of L1,L2;
 attr f is antitone means
:: WAYBEL_0:def 5
    for x,y being Element of L1 st x <= y
   for a,b being Element of L2 st a = f.x & b = f.y holds a >= b;
end;

:: Definition 1.2

definition let L be 1-sorted;
 struct (RelStr) NetStr over L (#
   carrier -> set,
   InternalRel -> (Relation of the carrier),
   mapping -> Function of the carrier, the carrier of L
 #);
end;

definition let L be 1-sorted;
 let X be non empty set;
 let O be Relation of X;
 let F be Function of X, the carrier of L;
 cluster NetStr(#X,O,F#) -> non empty;
end;

definition
 let N be RelStr;
 attr N is directed means
:: WAYBEL_0:def 6
  [#]N is directed;
end;

definition let L be 1-sorted;
 cluster non empty reflexive transitive antisymmetric directed
         (strict NetStr over L);
end;

definition let L be 1-sorted;
 mode prenet of L is directed non empty NetStr over L;
end;

definition let L be 1-sorted;
 mode net of L is transitive prenet of L;
end;

definition
 let L be non empty 1-sorted;
 let N be non empty NetStr over L;
 func netmap(N,L) -> map of N,L equals
:: WAYBEL_0:def 7
   the mapping of N;
 let i be Element of N;
 func N.i -> Element of L equals
:: WAYBEL_0:def 8
   (the mapping of N).i;
end;

definition
 let L be non empty RelStr;
 let N be non empty NetStr over L;
 attr N is monotone means
:: WAYBEL_0:def 9
    netmap(N,L) is monotone;
 attr N is antitone means
:: WAYBEL_0:def 10
    netmap(N,L) is antitone;
end;

definition let L be non empty 1-sorted;
 let N be non empty NetStr over L;
 let X be set;
 pred N is_eventually_in X means
:: WAYBEL_0:def 11
  ex i being Element of N st
   for j being Element of N st i <= j holds N.j in X;
 pred N is_often_in X means
:: WAYBEL_0:def 12
    for i being Element of N
   ex j being Element of N st i <= j & N.j in X;
end;

theorem :: WAYBEL_0:8
   for L being non empty 1-sorted, N being non empty NetStr over L
 for X,Y being set st X c= Y holds
   (N is_eventually_in X implies N is_eventually_in Y) &
   (N is_often_in X implies N is_often_in Y);

theorem :: WAYBEL_0:9
   for L being non empty 1-sorted, N being non empty NetStr over L
 for X being set holds
  N is_eventually_in X iff not N is_often_in (the carrier of L) \ X;

theorem :: WAYBEL_0:10
   for L being non empty 1-sorted, N being non empty NetStr over L
 for X being set holds
  N is_often_in X iff not N is_eventually_in (the carrier of L) \ X;

definition
 let L be non empty RelStr;
 let N be non empty NetStr over L;
 attr N is eventually-directed means
:: WAYBEL_0:def 13
  for i being Element of N holds N is_eventually_in
   {N.j where j is Element of N: N.i <= N.j};
 attr N is eventually-filtered means
:: WAYBEL_0:def 14
  for i being Element of N holds N is_eventually_in
   {N.j where j is Element of N: N.i >= N.j};
end;

theorem :: WAYBEL_0:11
 for L being non empty RelStr, N being non empty NetStr over L holds
   N is eventually-directed
  iff
   for i being Element of N ex j being Element of N st
   for k being Element of N st j <= k holds N.i <= N.k;

theorem :: WAYBEL_0:12
 for L being non empty RelStr, N being non empty NetStr over L holds
   N is eventually-filtered
  iff
   for i being Element of N ex j being Element of N st
   for k being Element of N st j <= k holds N.i >= N.k;

definition
 let L be non empty RelStr;
 cluster monotone -> eventually-directed prenet of L;
 cluster antitone -> eventually-filtered prenet of L;
end;

definition
 let L be non empty reflexive RelStr;
 cluster monotone antitone strict prenet of L;
end;

begin :: Closure by lower elements and finite sups

:: Definition 1.3

definition
 let L be RelStr;
 let X be Subset of L;
 func downarrow X -> Subset of L means
:: WAYBEL_0:def 15
  for x being Element of L holds x in it iff
   ex y being Element of L st y >= x & y in X;
 func uparrow X -> Subset of L means
:: WAYBEL_0:def 16
  for x being Element of L holds x in it iff
   ex y being Element of L st y <= x & y in X;
end;

theorem :: WAYBEL_0:13
 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
 for X being Subset of L1
 for Y being Subset of L2
  st X = Y holds downarrow X = downarrow Y & uparrow X = uparrow Y;

theorem :: WAYBEL_0:14
 for L being non empty RelStr, X being Subset of L holds
  downarrow X =
  {x where x is Element of L: ex y being Element of L st x <= y & y in X};

theorem :: WAYBEL_0:15
 for L being non empty RelStr, X being Subset of L holds
  uparrow X =
  {x where x is Element of L: ex y being Element of L st x >= y & y in X};

definition
 let L be non empty reflexive RelStr;
 let X be non empty Subset of L;
 cluster downarrow X -> non empty;
 cluster uparrow X -> non empty;
end;

theorem :: WAYBEL_0:16
 for L being reflexive RelStr, X being Subset of L holds
  X c= downarrow X & X c= uparrow X;

definition
 let L be non empty RelStr;
 let x be Element of L;
 func downarrow x -> Subset of L equals
:: WAYBEL_0:def 17  :: Definition 1.3 (iii)
   downarrow {x};
 func uparrow x -> Subset of L equals
:: WAYBEL_0:def 18    :: Definition 1.3 (iv)
   uparrow {x};
end;

theorem :: WAYBEL_0:17
 for L being non empty RelStr, x,y being Element of L
  holds y in downarrow x iff y <= x;

theorem :: WAYBEL_0:18
 for L being non empty RelStr, x,y being Element of L
  holds y in uparrow x iff x <= y;

theorem :: WAYBEL_0:19
   for L being non empty reflexive antisymmetric RelStr
 for x,y being Element of L
  st downarrow x = downarrow y holds x = y;

theorem :: WAYBEL_0:20
   for L being non empty reflexive antisymmetric RelStr
 for x,y being Element of L
  st uparrow x = uparrow y holds x = y;

theorem :: WAYBEL_0:21
 for L being non empty transitive RelStr
 for x,y being Element of L st x <= y
  holds downarrow x c= downarrow y;

theorem :: WAYBEL_0:22
 for L being non empty transitive RelStr
 for x,y being Element of L st x <= y
  holds uparrow y c= uparrow x;

definition
 let L be non empty reflexive RelStr;
 let x be Element of L;
 cluster downarrow x -> non empty directed;
 cluster uparrow x -> non empty filtered;
end;

definition
 let L be RelStr;
 let X be Subset of L;
 attr X is lower means
:: WAYBEL_0:def 19                  :: Definition 1.3 (v)
  for x,y being Element of L st x in X & y <= x holds y in X;
 attr X is upper means
:: WAYBEL_0:def 20                  :: Definition 1.3 (vi)
  for x,y being Element of L st x in X & x <= y holds y in X;
end;

definition
 let L be RelStr;
 cluster lower upper Subset of L;
end;

theorem :: WAYBEL_0:23
 for L being RelStr, X being Subset of L holds
  X is lower iff downarrow X c= X;

theorem :: WAYBEL_0:24
 for L being RelStr, X being Subset of L holds
  X is upper iff uparrow X c= X;

theorem :: WAYBEL_0:25
   for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
 for X1 being Subset of L1, X2 being Subset of L2
  st X1 = X2 holds
   (X1 is lower implies X2 is lower) &
   (X1 is upper implies X2 is upper);

theorem :: WAYBEL_0:26
   for L being RelStr, A being Subset of bool the carrier of L st
   for X being Subset of L st X in A holds X is lower
 holds union A is lower Subset of L;

theorem :: WAYBEL_0:27
 for L being RelStr, X,Y being Subset of L st X is lower & Y is lower
  holds X /\ Y is lower & X \/ Y is lower;

theorem :: WAYBEL_0:28
   for L being RelStr, A being Subset of bool the carrier of L st
   for X being Subset of L st X in A holds X is upper
 holds union A is upper Subset of L;

theorem :: WAYBEL_0:29
 for L being RelStr, X,Y being Subset of L st X is upper & Y is upper
  holds X /\ Y is upper & X \/ Y is upper;

definition
 let L be non empty transitive RelStr;
 let X be Subset of L;
 cluster downarrow X -> lower;
 cluster uparrow X -> upper;
end;

definition
 let L be non empty transitive RelStr;
 let x be Element of L;
 cluster downarrow x -> lower;
 cluster uparrow x -> upper;
end;

definition
 let L be non empty RelStr;
 cluster [#]L -> lower upper;
end;

definition
 let L be non empty RelStr;
 cluster non empty lower upper Subset of L;
end;

definition
 let L be non empty reflexive transitive RelStr;
 cluster non empty lower directed Subset of L;
 cluster non empty upper filtered Subset of L;
end;

definition
 let L be with_infima with_suprema Poset;
 cluster non empty directed filtered lower upper Subset of L;
end;

theorem :: WAYBEL_0:30
 for L being non empty transitive reflexive RelStr, X be Subset of L holds
  X is directed iff downarrow X is directed;

definition
 let L be non empty transitive reflexive RelStr;
 let X be directed Subset of L;
 cluster downarrow X -> directed;
end;

theorem :: WAYBEL_0:31
 for L being non empty transitive reflexive RelStr, X be Subset of L
 for x be Element of L holds x is_>=_than X iff x is_>=_than downarrow X;

theorem :: WAYBEL_0:32
 for L being non empty transitive reflexive RelStr, X be Subset of L holds
  ex_sup_of X,L iff ex_sup_of downarrow X,L;

theorem :: WAYBEL_0:33
 for L being non empty transitive reflexive RelStr, X be Subset of L
  st ex_sup_of X,L
  holds sup X = sup downarrow X;

theorem :: WAYBEL_0:34
   for L being non empty Poset, x being Element of L holds
   ex_sup_of downarrow x, L & sup downarrow x = x;

theorem :: WAYBEL_0:35
 for L being non empty transitive reflexive RelStr, X be Subset of L holds
  X is filtered iff uparrow X is filtered;

definition
 let L be non empty transitive reflexive RelStr;
 let X be filtered Subset of L;
 cluster uparrow X -> filtered;
end;

theorem :: WAYBEL_0:36
 for L being non empty transitive reflexive RelStr, X be Subset of L
 for x be Element of L holds
  x is_<=_than X iff x is_<=_than uparrow X;

theorem :: WAYBEL_0:37
 for L being non empty transitive reflexive RelStr, X be Subset of L holds
  ex_inf_of X,L iff ex_inf_of uparrow X,L;

theorem :: WAYBEL_0:38
 for L being non empty transitive reflexive RelStr, X be Subset of L
  st ex_inf_of X,L
  holds inf X = inf uparrow X;

theorem :: WAYBEL_0:39
   for L being non empty Poset, x being Element of L holds
   ex_inf_of uparrow x, L & inf uparrow x = x;

begin :: Ideals and filters

definition
 let L be non empty reflexive transitive RelStr;
 mode Ideal of L is directed lower non empty Subset of L;
                                :: Definition 1.3 (vii)
 mode Filter of L is filtered upper non empty Subset of L;
                                :: Definition 1.3 (viii)
end;

theorem :: WAYBEL_0:40
 for L being with_suprema antisymmetric RelStr, X being lower Subset of L holds
  X is directed iff for x,y being Element of L st x in X & y in X holds x"\/"
y in
 X;

theorem :: WAYBEL_0:41
 for L being with_infima antisymmetric RelStr, X being upper Subset of L holds
  X is filtered iff for x,y being Element of L st x in X & y in X holds x"/\"
y in
 X;

theorem :: WAYBEL_0:42
 for L being with_suprema Poset
 for X being non empty lower Subset of L holds
  X is directed iff for Y being finite Subset of X st Y <> {} holds "\/"
(Y,L) in
 X;

theorem :: WAYBEL_0:43
 for L being with_infima Poset
 for X being non empty upper Subset of L holds
  X is filtered iff for Y being finite Subset of X st Y <> {} holds "/\"
(Y,L) in
 X;

theorem :: WAYBEL_0:44
   for L being non empty antisymmetric RelStr
  st L is with_suprema or L is with_infima
 for X,Y being Subset of L
  st X is lower directed & Y is lower directed
  holds X /\ Y is directed;

theorem :: WAYBEL_0:45
   for L being non empty antisymmetric RelStr
  st L is with_suprema or L is with_infima
 for X,Y being Subset of L
  st X is upper filtered & Y is upper filtered
  holds X /\ Y is filtered;

theorem :: WAYBEL_0:46
   for L being RelStr, A being Subset of bool the carrier of L st
   (for X being Subset of L st X in A holds X is directed) &
   (for X,Y being Subset of L st X in A & Y in A
     ex Z being Subset of L st Z in A & X \/ Y c= Z)
 for X being Subset of L st X = union A holds X is directed;

theorem :: WAYBEL_0:47
   for L being RelStr, A being Subset of bool the carrier of L st
   (for X being Subset of L st X in A holds X is filtered) &
   (for X,Y being Subset of L st X in A & Y in A
     ex Z being Subset of L st Z in A & X \/ Y c= Z)
 for X being Subset of L st X = union A holds X is filtered;

definition
 let L be non empty reflexive transitive RelStr;
 let I be Ideal of L;
 attr I is principal means
:: WAYBEL_0:def 21
    ex x being Element of L st x in I & x is_>=_than I;
end;

definition
 let L be non empty reflexive transitive RelStr;
 let F be Filter of L;
 attr F is principal means
:: WAYBEL_0:def 22
    ex x being Element of L st x in F & x is_<=_than F;
end;

theorem :: WAYBEL_0:48
   for L being non empty reflexive transitive RelStr, I being Ideal of L holds
  I is principal iff ex x being Element of L st I = downarrow x;

theorem :: WAYBEL_0:49
   for L being non empty reflexive transitive RelStr, F being Filter of L holds
  F is principal iff ex x being Element of L st F = uparrow x;

definition let L be non empty reflexive transitive RelStr;
 func Ids L -> set equals
:: WAYBEL_0:def 23                 :: Definition 1.3 (xi)
     {X where X is Ideal of L: not contradiction};
 func Filt L -> set equals
:: WAYBEL_0:def 24                :: Definition 1.3 (xi)
     {X where X is Filter of L: not contradiction};
end;

definition let L be non empty reflexive transitive RelStr;
 func Ids_0 L -> set equals
:: WAYBEL_0:def 25               :: Definition 1.3 (xii)
     Ids L \/ {{}};
 func Filt_0 L -> set equals
:: WAYBEL_0:def 26              :: Definition 1.3 (xiii)
     Filt L \/ {{}};
end;

definition
 let L be non empty RelStr;
 let X be Subset of L;
 func finsups X -> Subset of L equals
:: WAYBEL_0:def 27
   {"\/"(Y,L) where Y is finite Subset of X: ex_sup_of Y,L};
 func fininfs X -> Subset of L equals
:: WAYBEL_0:def 28
   {"/\"(Y,L) where Y is finite Subset of X: ex_inf_of Y,L};
end;

definition
 let L be non empty antisymmetric lower-bounded RelStr;
 let X be Subset of L;
 cluster finsups X -> non empty;
end;

definition
 let L be non empty antisymmetric upper-bounded RelStr;
 let X be Subset of L;
 cluster fininfs X -> non empty;
end;

definition
 let L be non empty reflexive antisymmetric RelStr;
 let X be non empty Subset of L;
 cluster finsups X -> non empty;
 cluster fininfs X -> non empty;
end;

theorem :: WAYBEL_0:50
 for L being non empty reflexive antisymmetric RelStr
 for X being Subset of L
  holds X c= finsups X & X c= fininfs X;

theorem :: WAYBEL_0:51
 for L being non empty transitive RelStr
 for X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F)
 holds F is directed;

definition
 let L be with_suprema Poset;
 let X be Subset of L;
 cluster finsups X -> directed;
end;

theorem :: WAYBEL_0:52
 for L being non empty transitive reflexive RelStr, X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F)
 for x being Element of L holds x is_>=_than X iff x is_>=_than F;

theorem :: WAYBEL_0:53
 for L being non empty transitive reflexive RelStr, X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F)
 holds ex_sup_of X,L iff ex_sup_of F,L;

theorem :: WAYBEL_0:54
 for L being non empty transitive reflexive RelStr, X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F) &
  ex_sup_of X,L
 holds sup F = sup X;

theorem :: WAYBEL_0:55
   for L being with_suprema Poset, X being Subset of L
  st ex_sup_of X,L or L is complete
  holds sup X = sup finsups X;

theorem :: WAYBEL_0:56
 for L being non empty transitive RelStr
 for X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F)
 holds F is filtered;

definition
 let L be with_infima Poset;
 let X be Subset of L;
 cluster fininfs X -> filtered;
end;

theorem :: WAYBEL_0:57
 for L being non empty transitive reflexive RelStr, X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F)
 for x being Element of L holds x is_<=_than X iff x is_<=_than F;

theorem :: WAYBEL_0:58
 for L being non empty transitive reflexive RelStr, X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F)
 holds ex_inf_of X,L iff ex_inf_of F,L;

theorem :: WAYBEL_0:59
 for L being non empty transitive reflexive RelStr, X,F being Subset of L st
  (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) &
  (for x being Element of L st x in F
    ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) &
  (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F) &
  ex_inf_of X, L
 holds inf F = inf X;

theorem :: WAYBEL_0:60
   for L being with_infima Poset, X being Subset of L
  st ex_inf_of X,L or L is complete
  holds inf X = inf fininfs X;

theorem :: WAYBEL_0:61
   for L being with_suprema Poset, X being Subset of L holds
   X c= downarrow finsups X &
   for I being Ideal of L st X c= I holds downarrow finsups X c= I;

theorem :: WAYBEL_0:62
   for L being with_infima Poset, X being Subset of L holds
   X c= uparrow fininfs X &
   for F being Filter of L st X c= F holds uparrow fininfs X c= F;

begin :: Chains

definition
 let L be non empty RelStr;
 attr L is connected means
:: WAYBEL_0:def 29
  for x,y being Element of L holds x <= y or y <= x;
end;

definition
 cluster trivial -> connected (non empty reflexive RelStr);
end;

definition
 cluster connected (non empty Poset);
end;

definition
 mode Chain is connected (non empty Poset);
end;

definition
 let L be Chain;
 cluster L~ -> connected;
end;

begin :: Semilattices

definition
 mode Semilattice is with_infima Poset;
 mode sup-Semilattice is with_suprema Poset;
 mode LATTICE is with_infima with_suprema Poset;
end;

theorem :: WAYBEL_0:63
   for L being Semilattice for X being upper non empty Subset of L holds
   X is Filter of L iff subrelstr X is meet-inheriting;

theorem :: WAYBEL_0:64
   for L being sup-Semilattice for X being lower non empty Subset of L holds
   X is Ideal of L iff subrelstr X is join-inheriting;

begin :: Maps

definition
 let S,T be non empty RelStr;
 let f be map of S,T;
 let X be Subset of S;
 pred f preserves_inf_of X means
:: WAYBEL_0:def 30
  ex_inf_of X,S implies ex_inf_of f.:X,T & inf (f.:X) = f.inf X;
 pred f preserves_sup_of X means
:: WAYBEL_0:def 31
  ex_sup_of X,S implies ex_sup_of f.:X,T & sup (f.:X) = f.sup X;
end;

theorem :: WAYBEL_0:65
   for S1,S2, T1,T2 being non empty RelStr st
  the RelStr of S1 = the RelStr of T1 & the RelStr of S2 = the RelStr of T2
 for f being map of S1,S2, g being map of T1,T2 st f = g
 for X being Subset of S1, Y being Subset of T1 st X = Y holds
   (f preserves_sup_of X implies g preserves_sup_of Y) &
   (f preserves_inf_of X implies g preserves_inf_of Y);

definition
 let L1,L2 be non empty RelStr;
 let f be map of L1,L2;
 attr f is infs-preserving means
:: WAYBEL_0:def 32
    for X being Subset of L1 holds f preserves_inf_of X;
 attr f is sups-preserving means
:: WAYBEL_0:def 33
    for X being Subset of L1 holds f preserves_sup_of X;
 attr f is meet-preserving means
:: WAYBEL_0:def 34
    for x,y being Element of L1 holds f preserves_inf_of {x,y};
 attr f is join-preserving means
:: WAYBEL_0:def 35
    for x,y being Element of L1 holds f preserves_sup_of {x,y};
 attr f is filtered-infs-preserving means
:: WAYBEL_0:def 36
    for X being Subset of L1 st X is non empty filtered
   holds f preserves_inf_of X;
 attr f is directed-sups-preserving means
:: WAYBEL_0:def 37
    for X being Subset of L1 st X is non empty directed
   holds f preserves_sup_of X;
end;

definition
 let L1,L2 be non empty RelStr;
 cluster infs-preserving ->
    filtered-infs-preserving meet-preserving map of L1,L2;
 cluster sups-preserving ->
    directed-sups-preserving join-preserving map of L1,L2;
end;

definition
 let S,T be RelStr;
 let f be map of S,T;
 attr f is isomorphic means
:: WAYBEL_0:def 38
  f is one-to-one monotone & ex g being map of T,S st g = f" & g is monotone
  if S is non empty & T is non empty
  otherwise S is empty & T is empty;
end;

theorem :: WAYBEL_0:66
 for S,T being non empty RelStr, f being map of S,T holds f is isomorphic iff
  f is one-to-one & rng f = the carrier of T &
   for x,y being Element of S holds x <= y iff f.x <= f.y;

definition
 let S,T be non empty RelStr;
 cluster isomorphic -> one-to-one monotone map of S,T;
end;

theorem :: WAYBEL_0:67
   for S,T being non empty RelStr, f being map of S,T st f is isomorphic
   holds f" is map of T,S & rng (f") = the carrier of S;

theorem :: WAYBEL_0:68
   for S,T being non empty RelStr, f being map of S,T st f is isomorphic
  for g being map of T,S st g = f" holds g is isomorphic;

theorem :: WAYBEL_0:69
 for S,T being non empty Poset, f being map of S,T st
   for X being Filter of S holds f preserves_inf_of X
 holds f is monotone;

theorem :: WAYBEL_0:70
   for S,T being non empty Poset, f being map of S,T st
   for X being Filter of S holds f preserves_inf_of X
 holds f is filtered-infs-preserving;

theorem :: WAYBEL_0:71
   for S being Semilattice, T being non empty Poset, f being map of S,T st
  (for X being finite Subset of S holds f preserves_inf_of X) &
  (for X being non empty filtered Subset of S holds f preserves_inf_of X)
 holds f is infs-preserving;

theorem :: WAYBEL_0:72
 for S,T being non empty Poset, f being map of S,T st
   for X being Ideal of S holds f preserves_sup_of X
 holds f is monotone;

theorem :: WAYBEL_0:73
   for S,T being non empty Poset, f being map of S,T st
   for X being Ideal of S holds f preserves_sup_of X
 holds f is directed-sups-preserving;

theorem :: WAYBEL_0:74
   for S being sup-Semilattice, T being non empty Poset, f being map of S,T st
  (for X being finite Subset of S holds f preserves_sup_of X) &
  (for X being non empty directed Subset of S holds f preserves_sup_of X)
 holds f is sups-preserving;

begin :: Complete Semilattice

definition
 let L be non empty reflexive RelStr;
 attr L is up-complete means
:: WAYBEL_0:def 39
  for X being non empty directed Subset of L
  ex x being Element of L st x is_>=_than X &
   for y being Element of L st y is_>=_than X holds x <= y;
end;

definition
 cluster up-complete -> upper-bounded (with_suprema reflexive RelStr);
end;

theorem :: WAYBEL_0:75
   for L being non empty reflexive antisymmetric RelStr holds
   L is up-complete
  iff
   for X being non empty directed Subset of L holds ex_sup_of X,L;

definition
 let L be non empty reflexive RelStr;
 attr L is /\-complete means
:: WAYBEL_0:def 40
  for X being non empty Subset of L
  ex x being Element of L st x is_<=_than X &
   for y being Element of L st y is_<=_than X holds x >= y;
end;

theorem :: WAYBEL_0:76
 for L being non empty reflexive antisymmetric RelStr holds
   L is /\-complete
  iff
   for X being non empty Subset of L holds ex_inf_of X,L;

definition
 cluster complete -> up-complete /\-complete (non empty reflexive RelStr);
 cluster /\-complete -> lower-bounded (non empty reflexive RelStr);
 cluster up-complete with_suprema lower-bounded -> complete (non empty Poset);
:: cluster up-complete /\-complete upper-bounded -> complete (non empty Poset);
::        to appear in YELLOW_2
end;

definition
 cluster /\-complete -> with_infima (non empty reflexive antisymmetric RelStr);
end;

definition
 cluster /\-complete -> with_suprema
  (non empty reflexive antisymmetric upper-bounded RelStr);
end;

definition
 cluster complete strict LATTICE;
end;