The abstract of the Mizar article:

Bounds in Posets and Relational Substructures

by

Grzegorz Bancerek

Received September 10, 1996

MML identifier: YELLOW_0

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, RELAT_1, RELAT_2, BHSP_3, LATTICE3, REALSET1, BOOLE,
      SUBSET_1, LATTICES, FILTER_0, FILTER_1, ORDINAL2, FINSET_1, WELLORD1,
      CAT_1, YELLOW_0;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_2, RELSET_1, FINSET_1,
      TOLER_1, STRUCT_0, LATTICES, REALSET1, PRE_TOPC, ORDERS_1, LATTICE3;
 constructors LATTICE3, PRE_TOPC, REALSET1, TOLER_1;
 clusters STRUCT_0, FINSET_1, RELSET_1, ORDERS_1, LATTICE3, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin :: Reexamination of poset concepts

scheme RelStrEx {X() -> non empty set, P[set,set]}:
 ex L being non empty strict RelStr st the carrier of L = X() &
  for a,b being Element of L holds a <= b iff P[a,b];

definition let A be non empty RelStr;
 redefine attr A is reflexive means
:: YELLOW_0:def 1
    for x being Element of A holds x <= x;
end;

definition let A be RelStr;
 redefine attr A is transitive means
:: YELLOW_0:def 2
    for x,y,z being Element of A st x <= y & y <= z holds x <= z;
 attr A is antisymmetric means
:: YELLOW_0:def 3
    for x,y being Element of A st x <= y & y <= x holds x = y;
end;

definition
 cluster complete -> with_suprema with_infima (non empty RelStr);
 cluster trivial -> complete transitive antisymmetric
         (non empty reflexive RelStr);
end;

