Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### 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;

Back to top