definition
 let x be set;
 let R be Relation of {x};
 cluster RelStr(#{x},R#) -> trivial;
end;

definition
 cluster strict trivial non empty reflexive RelStr;
end;

theorem :: YELLOW_0:1
 for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2
 for a1,b1 being Element of P1 for a2,b2 being Element of P2
  st a1 = a2 & b1 = b2
  holds (a1 <= b1 implies a2 <= b2) & (a1 < b1 implies a2 < b2);

theorem :: YELLOW_0:2
 for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2
 for X being set
 for a1 being Element of P1 for a2 being Element of P2 st a1 = a2
  holds
   (X is_<=_than a1 implies X is_<=_than a2) &
   (X is_>=_than a1 implies X is_>=_than a2);

theorem :: YELLOW_0:3
   for P1,P2 being RelStr
  st the RelStr of P1 = the RelStr of P2 & P1 is complete
  holds P2 is complete;

theorem :: YELLOW_0:4
 for L being transitive RelStr, x,y being Element of L st x <= y
 for X being set holds
  (y is_<=_than X implies x is_<=_than X) &
  (x is_>=_than X implies y is_>=_than X);

theorem :: YELLOW_0:5
 for L being non empty RelStr, X being set, x being Element of L holds
   (x is_>=_than X iff x is_>=_than X /\ the carrier of L) &
   (x is_<=_than X iff x is_<=_than X /\ the carrier of L);

theorem :: YELLOW_0:6
 for L being RelStr, a being Element of L holds
  {} is_<=_than a & {} is_>=_than a;

theorem :: YELLOW_0:7
 for L being RelStr, a,b being Element of L holds
  (a is_<=_than {b} iff a <= b) &
  (a is_>=_than {b} iff b <= a);

theorem :: YELLOW_0:8
 for L being RelStr, a,b,c being Element of L holds
  (a is_<=_than {b,c} iff a <= b & a <= c) &
  (a is_>=_than {b,c} iff b <= a & c <= a);

theorem :: YELLOW_0:9
 for L being RelStr, X,Y being set st X c= Y
 for x being Element of L holds
  (x is_<=_than Y implies x is_<=_than X) &
  (x is_>=_than Y implies x is_>=_than X);

theorem :: YELLOW_0:10
 for L being RelStr, X,Y being set, x being Element of L holds
  (x is_<=_than X & x is_<=_than Y implies x is_<=_than X \/ Y) &
  (x is_>=_than X & x is_>=_than Y implies x is_>=_than X \/ Y);

theorem :: YELLOW_0:11
 for L being transitive RelStr
 for X being set, x,y being Element of L st X is_<=_than x & x <= y
  holds X is_<=_than y;

theorem :: YELLOW_0:12
 for L being transitive RelStr
 for X being set, x,y being Element of L st X is_>=_than x & x >= y
  holds X is_>=_than y;

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

begin :: Least upper and greatest lower bounds

definition
 let L be RelStr;
 attr L is lower-bounded means
:: YELLOW_0:def 4
  ex x being Element of L st x is_<=_than the carrier of L;
 attr L is upper-bounded means
:: YELLOW_0:def 5
  ex x being Element of L st x is_>=_than the carrier of L;
end;

definition
 let L be RelStr;
 attr L is bounded means
:: YELLOW_0:def 6
L is lower-bounded upper-bounded;
end;

theorem :: YELLOW_0:13
   for P1,P2 being RelStr st the RelStr of P1 = the RelStr of P2 holds
  (P1 is lower-bounded implies P2 is lower-bounded) &
  (P1 is upper-bounded implies P2 is upper-bounded);

definition
 cluster complete -> bounded (non empty RelStr);
 cluster bounded -> lower-bounded upper-bounded RelStr;
 cluster lower-bounded upper-bounded -> bounded RelStr;
end;

definition
 cluster complete (non empty Poset);
end;

definition
 let L be RelStr;
 let X be set;
 pred ex_sup_of X,L means
:: YELLOW_0:def 7
  ex a being Element of L st X is_<=_than a &
   (for b being Element of L st X is_<=_than b holds b >= a) &
   for c being Element of L st X is_<=_than c &
     for b being Element of L st X is_<=_than b holds b >= c
   holds c = a;
 pred ex_inf_of X,L means
:: YELLOW_0:def 8
  ex a being Element of L st X is_>=_than a &
   (for b being Element of L st X is_>=_than b holds b <= a) &
   for c being Element of L st X is_>=_than c &
     for b being Element of L st X is_>=_than b holds b <= c
   holds c = a;
end;

theorem :: YELLOW_0:14
 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
 for X being set holds
   (ex_sup_of X,L1 implies ex_sup_of X,L2) &
   (ex_inf_of X,L1 implies ex_inf_of X,L2);

theorem :: YELLOW_0:15
 for L being antisymmetric RelStr, X being set holds
  ex_sup_of X,L iff ex a being Element of L st X is_<=_than a &
   for b being Element of L st X is_<=_than b holds a <= b;

theorem :: YELLOW_0:16
 for L being antisymmetric RelStr, X being set holds
  ex_inf_of X,L iff ex a being Element of L st X is_>=_than a &
   for b being Element of L st X is_>=_than b holds a >= b;

theorem :: YELLOW_0:17
 for L being complete non empty antisymmetric RelStr, X being set
  holds ex_sup_of X,L & ex_inf_of X,L;

theorem :: YELLOW_0:18
 for L being antisymmetric RelStr
 for a,b,c being Element of L holds
  c = a"\/"b & ex_sup_of {a,b},L iff c >= a & c >= b &
   for d being Element of L st d >= a & d >= b holds c <= d;

theorem :: YELLOW_0:19
 for L being antisymmetric RelStr
 for a,b,c being Element of L holds
  c = a"/\"b & ex_inf_of {a,b},L iff c <= a & c <= b &
   for d being Element of L st d <= a & d <= b holds c >= d;

theorem :: YELLOW_0:20
 for L being antisymmetric RelStr holds L is with_suprema iff
  for a,b being Element of L holds ex_sup_of {a,b},L;

theorem :: YELLOW_0:21
 for L being antisymmetric RelStr holds L is with_infima iff
  for a,b being Element of L holds ex_inf_of {a,b},L;

theorem :: YELLOW_0:22
 for L being antisymmetric with_suprema RelStr
 for a,b,c being Element of L holds
  c = a"\/"b iff c >= a & c >= b &
   for d being Element of L st d >= a & d >= b holds c <= d;

theorem :: YELLOW_0:23
 for L being antisymmetric with_infima RelStr
 for a,b,c being Element of L holds
  c = a"/\"b iff c <= a & c <= b &
   for d being Element of L st d <= a & d <= b holds c >= d;

theorem :: YELLOW_0:24
   for L being antisymmetric reflexive with_suprema RelStr
 for a,b being Element of L holds a = a"\/"b iff a >= b;

theorem :: YELLOW_0:25
   for L being antisymmetric reflexive with_infima RelStr
 for a,b being Element of L holds a = a"/\"b iff a <= b;

definition
 let L be RelStr;
 let X be set;
 func "\/"(X,L) -> Element of L means
:: YELLOW_0:def 9  :: Definition 1.1
  X is_<=_than it &
   for a being Element of L st X is_<=_than a holds it <= a
  if ex_sup_of X,L;
 func "/\"(X,L) -> Element of L means
:: YELLOW_0:def 10   :: Definition 1.1
  X is_>=_than it &
   for a being Element of L st X is_>=_than a holds a <= it
  if ex_inf_of X,L;
end;

theorem :: YELLOW_0:26
   for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
 for X being set st ex_sup_of X,L1 holds "\/"(X,L1) = "\/"(X,L2);

theorem :: YELLOW_0:27
   for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2
 for X being set st ex_inf_of X,L1 holds "/\"(X,L1) = "/\"(X,L2);

theorem :: YELLOW_0:28
   for L being complete (non empty Poset), X being set holds
  "\/"(X,L) = "\/"(X, latt L) & "/\"(X,L) = "/\"(X, latt L);

theorem :: YELLOW_0:29
   for L being complete Lattice, X being set holds
  "\/"(X,L) = "\/"(X, LattPOSet L) & "/\"(X,L) = "/\"(X, LattPOSet L);

theorem :: YELLOW_0:30
 for L being antisymmetric RelStr
 for a being Element of L, X being set holds
  a = "\/"(X,L) & ex_sup_of X,L iff a is_>=_than X &
   for b being Element of L st b is_>=_than X holds a <= b;

theorem :: YELLOW_0:31
 for L being antisymmetric RelStr
 for a being Element of L, X being set holds
  a = "/\"(X,L) & ex_inf_of X,L iff a is_<=_than X &
   for b being Element of L st b is_<=_than X holds a >= b;

theorem :: YELLOW_0:32
   for L being complete antisymmetric non empty RelStr
 for a being Element of L, X being set holds
  a = "\/"(X,L) iff a is_>=_than X &
   for b being Element of L st b is_>=_than X holds a <= b;

theorem :: YELLOW_0:33
   for L being complete antisymmetric (non empty RelStr)
 for a being Element of L, X being set holds
  a = "/\"(X,L) iff a is_<=_than X &
   for b being Element of L st b is_<=_than X holds a >= b;

theorem :: YELLOW_0:34
 for L being RelStr, X,Y being set
  st X c= Y & ex_sup_of X,L & ex_sup_of Y,L
  holds "\/"(X,L) <= "\/"(Y,L);

theorem :: YELLOW_0:35
 for L being RelStr, X,Y being set
  st X c= Y & ex_inf_of X,L & ex_inf_of Y,L
  holds "/\"(X,L) >= "/\"(Y,L);

theorem :: YELLOW_0:36
   for L being antisymmetric transitive RelStr, X,Y being set
  st ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y, L
  holds "\/"(X \/ Y, L) = "\/"(X,L)"\/""\/"(Y,L);

theorem :: YELLOW_0:37
   for L being antisymmetric transitive RelStr, X,Y being set
  st ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y, L
  holds "/\"(X \/ Y, L) = "/\"(X,L) "/\" "/\"(Y,L);

definition
 let L be RelStr;
 let X be Subset of L;
 redefine func "\/"(X,L); synonym sup X; func "/\"(X,L); synonym inf X;
end;

theorem :: YELLOW_0:38
 for L being non empty reflexive antisymmetric RelStr
 for a being Element of L holds ex_sup_of {a},L & ex_inf_of {a},L;

theorem :: YELLOW_0:39
   for L being non empty reflexive antisymmetric RelStr
 for a being Element of L holds sup {a} = a & inf {a} = a;

theorem :: YELLOW_0:40
 for L being with_infima Poset, a,b being Element of L holds inf {a,b} = a"/\"b
;

theorem :: YELLOW_0:41
 for L being with_suprema Poset, a,b being Element of L holds sup {a,b} = a"\/"
b;

theorem :: YELLOW_0:42
 for L being lower-bounded antisymmetric non empty RelStr holds
  ex_sup_of {},L & ex_inf_of the carrier of L, L;

theorem :: YELLOW_0:43
 for L being upper-bounded antisymmetric non empty RelStr holds
  ex_inf_of {},L & ex_sup_of the carrier of L, L;

definition
 let L be RelStr;
 func Bottom L -> Element of L equals
:: YELLOW_0:def 11

   "\/"({},L);
 func Top L -> Element of L equals
:: YELLOW_0:def 12

   "/\"({},L);
end;

theorem :: YELLOW_0:44
   for L being lower-bounded antisymmetric non empty RelStr
 for x being Element of L holds Bottom L <= x;

theorem :: YELLOW_0:45
   for L being upper-bounded antisymmetric non empty RelStr
 for x being Element of L holds x <= Top L;

theorem :: YELLOW_0:46
 for L being non empty RelStr, X,Y being set st
  for x being Element of L holds x is_>=_than X iff x is_>=_than Y
 holds ex_sup_of X,L implies ex_sup_of Y,L;

theorem :: YELLOW_0:47
 for L being non empty RelStr, X,Y being set st
  ex_sup_of X,L &
  for x being Element of L holds x is_>=_than X iff x is_>=_than Y
 holds "\/"(X,L) = "\/"(Y,L);

theorem :: YELLOW_0:48
 for L being non empty RelStr, X,Y being set st
  for x being Element of L holds x is_<=_than X iff x is_<=_than Y
 holds ex_inf_of X,L implies ex_inf_of Y,L;

theorem :: YELLOW_0:49
 for L being non empty RelStr, X,Y being set st
  ex_inf_of X,L &
  for x being Element of L holds x is_<=_than X iff x is_<=_than Y
 holds "/\"(X,L) = "/\"(Y,L);

theorem :: YELLOW_0:50
 for L being non empty RelStr, X being set holds
   (ex_sup_of X,L iff ex_sup_of X /\ the carrier of L, L) &
   (ex_inf_of X,L iff ex_inf_of X /\ the carrier of L, L);

theorem :: YELLOW_0:51
   for L being non empty RelStr, X being set
  st ex_sup_of X,L or ex_sup_of X /\ the carrier of L, L
  holds "\/"(X,L) = "\/"(X /\ the carrier of L, L);

theorem :: YELLOW_0:52
   for L being non empty RelStr, X being set
  st ex_inf_of X,L or ex_inf_of X /\ the carrier of L, L
  holds "/\"(X,L) = "/\"(X /\ the carrier of L, L);

theorem :: YELLOW_0:53
   for L being non empty RelStr st
  for X being Subset of L holds ex_sup_of X,L
 holds L is complete;

theorem :: YELLOW_0:54
   for L being non empty Poset holds L is with_suprema iff
   for X being finite non empty Subset of L holds ex_sup_of X,L;

theorem :: YELLOW_0:55
   for L being non empty Poset holds L is with_infima iff
  for X being finite non empty Subset of L holds ex_inf_of X,L;

begin :: Relational substructures

theorem :: YELLOW_0:56
 for X being set, R being Relation of X holds R = R|_2 X;

definition
 let L be RelStr;
 mode SubRelStr of L -> RelStr means
:: YELLOW_0:def 13
  the carrier of it c= the carrier of L &
  the InternalRel of it c= the InternalRel of L;
end;

definition
 let L be RelStr;
 let S be SubRelStr of L;
 attr S is full means
:: YELLOW_0:def 14
  the InternalRel of S = (the InternalRel of L)|_2 the carrier of S;
end;

definition
 let L be RelStr;
 cluster strict full SubRelStr of L;
end;

definition
 let L be non empty RelStr;
 cluster non empty full strict SubRelStr of L;
end;

theorem :: YELLOW_0:57
 for L being RelStr, X being Subset of L holds
  RelStr(#X, (the InternalRel of L)|_2 X#) is full SubRelStr of L;

theorem :: YELLOW_0:58
 for L being RelStr, S1,S2 being full SubRelStr of L
  st the carrier of S1 = the carrier of S2
  holds the RelStr of S1 = the RelStr of S2;

definition let L be RelStr;
 let X be Subset of L;
 func subrelstr X -> full strict SubRelStr of L means
:: YELLOW_0:def 15
    the carrier of it = X;
end;

theorem :: YELLOW_0:59
 for L being non empty RelStr, S being non empty SubRelStr of L
 for x being Element of S holds x is Element of L;

theorem :: YELLOW_0:60
 for L being RelStr, S being SubRelStr of L
 for a,b being Element of L for x,y being Element of S
  st x = a & y = b & x <= y holds a <= b;

theorem :: YELLOW_0:61
 for L being RelStr, S being full SubRelStr of L
 for a,b being Element of L for x,y being Element of S
  st x = a & y = b & a <= b & x in the carrier of S & y in the carrier of S
  holds x <= y;

theorem :: YELLOW_0:62
 for L being non empty RelStr, S being non empty full SubRelStr of L
 for X being set, a being Element of L for x being Element of S st x = a
  holds (a is_<=_than X implies x is_<=_than X) &
        (a is_>=_than X implies x is_>=_than X);

theorem :: YELLOW_0:63
 for L being non empty RelStr, S being non empty SubRelStr of L
 for X being Subset of S
 for a being Element of L for x being Element of S st x = a
  holds (x is_<=_than X implies a is_<=_than X) &
        (x is_>=_than X implies a is_>=_than X);

definition
 let L be reflexive RelStr;
 cluster -> reflexive (full SubRelStr of L);
end;

definition
 let L be transitive RelStr;
 cluster -> transitive (full SubRelStr of L);
end;

definition
 let L be antisymmetric RelStr;
 cluster -> antisymmetric (full SubRelStr of L);
end;

definition
 let L be non empty RelStr;
 let S be SubRelStr of L;
 attr S is meet-inheriting means
:: YELLOW_0:def 16
  for x,y being Element of L st
    x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L
   holds inf {x,y} in the carrier of S;
 attr S is join-inheriting means
:: YELLOW_0:def 17
  for x,y being Element of L st
    x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L
   holds sup {x,y} in the carrier of S;
end;

definition
 let L be non empty RelStr;
 let S be SubRelStr of L;
 attr S is infs-inheriting means
:: YELLOW_0:def 18
    for X being Subset of S st ex_inf_of X,L holds "/\"(X,L) in the carrier of
S
;
 attr S is sups-inheriting means
:: YELLOW_0:def 19
    for X being Subset of S st ex_sup_of X,L holds "\/"(X,L) in the carrier of
S
;
end;

definition
 let L be non empty RelStr;
 cluster infs-inheriting -> meet-inheriting SubRelStr of L;
 cluster sups-inheriting -> join-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 :: YELLOW_0:64
 for L being non empty transitive RelStr
 for S being non empty full SubRelStr of L
 for X being Subset of S st ex_inf_of X,L & "/\"(X,L) in the carrier of S
  holds ex_inf_of X,S & "/\"(X,S) = "/\"(X,L);

theorem :: YELLOW_0:65
 for L being non empty transitive RelStr
 for S being non empty full SubRelStr of L
 for X being Subset of S st ex_sup_of X,L & "\/"(X,L) in the carrier of S
  holds ex_sup_of X,S & "\/"(X,S) = "\/"(X,L);

theorem :: YELLOW_0:66
  for L being non empty transitive RelStr
 for S being non empty full SubRelStr of L
 for x,y being Element of S st ex_inf_of {x,y},L &
    "/\"({x,y},L) in the carrier of S
  holds ex_inf_of {x,y},S & "/\"({x,y},S) = "/\"({x,y},L);

theorem :: YELLOW_0:67
  for L being non empty transitive RelStr
 for S being non empty full SubRelStr of L
 for x,y being Element of S st ex_sup_of {x,y},L &
     "\/"({x,y},L) in the carrier of S
  holds ex_sup_of {x,y},S & "\/"({x,y},S) = "\/"({x,y},L);

definition
 let L be with_infima antisymmetric transitive RelStr;
 cluster -> with_infima (non empty meet-inheriting full SubRelStr of L);
end;

definition
 let L be with_suprema antisymmetric transitive RelStr;
 cluster -> with_suprema (non empty join-inheriting full SubRelStr of L);
end;

theorem :: YELLOW_0:68
   for L being complete (non empty Poset)
 for S being non empty full SubRelStr of L
 for X being Subset of S st "/\"(X,L) in the carrier of S
  holds "/\"(X,S) = "/\"(X,L);

theorem :: YELLOW_0:69
   for L being complete (non empty Poset)
 for S being non empty full SubRelStr of L
 for X being Subset of S st "\/"(X,L) in the carrier of S
  holds "\/"(X,S) = "\/"(X,L);

theorem :: YELLOW_0:70
   for L being with_infima Poset
 for S being meet-inheriting non empty full SubRelStr of L
 for x,y being Element of S, a,b be Element of L
  st a = x & b = y holds x"/\"y = a"/\"b;

theorem :: YELLOW_0:71
   for L being with_suprema Poset
 for S being join-inheriting non empty full SubRelStr of L
 for x,y being Element of S, a,b be Element of L
  st a = x & b = y holds x"\/"y = a"\/"b;