diff --git a/changes-set.txt b/changes-set.txt index f92b8cba63..8067b2cb11 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -95,6 +95,7 @@ make a github issue.) DONE: Date Old New Notes +17-Oct-24 posglbd posglbdg compare to poslubdg 15-Oct-24 --- --- well-founded induction theorems moved from SF's mathbox to main set.mm 12-Oct-24 syl5rbb bitr2id compare to bitr2i or bitr2d diff --git a/set.mm b/set.mm index d0d1e108a4..ee88e13fe6 100644 --- a/set.mm +++ b/set.mm @@ -215273,7 +215273,71 @@ that F(A') is isomorphic to B'.". Therefore, the category of sets and $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# - Preordered sets and directed sets using extensible structures + Dual of an order structure +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# +$) + + $c ODual $. + + $( Class function defining dual orders. $) + codu $a class ODual $. + + $( Define the dual of an ordered structure, which replaces the order + component of the structure with its reverse. See ~ odubas , ~ oduleval , + and ~ oduleg for its principal properties. + + _EDITORIAL_: likely usable to simplify many lattice proofs, as it allows + for duality arguments to be formalized; for instance ~ latmass . + (Contributed by Stefan O'Rear, 29-Jan-2015.) $) + df-odu $a |- ODual = ( w e. _V |-> + ( w sSet <. ( le ` ndx ) , `' ( le ` w ) >. ) ) $. + + ${ + $d D a $. $d .<_ a $. $d O a $. $d G a $. $d A a $. $d B a $. + oduval.d $e |- D = ( ODual ` O ) $. + + ${ + oduval.l $e |- .<_ = ( le ` O ) $. + $( Value of an order dual structure. (Contributed by Stefan O'Rear, + 29-Jan-2015.) $) + oduval $p |- D = ( O sSet <. ( le ` ndx ) , `' .<_ >. ) $= + ( va codu cfv cnx cple ccnv cop csts co cvv wcel wceq cv id fveq2 fvmpt + cnveqd opeq2d oveq12d df-odu ovex wn c0 reldmsets ovprc1 eqtr4d pm2.61i + fvprc cnveqi opeq2i oveq2i 3eqtr4i ) CGHZCIJHZCJHZKZLZMNZACUSBKZLZMNCOP + ZURVCQFCFRZUSVGJHZKZLZMNVCOGVGCQZVGCVJVBMVKSVKVIVAUSVKVHUTVGCJTUBUCUDFU + ECVBMUFUAVFUGURUHVCCGUMCVBMUIUJUKULDVEVBCMVDVAUSBUTEUNUOUPUQ $. + + $( Value of the less-equal relation in an order dual structure. + (Contributed by Stefan O'Rear, 29-Jan-2015.) $) + oduleval $p |- `' .<_ = ( le ` D ) $= + ( cple cfv ccnv cnx cop csts co cvv wcel wceq fvex cnvex pleid setsid + c0 mpan2 str0 fvprc cnveqd cnv0 eqtrdi reldmsets ovprc1 3eqtr4a pm2.61i + wn fveq2d cnveqi eqid oduval fveq2i 3eqtr4i ) CFGZHZCIFGZUSJZKLZFGZBHAF + GCMNZUSVCOZVDUSMNVEURCFPQMUSFMCRSUAVDUKZTTFGUSVCFUTRUBVFUSTHTVFURTCFUCU + DUEUFVFVBTFCVAKUGUHULUIUJBUREUMAVBFAURCDURUNUOUPUQ $. + + oduleg.g $e |- G = ( le ` D ) $. + $( Truth of the less-equal relation in an order dual structure. + (Contributed by Stefan O'Rear, 29-Jan-2015.) $) + oduleg $p |- ( ( A e. V /\ B e. W ) -> ( A G B <-> B .<_ A ) ) $= + ( wbr ccnv wcel wa cple cfv oduleval eqtr4i breqi brcnvg syl5bb ) ABDLA + BEMZLAGNBHNOBAELABDUCDCPQUCKCEFIJRSTABGHEUAUB $. + $} + + odubas.b $e |- B = ( Base ` O ) $. + $( Base set of an order dual structure. (Contributed by Stefan O'Rear, + 29-Jan-2015.) $) + odubas $p |- B = ( Base ` D ) $= + ( cbs cfv cnx cple ccnv cop csts co baseid wne c1 cc0 cdc 1re 1lt10 mpbir + ltneii basendx plendx neeq12i setsnid eqid oduval fveq2i 3eqtr4i ) CFGCHI + GZCIGZJZKLMZFGABFGUMUKFCNHFGZUKOPPQRZOPUPSTUBUOPUKUPUCUDUEUAUFEBUNFBULCDU + LUGUHUIUJ $. + $} + + +$( +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Preordered sets and directed sets #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# $) @@ -215466,17 +215530,10 @@ that F(A') is isomorphic to B'.". Therefore, the category of sets and $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# - Posets and lattices using extensible structures + Partially ordered sets (posets) #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# $) - -$( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - Posets -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -$) - $c Poset $. $c lt $. $c lub $. @@ -215694,6 +215751,66 @@ an empty base set ( ~ str0 ) and any relation partially orders an empty DENOTGDFQEUDUEUHZRIUFUGUIUJUKFRSFEQOTHDFQEUPRIUFUGUIULUKJKLUM $. $} + ${ + $d B x y a b c $. $d ph x y a b c $. $d K x y a b c $. $d L x y a b c $. + pospropd.kv $e |- ( ph -> K e. V ) $. + pospropd.lv $e |- ( ph -> L e. W ) $. + pospropd.kb $e |- ( ph -> B = ( Base ` K ) ) $. + pospropd.lb $e |- ( ph -> B = ( Base ` L ) ) $. + pospropd.xy $e |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> + ( x ( le ` K ) y <-> x ( le ` L ) y ) ) $. + $( Posethood is determined only by structure components and only by the + value of the relation within the base set. (Contributed by Stefan + O'Rear, 29-Jan-2015.) $) + pospropd $p |- ( ph -> ( K e. Poset <-> L e. Poset ) ) $= + ( va vb vc wbr wa wral wb cvv wcel cv cple cfv weq w3a cbs cpo ralrimivva + simp1 jca breq1 bibi12d breq2 rspc2va sylan 3adantl3 3simpb 3comr anbi12d + wi imbi1d 3adantl1 3anbi123d sylan2 ancoms 3exp2 imp42 ralbidva 2ralbidva + imbi12d wceq raleq raleqbi1dv 3bitr3d elexd biantrurd eqid ispos 3bitr4g + syl ) AEUAUBZNUCZWDEUDUEZQZWDOUCZWEQZWGWDWEQZRZNOUFZVBZWHWGPUCZWEQZRZWDWM + WEQZVBZUGZPEUHUEZSZOWSSZNWSSZRZFUAUBZWDWDFUDUEZQZWDWGXEQZWGWDXEQZRZWKVBZX + GWGWMXEQZRZWDWMXEQZVBZUGZPFUHUEZSZOXPSZNXPSZRZEUIUBFUIUBAXBXSXCXTAWRPDSZO + DSZNDSZXOPDSZODSZNDSZXBXSAYAYDNODDAWDDUBZWGDUBZRRWRXOPDAYGYHWMDUBZWRXOTZA + YGYHYIYJYGYHYIUGZAYJAYKBUCZCUCZWEQZYLYMXEQZTZCDSBDSZYJAYPBCDDMUJYKYQRZWFX + FWLXJWQXNYKYGYGRYQWFXFTZYKYGYGYGYHYIUKZYTULYPYSWDYMWEQZWDYMXEQZTZBCWDWDDD + BNUFYNUUAYOUUBYLWDYMWEUMYLWDYMXEUMUNZCNUFZUUAWFUUBXFYMWDWDWEUOYMWDWDXEUOU + NUPUQYRWJXIWKYRWHXGWIXHYGYHYQWHXGTZYIYPUUFUUCBCWDWGDDUUDCOUFUUAWHUUBXGYMW + GWDWEUOYMWGWDXEUOUNUPURZYKYHYGRZYQWIXHTZYHYIYGUUHYHYIYGUSUTYPUUIWGYMWEQZW + GYMXEQZTZBCWGWDDDBOUFYNUUJYOUUKYLWGYMWEUMYLWGYMXEUMUNZUUEUUJWIUUKXHYMWDWG + WEUOYMWDWGXEUOUNUPUQVAVCYRWOXLWPXMYRWHXGWNXKUUGYHYIYQWNXKTZYGYPUUNUULBCWG + WMDDUUMCPUFZUUJWNUUKXKYMWMWGWEUOYMWMWGXEUOUNUPVDVAYKYGYIRYQWPXMTZYGYHYIUS + YPUUPUUCBCWDWMDDUUDUUOUUAWPUUBXMYMWMWDWEUOYMWMWDXEUOUNUPUQVLVEVFVGVHVIVJV + KADWSVMYCXBTKYBXANDWSYAWTODWSWRPDWSVNVOVOWBADXPVMYFXSTLYEXRNDXPYDXQODXPXO + PDXPVNVOVOWBVPAWCXBAEGIVQVRAXDXSAFHJVQVRVPNOPWSEWEWSVSWEVSVTNOPXPFXEXPVSX + EVSVTWA $. + $} + + ${ + $d D a b c $. $d O a b c $. $d V a b c $. + odupos.d $e |- D = ( ODual ` O ) $. + $( Being a poset is a self-dual property. (Contributed by Stefan O'Rear, + 29-Jan-2015.) $) + odupos $p |- ( O e. Poset -> D e. Poset ) $= + ( va vb vc wcel cbs cfv cple cvv a1i wceq eqid cv wa wbr vex brcnv w3a wi + cpo ccnv fvexi odubas oduleval posref sylibr weq anbi12ci posasymb biimpd + codu syl5bi 3anrev postr sylan2b 3imtr4g isposd ) BUBGZDEFBHIZABJIZUCZKAK + GUTABUMCUDLVAAHIMUTVAABCVANZUELVCAJIMUTAVBBCVBNZUFLUTDOZVAGZPVFVFVBQVFVFV + CQVABVBVFVDVEUGVFVFVBDRZVHSUHVFEOZVCQZVIVFVCQZPVFVIVBQZVIVFVBQZPZUTVGVIVA + GZTZDEUIZVJVMVKVLVFVIVBVHERZSZVIVFVBVRVHSUJVPVNVQVABVBVFVIVDVEUKULUNUTVGV + OFOZVAGZTZPVTVIVBQZVMPZVTVFVBQZVJVIVTVCQZPVFVTVCQWBUTWAVOVGTWDWEUAVGVOWAU + OVABVBVTVIVFVDVEUPUQVJVMWFWCVSVIVTVBVRFRZSUJVFVTVBVHWGSURUS $. + + $( Being a poset is a self-dual property. (Contributed by Stefan O'Rear, + 29-Jan-2015.) $) + oduposb $p |- ( O e. V -> ( O e. Poset <-> D e. Poset ) ) $= + ( va vb wcel cpo odupos codu cfv eqid cbs odubas a1i cv cple wbr wa ccnv + fvexd id wceq eqidd wb oduleval eqcomi breqi brcnv 3bitri pospropd syl5ib + cvv vex impbid2 ) BCGZBHGZAHGZABDIURAJKZHGUPUQUSAUSLZIUPEFBMKZUSBUMCUPAJU + AUPUBVAUSMKUCUPVAUSAUTVAABDVALNNOUPVAUDEPZFPZUSQKZRZVBVCBQKZRZUEUPVBVAGVC + VAGSSVEVBVCVFTZTZRVCVBVHRVGVBVCVDVIVIVDUSVHAUTAVFBDVFLUFUFUGUHVBVCVHEUNZF + UNZUIVCVBVFVKVJUIUJOUKULUO $. + $} + $( Define less-than ordering for posets and related structures. Unlike ~ df-base and ~ df-ple , this is a derived component extractor and not an extensible structure component extractor that defines the poset. @@ -216721,6 +216838,210 @@ net proof size (existence part)? $) DEMCNZIEDMRIOABCHDEFGPQ $. $} + ${ + $d x y z w $. + $( Lemma for ~ odumeet . (Contributed by Stefan O'Rear, 29-Jan-2015.) $) + join0 $p |- ( join ` (/) ) = (/) $= + ( vx vy vz vw c0 cfv cv wbr cvv wceq 0ex eqid ax-mp cop wa wex wral eqtri + cab nex cjn cpr club coprab wcel joinfval df-oprab br0 cpw cple crio cmpt + wi wreu cres base0 biid lubfval reu0 abf reseq2i res0 breqi mtbir intnan + id ) EUAFZAGZBGZUBZCGZEUCFZHZABCUDZEEIUEZVGVNJKABCVLVGEIVLLZVGLUFMVNDGZVH + VINVKNJZVMOZCPZBPZAPZDSEVMABCDUGWBDWAAVTBVSCVMVRVMVJVKEHVJVKUHVJVKVLEVLDE + UIVHVKEUJFZHAVQQVHVIWCHAVQQVKVIWCHUMBEQOZCEUKULZWDCEUNZDSZUOZEVOVLWHJKVOW + DCABEVLEWCIDUPWCLVPWDUQVOVFURMWHWEEUOEWGEWEWFDWDCUSUTVAWEVBRRVCVDVETTTUTR + R $. + + $( Lemma for ~ odujoin . (Contributed by Stefan O'Rear, 29-Jan-2015.) + TODO ( ~ df-riota update): This proof increased from 152 bytes to 547 + bytes after the ~ df-riota change. Any way to shorten it? ~ join0 + also. $) + meet0 $p |- ( meet ` (/) ) = (/) $= + ( vx vy vz vw c0 cfv cv wbr cvv wceq 0ex eqid ax-mp cop wa wex wral eqtri + cab nex cmee cpr cglb coprab wcel meetfval df-oprab br0 cple wi crio cmpt + cpw wreu cres base0 biid glbfval reu0 abf reseq2i res0 breqi mtbir intnan + id ) EUAFZAGZBGZUBZCGZEUCFZHZABCUDZEEIUEZVGVNJKABCVLEVGIVLLZVGLUFMVNDGZVH + VINVKNJZVMOZCPZBPZAPZDSEVMABCDUGWBDWAAVTBVSCVMVRVMVJVKEHVJVKUHVJVKVLEVLAE + UMVIVKEUIFZHCVHQVQVKWCHCVHQVQVIWCHUJDEQOZBEUKULZWDBEUNZASZUOZEVOVLWHJKVOW + DBCDEVLEWCIAUPWCLVPWDUQVOVFURMWHWEEUOEWGEWEWFAWDBUSUTVAWEVBRRVCVDVETTTUTR + R $. + $} + + ${ + $d D a b c d $. $d L a b c d $. $d U a b c d $. $d O a b c d $. + $d V a b c d $. $d .\/ a b $. $d ./\ a b $. + oduglb.d $e |- D = ( ODual ` O ) $. + + ${ + odulub.l $e |- L = ( glb ` O ) $. + $( Least upper bounds in a dual order are greatest lower bounds in the + original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) $) + odulub $p |- ( O e. V -> L = ( lub ` D ) ) $= + ( va vb vc vd wcel cfv cv wbr wral wi vex brcnv ralbii eqid cglb cbs wa + club cpw cple crio cmpt wreu cab cres ccnv wb imbi12i anbi12i riotabiia + a1i mpteq2i reubii abbii reseq12i eqcomi biid id glbfval cvv wceq fvexi + codu odubas oduleval lubfval mp1i 3eqtr4a syl5eq ) CDKZBCUALZAUDLZFVPGC + UBLZUEZHMZIMZCUFLZNZIGMZOZJMZWBWCNZIWEOZWGWAWCNZPZJVSOZUCZHVSUGZUHZWMHV + SUIZGUJZUKZGVTWBWAWCULZNZIWEOZWBWGWSNZIWEOZWAWGWSNZPZJVSOZUCZHVSUGZUHZX + GHVSUIZGUJZUKZVQVRXLWRXIWOXKWQGVTXHWNXGWMHVSXGWMUMWAVSKXAWFXFWLWTWDIWEW + BWAWCIQZHQZRSXEWKJVSXCWIXDWJXBWHIWEWBWGWCXMJQZRSWAWGWCXNXORUNSUOZUQUPUR + XJWPGXGWMHVSXPUSUTVAVBVPWMHIJVSVQCWCDGVSTZWCTZVQTWMVCVPVDVEAVFKZVRXLVGV + PACVIEVHXSXGHIJVSVRAWSVFGVSACEXQVJAWCCEXRVKVRTXGVCXSVDVLVMVNVO $. + $} + + ${ + odujoin.m $e |- ./\ = ( meet ` O ) $. + $( Joins in a dual order are meets in the original. (Contributed by + Stefan O'Rear, 29-Jan-2015.) $) + odujoin $p |- ./\ = ( join ` D ) $= + ( va vb vc cmee cfv cjn cvv wcel wceq cv wbr coprab eqid codu c0 odulub + cglb club breqd oprabbidv meetfval fvexi joinfval mp1i 3eqtr4d wn fvprc + cpr syl5eq fveq2d join0 eqtrdi eqtr4d pm2.61i eqtri ) BCIJZAKJZECLMZVAV + BNVCFOGOUMZHOZCUBJZPZFGHQVDVEAUCJZPZFGHQZVAVBVCVGVIFGHVCVFVHVDVEAVFCLDV + FRZUAUDUEFGHVFCVALVKVARUFALMVBVJNVCACSDUGFGHVHVBALVHRVBRUHUIUJVCUKZVATV + BCIULVLVBTKJTVLATKVLACSJTDCSULUNUOUPUQURUSUT $. + $} + + ${ + oduglb.l $e |- U = ( lub ` O ) $. + $( Greatest lower bounds in a dual order are least upper bounds in the + original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) $) + oduglb $p |- ( O e. V -> U = ( glb ` D ) ) $= + ( va vc vb vd wcel cfv cv wbr wral wi vex brcnv ralbii eqid club cbs wa + cglb cpw cple crio cmpt wreu cab cres ccnv wb imbi12i anbi12i riotabiia + a1i mpteq2i reubii abbii reseq12i eqcomi biid id lubfval cvv wceq fvexi + codu odubas oduleval glbfval mp1i 3eqtr4a syl5eq ) CDKZBCUALZAUDLZFVPGC + UBLZUEZHMZIMZCUFLZNZHGMZOZWAJMZWCNZHWEOZWBWGWCNZPZJVSOZUCZIVSUGZUHZWMIV + SUIZGUJZUKZGVTWBWAWCULZNZHWEOZWGWAWSNZHWEOZWGWBWSNZPZJVSOZUCZIVSUGZUHZX + GIVSUIZGUJZUKZVQVRXLWRXIWOXKWQGVTXHWNXGWMIVSXGWMUMWBVSKXAWFXFWLWTWDHWEW + BWAWCIQZHQZRSXEWKJVSXCWIXDWJXBWHHWEWGWAWCJQZXNRSWGWBWCXOXMRUNSUOZUQUPUR + XJWPGXGWMIVSXPUSUTVAVBVPWMIHJVSVQCWCDGVSTZWCTZVQTWMVCVPVDVEAVFKZVRXLVGV + PACVIEVHXSXGIHJVSVRAWSVFGVSACEXQVJAWCCEXRVKVRTXGVCXSVDVLVMVNVO $. + $} + + ${ + odumeet.j $e |- .\/ = ( join ` O ) $. + $( Meets in a dual order are joins in the original. (Contributed by + Stefan O'Rear, 29-Jan-2015.) $) + odumeet $p |- .\/ = ( meet ` D ) $= + ( va vb vc cjn cfv cmee cvv wcel wceq cv wbr coprab eqid codu c0 oduglb + club cglb breqd oprabbidv joinfval fvexi meetfval mp1i 3eqtr4d wn fvprc + cpr syl5eq fveq2d meet0 eqtrdi eqtr4d pm2.61i eqtri ) BCIJZAKJZECLMZVAV + BNVCFOGOUMZHOZCUBJZPZFGHQVDVEAUCJZPZFGHQZVAVBVCVGVIFGHVCVFVHVDVEAVFCLDV + FRZUAUDUEFGHVFVACLVKVARUFALMVBVJNVCACSDUGFGHVHAVBLVHRVBRUHUIUJVCUKZVATV + BCIULVLVBTKJTVLATKVLACSJTDCSULUNUOUPUQURUSUT $. + $} + $} + + ${ + $d .<_ x y z w $. $d B x y z w $. $d K x y z w $. $d S x y z w $. + poslubmo.l $e |- .<_ = ( le ` K ) $. + poslubmo.b $e |- B = ( Base ` K ) $. + $( Least upper bounds in a poset are unique if they exist. (Contributed by + Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.) $) + poslubmo $p |- ( ( K e. Poset /\ S C_ B ) -> E* x e. B + ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) $= + ( vw wcel wa cv wbr wral wi weq breq2 ralbidv imbi12d cpo simprrl simprlr + wss wrmo simplrr rspcdva mpd simprll simprrr simplrl wb posasymb ad4ant13 + 3expb mpbi2and ex ralrimivva breq1 imbi2d anbi12d rmo4 sylibr ) FUAKZEDUD + ZLZBMZAMZGNZBEOZVGCMZGNZBEOZVHVKGNZPZCDOZLZVGJMZGNZBEOZVMVRVKGNZPZCDOZLZL + ZAJQZPZJDOADOVQADUEVFWGAJDDVFVHDKZVRDKZLZLZWEWFWKWELZVHVRGNZVRVHGNZWFWLVT + WMWKVQVTWCUBWLVOVTWMPCDVRCJQZVMVTVNWMWOVLVSBEVKVRVGGRSVKVRVHGRTWKVJVPWDUC + VFWHWIWEUFUGUHWLVJWNWKVJVPWDUIWLWBVJWNPCDVHCAQZVMVJWAWNWPVLVIBEVKVHVGGRSV + KVHVRGRTWKVQVTWCUJVFWHWIWEUKUGUHVDWJWMWNLWFULZVEWEVDWHWIWQDFGVHVRIHUMUOUN + UPUQURVQWDAJDWFVJVTVPWCWFVIVSBEVHVRVGGRSWFVOWBCDWFVNWAVMVHVRVKGUSUTSVAVBV + C $. + + $( Greatest lower bounds in a poset are unique if they exist. (Contributed + by NM, 20-Sep-2018.) $) + posglbmo $p |- ( ( K e. Poset /\ S C_ B ) -> E* x e. B + ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) $= + ( vw wcel wa cv wbr wral wi weq breq1 ralbidv imbi12d cpo simprrl simprlr + wss wrmo simplrr rspcdva simprll simprrr simplrl wb ancom posasymb syl5bb + mpd w3a 3expb ad4ant13 mpbi2and ex ralrimivva breq2 imbi2d anbi12d sylibr + rmo4 ) FUAKZEDUDZLZAMZBMZGNZBEOZCMZVKGNZBEOZVNVJGNZPZCDOZLZJMZVKGNZBEOZVP + VNWAGNZPZCDOZLZLZAJQZPZJDOADOVTADUEVIWJAJDDVIVJDKZWADKZLZLZWHWIWNWHLZWAVJ + GNZVJWAGNZWIWOWCWPWNVTWCWFUBWOVRWCWPPCDWACJQZVPWCVQWPWRVOWBBEVNWAVKGRSVNW + AVJGRTWNVMVSWGUCVIWKWLWHUFUGUOWOVMWQWNVMVSWGUHWOWEVMWQPCDVJCAQZVPVMWDWQWS + VOVLBEVNVJVKGRSVNVJWAGRTWNVTWCWFUIVIWKWLWHUJUGUOVGWMWPWQLZWIUKZVHWHVGWKWL + XAWTWQWPLVGWKWLUPWIWPWQULDFGVJWAIHUMUNUQURUSUTVAVTWGAJDWIVMWCVSWFWIVLWBBE + VJWAVKGRSWIVRWECDWIVQWDVPVJWAVNGVBVCSVDVFVE $. + $} + + ${ + $d .<_ x y z $. $d B x y z $. $d K x y z $. $d S x y z $. $d U x y z $. + $d T x y z $. $d ph x y z $. + poslubd.l $e |- .<_ = ( le ` K ) $. + poslubd.b $e |- B = ( Base ` K ) $. + poslubd.u $e |- U = ( lub ` K ) $. + poslubd.k $e |- ( ph -> K e. Poset ) $. + poslubd.s $e |- ( ph -> S C_ B ) $. + poslubd.t $e |- ( ph -> T e. B ) $. + poslubd.ub $e |- ( ( ph /\ x e. S ) -> x .<_ T ) $. + poslubd.le $e |- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y ) $. + $( Properties which determine the least upper bound in a poset. + (Contributed by Stefan O'Rear, 31-Jan-2015.) $) + poslubd $p |- ( ph -> ( U ` S ) = T ) $= + ( vz wbr wral cfv cv wi wa crio cpo biid lubval wceq ralrimiva 3expia jca + wcel wreu wrex wrmo breq2 ralbidv breq1 imbi2d anbi12d rspcev syl2anc wss + wb poslubmo reu5 sylanbrc riota2 mpbid eqtrd ) AEGUABUBZRUBZISZBETZVLCUBZ + ISBETZVMVPISZUCZCDTZUDZRDUEZFAWARBCDEGHIUFKJLWAUGMNUHAVLFISZBETZVQFVPISZU + CZCDTZUDZWBFUIZAWDWGAWCBEPUJAWFCDAVPDUMVQWEQUKUJULZAFDUMZWARDUNZWHWIVEOAW + ARDUOZWARDUPZWLAWKWHWMOWJWAWHRFDVMFUIZVOWDVTWGWOVNWCBEVMFVLIUQURWOVSWFCDW + OVRWEVQVMFVPIUSUTURVAZVBVCAHUFUMEDVDWNMNRBCDEHIJKVFVCWARDVGVHWAWHRDFWPVIV + CVJVK $. + $} + + ${ + $d .<_ x y $. $d B x y $. $d K x y $. $d S x y $. $d U x y $. + $d T x y $. $d ph x y $. + poslubdg.l $e |- .<_ = ( le ` K ) $. + poslubdg.b $e |- ( ph -> B = ( Base ` K ) ) $. + poslubdg.u $e |- ( ph -> U = ( lub ` K ) ) $. + poslubdg.k $e |- ( ph -> K e. Poset ) $. + poslubdg.s $e |- ( ph -> S C_ B ) $. + poslubdg.t $e |- ( ph -> T e. B ) $. + poslubdg.ub $e |- ( ( ph /\ x e. S ) -> x .<_ T ) $. + poslubdg.le $e |- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y ) $. + $( Properties which determine the least upper bound in a poset. + (Contributed by Stefan O'Rear, 31-Jan-2015.) $) + poslubdg $p |- ( ph -> ( U ` S ) = T ) $= + ( cfv eqid cv club fveq1d cbs sseqtrd eleqtrd wcel eleq2d biimpar 3adant3 + wbr wral syld3an2 poslubd eqtrd ) AEGREHUARZRFAEGUOLUBABCHUCRZEFUOHIJUPSU + OSMAEDUPNKUDAFDUPOKUEPACTZDUFZUQUPUFZBTUQIUJBEUKZFUQIUJAUSURUTAURUSADUPUQ + KUGUHUIQULUMUN $. + $} + + ${ + $d .<_ x y $. $d B x y $. $d K x y $. $d S x y $. $d G x y $. + $d T x y $. $d ph x y $. + posglbdg.l $e |- .<_ = ( le ` K ) $. + posglbdg.b $e |- ( ph -> B = ( Base ` K ) ) $. + posglbdg.g $e |- ( ph -> G = ( glb ` K ) ) $. + posglbdg.k $e |- ( ph -> K e. Poset ) $. + posglbdg.s $e |- ( ph -> S C_ B ) $. + posglbdg.t $e |- ( ph -> T e. B ) $. + posglbdg.lb $e |- ( ( ph /\ x e. S ) -> T .<_ x ) $. + posglbdg.gt $e |- ( ( ph /\ y e. B /\ A. x e. S y .<_ x ) -> y .<_ T ) $. + $( Properties which determine the greatest lower bound in a poset. + (Contributed by Stefan O'Rear, 31-Jan-2015.) $) + posglbdg $p |- ( ph -> ( G ` S ) = T ) $= + ( cfv wcel wbr codu ccnv eqid oduleval cbs odubas eqtrdi cglb club odulub + cpo wceq syl eqtrd odupos cv wa cvv vex brcnvg sylancr adantr mpbird wral + wb w3a brcnv ralbii syl3an3b sylancl 3ad2ant1 poslubdg ) ABCDEFGHUARZIUBZ + VMIHVMUCZJUDADHUERZVMUERKVPVMHVOVPUCUFUGAGHUHRZVMUIRZLAHUKSZVQVRULMVMVQHU + KVOVQUCUJUMUNAVSVMUKSMVMHVOUOUMNOABUPZESZUQVTFVNTZFVTITZPAWBWCVEZWAAVTURS + FDSZWDBUSZOVTFURDIUTVAVBVCACUPZDSZVTWGVNTZBEVDZVFFWGVNTZWGFITZWJAWHWGVTIT + ZBEVDWLWIWMBEVTWGIWFCUSZVGVHQVIAWHWKWLVEZWJAWEWGURSWOOWNFWGDURIUTVJVKVCVL + $. + $} + + +$( +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Totally ordered sets (tosets) +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# +$) + $c Toset $. $( Extend class notation with the class of all tosets. $) @@ -216877,6 +217198,13 @@ net proof size (existence part)? $) $} +$( +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Lattices +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# +$) + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Lattices @@ -216908,6 +217236,22 @@ net proof size (existence part)? $) JAUHCLQERUDZTVBUOUTULURVBUNDVBUNCOJDUHCOQGRSVCTUEHUFUG $. $} + ${ + odulat.d $e |- D = ( ODual ` O ) $. + $( Being a lattice is self-dual. (Contributed by Stefan O'Rear, + 29-Jan-2015.) $) + odulatb $p |- ( O e. V -> ( O e. Lat <-> D e. Lat ) ) $= + ( wcel cpo cjn cfv cdm cbs cxp wceq cmee wa clat oduposb ancom eqid islat + wb a1i anbi12d odubas odujoin odumeet 3bitr4g ) BCEZBFEZBGHZIBJHZUJKZLZBM + HZIUKLZNZNAFEZUNULNZNBOEAOEUGUHUPUOUQABCDPUOUQTUGULUNQUAUBUJUIBUMUJRZUIRZ + UMRZSUJUMAUIUJABDURUCAUMBDUTUDAUIBDUSUESUF $. + + $( Being a lattice is self-dual. (Contributed by Stefan O'Rear, + 29-Jan-2015.) $) + odulat $p |- ( O e. Lat -> D e. Lat ) $= + ( clat wcel odulatb ibi ) BDEADEABDCFG $. + $} + ${ latcl2.b $e |- B = ( Base ` K ) $. latcl2.j $e |- .\/ = ( join ` K ) $. @@ -217537,6 +217881,76 @@ net proof size (existence part)? $) AMZWBVNRVPVSVJUSVBVAWCVPVQVRABCHGIKUPTACEFVMILSTUNUQUR $. $} + ${ + latmass.b $e |- B = ( Base ` K ) $. + latmass.m $e |- ./\ = ( meet ` K ) $. + $( Lattice meet is associative. (Contributed by Stefan O'Rear, + 30-Jan-2015.) $) + latmass $p |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> + ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) ) $= + ( clat wcel codu cfv w3a co wceq eqid odulat odubas odujoin latjass sylan + ) BIJBKLZIJDAJEAJFAJMDECNFCNDEFCNCNOUBBUBPZQACUBDEFAUBBUCGRUBCBUCHSTUA $. + $} + + ${ + $d u v w x y z K $. $d u v w x y z B $. $d u v w x y z .\/ $. + $d u v w x y z ./\ $. + latdisd.b $e |- B = ( Base ` K ) $. + latdisd.j $e |- .\/ = ( join ` K ) $. + latdisd.m $e |- ./\ = ( meet ` K ) $. + $( Lemma for ~ latdisd . (Contributed by Stefan O'Rear, 30-Jan-2015.) $) + latdisdlem $p |- ( K e. Lat -> + ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = + ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> + A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = + ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) ) $= + ( wcel cv co wceq oveq1 oveq2d syl3anc clat wa wi latmcl 3adant3r3 simpr1 + wral w3a simpr3 oveq12d eqeq12d weq oveq2 oveq1d rspc3v imp simpl latjcom + latabs1 eqtrd adantr simpr2 latjcl latmass syl13anc latabs2 3eqtrrd an32s + eqtr3d ralrimivvva ex ) IUANZFOZEOZDOZJPZHPZVMVNHPZVMVOHPZJPZQZDGUGEGUGFG + UGZAOZBOZCOZHPZJPZWCWDJPZWCWEJPZHPZQZCGUGBGUGAGUGVLWBUBWKABCGGGVLWCGNZWDG + NZWEGNZUHZWBWKVLWOUBZWBUBZWJWHWCHPZWHWEHPZJPZWCWEWHHPZJPZWGWPWBWJWTQZWPWH + GNZWLWNWBXCUCVLWLWMXDWNGIJWCWDKMUDUEZVLWLWMWNUFZVLWLWMWNUIZWAXCWHVPHPZWHV + NHPZWHVOHPZJPZQWHWCVOJPZHPZWRXJJPZQFEDWHWCWEGGGVMWHQZVQXHVTXKVMWHVPHRXOVR + XIVSXJJVMWHVNHRVMWHVOHRUJUKEAULZXHXMXKXNXPVPXLWHHVNWCVOJRZSXPXIWRXJJVNWCW + HHUMUNUKDCULZXMWJXNWTXRXLWIWHHVOWEWCJUMSXRXJWSWRJVOWEWHHUMSUKUOTUPWPWTXBQ + WBWPWRWCWSXAJWPWRWCWHHPZWCWPVLXDWLWRXSQVLWOUQZXEXFGHIWHWCKLURTVLWLWMXSWCQ + WNGHIJWCWDKLMUSUEUTWPVLXDWNWSXAQXTXEXGGHIWHWEKLURTUJVAWQXBWCWEWCHPZWEWDHP + ZJPZJPZWGWQXAYCWCJWPWBXAYCQZWPWNWLWMWBYEUCXGXFVLWLWMWNVBZWAYEWEVPHPZWEVNH + PZWEVOHPZJPZQWEXLHPZYAYIJPZQFEDWEWCWDGGGFCULZVQYGVTYJVMWEVPHRYMVRYHVSYIJV + MWEVNHRVMWEVOHRUJUKXPYGYKYJYLXPVPXLWEHXQSXPYHYAYIJVNWCWEHUMUNUKDBULZYKXAY + LYCYNXLWHWEHVOWDWCJUMSYNYIYBYAJVOWDWEHUMSUKUOTUPSWPYDWGQWBWPWCYAJPZYBJPZY + DWGWPVLWLYAGNZYBGNZYPYDQXTXFWPVLWNWLYQXTXGXFGHIWEWCKLVCTWPVLWNWMYRXTXGYFG + HIWEWDKLVCTGIJWCYAYBKMVDVEWPYOWCYBWFJWPYOWCWCWEHPZJPZWCWPYAYSWCJWPVLWNWLY + AYSQXTXGXFGHIWEWCKLURTSWPVLWLWNYTWCQXTXFXGGHIJWCWEKLMVFTUTWPVLWNWMYBWFQXT + XGYFGHIWEWDKLURTUJVIVAUTVGVHVJVK $. + + $( In a lattice, joins distribute over meets if and only if meets + distribute over joins; the distributive property is self-dual. + (Contributed by Stefan O'Rear, 29-Jan-2015.) $) + latdisd $p |- ( K e. Lat -> + ( A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = + ( ( x .\/ y ) ./\ ( x .\/ z ) ) <-> + A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = + ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) ) $= + ( vu vv vw cv co wceq wral weq oveq1 eqeq12d clat wcel latdisdlem codu wi + cfv eqid odulat odubas odujoin odumeet impbid oveq12d oveq2d oveq2 oveq1d + syl cbvral3vw bitrdi ) FUAUBZANZBNZCNZGOEOVAVBEOVAVCEOGOPCDQBDQADQZKNZLNZ + MNZEOZGOZVEVFGOZVEVGGOZEOZPZMDQLDQKDQZVAVBVCEOZGOZVAVBGOZVAVCGOZEOZPZCDQB + DQADQUTVDVNKLMCBADEFGHIJUCUTFUDUFZUAUBVNVDUEWAFWAUGZUHABCMLKDGWAEDWAFWBHU + IWAGFWBJUJWAEFWBIUKUCUQULVMVTVAVHGOZVAVFGOZVAVGGOZEOZPVAVBVGEOZGOZVQWEEOZ + PKLMABCDDDKARZVIWCVLWFVEVAVHGSWJVJWDVKWEEVEVAVFGSVEVAVGGSUMTLBRZWCWHWFWIW + KVHWGVAGVFVBVGESUNWKWDVQWEEVFVBVAGUOUPTMCRZWHVPWIVSWLWGVOVAGVGVCVBEUOUNWL + WEVRVQEVGVCVAGUOUNTURUS $. + $} + + +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Complete lattices +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + $c CLat $. $( Extend class notation with complete lattices. $) @@ -217617,6 +218031,21 @@ net proof size (existence part)? $) $. $} + ${ + oduclatb.d $e |- D = ( ODual ` O ) $. + $( Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, + 29-Jan-2015.) $) + oduclatb $p |- ( O e. CLat <-> D e. CLat ) $= + ( ccla wcel cvv c0 club cfv eqid codu cpo cdm wceq cglb wa eqeq1d anbi12d + dmeqd isclat elex wn noel wss ssid base0 clatlubcl mpan2 mto fvprc syl5eq + eleq1d mtbiri con4i cbs oduposb ancom odulub oduglb syl5bb odubas 3bitr4g + cpw pm5.21nii ) BDEZBFEZADEZBDUAVFVGVFUBZVGGDEZVIGGHIZIZGEZVKUCVIGGUDVLGU + EGGVJGUFVJJUGUHUIVHAGDVHABKIGCBKUJUKULUMUNVFBLEZBHIZMZBUOIZVCZNZBOIZMZVQN + ZPZPALEZAHIZMZVQNZAOIZMZVQNZPZPVEVGVFVMWCWBWJABFCUPWBWAVRPVFWJVRWAUQVFWAW + FVRWIVFVTWEVQVFVSWDAVSBFCVSJZURSQVFVOWHVQVFVNWGAVNBFCVNJZUSSQRUTRVPVNVSBV + PJZWLWKTVPWDWGAVPABCWMVAWDJWGJTVBVD $. + $} + ${ $d x y K $. $( A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) @@ -217799,347 +218228,95 @@ net proof size (existence part)? $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - The dual of an ordered set + Distributive lattices =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) - $c ODual $. - - $( Class function defining dual orders. $) - codu $a class ODual $. - - $( Define the dual of an ordered structure, which replaces the order - component of the structure with its reverse. See ~ odubas , ~ oduleval , - and ~ oduleg for its principal properties. - - _EDITORIAL_: likely usable to simplify many lattice proofs, as it allows - for duality arguments to be formalized; for instance ~ latmass . - (Contributed by Stefan O'Rear, 29-Jan-2015.) $) - df-odu $a |- ODual = ( w e. _V |-> - ( w sSet <. ( le ` ndx ) , `' ( le ` w ) >. ) ) $. - - ${ - $d D a $. $d .<_ a $. $d O a $. $d G a $. $d A a $. $d B a $. - oduval.d $e |- D = ( ODual ` O ) $. - - ${ - oduval.l $e |- .<_ = ( le ` O ) $. - $( Value of an order dual structure. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) - oduval $p |- D = ( O sSet <. ( le ` ndx ) , `' .<_ >. ) $= - ( va codu cfv cnx cple ccnv cop csts co cvv wcel wceq cv id fveq2 fvmpt - cnveqd opeq2d oveq12d df-odu ovex wn c0 reldmsets ovprc1 eqtr4d pm2.61i - fvprc cnveqi opeq2i oveq2i 3eqtr4i ) CGHZCIJHZCJHZKZLZMNZACUSBKZLZMNCOP - ZURVCQFCFRZUSVGJHZKZLZMNVCOGVGCQZVGCVJVBMVKSVKVIVAUSVKVHUTVGCJTUBUCUDFU - ECVBMUFUAVFUGURUHVCCGUMCVBMUIUJUKULDVEVBCMVDVAUSBUTEUNUOUPUQ $. - - $( Value of the less-equal relation in an order dual structure. - (Contributed by Stefan O'Rear, 29-Jan-2015.) $) - oduleval $p |- `' .<_ = ( le ` D ) $= - ( cple cfv ccnv cnx cop csts co cvv wcel wceq fvex cnvex pleid setsid - c0 mpan2 str0 fvprc cnveqd cnv0 eqtrdi reldmsets ovprc1 3eqtr4a pm2.61i - wn fveq2d cnveqi eqid oduval fveq2i 3eqtr4i ) CFGZHZCIFGZUSJZKLZFGZBHAF - GCMNZUSVCOZVDUSMNVEURCFPQMUSFMCRSUAVDUKZTTFGUSVCFUTRUBVFUSTHTVFURTCFUCU - DUEUFVFVBTFCVAKUGUHULUIUJBUREUMAVBFAURCDURUNUOUPUQ $. - - oduleg.g $e |- G = ( le ` D ) $. - $( Truth of the less-equal relation in an order dual structure. - (Contributed by Stefan O'Rear, 29-Jan-2015.) $) - oduleg $p |- ( ( A e. V /\ B e. W ) -> ( A G B <-> B .<_ A ) ) $= - ( wbr ccnv wcel wa cple cfv oduleval eqtr4i breqi brcnvg syl5bb ) ABDLA - BEMZLAGNBHNOBAELABDUCDCPQUCKCEFIJRSTABGHEUAUB $. - $} - - odubas.b $e |- B = ( Base ` O ) $. - $( Base set of an order dual structure. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) - odubas $p |- B = ( Base ` D ) $= - ( cbs cfv cnx cple ccnv cop csts co baseid wne c1 cc0 cdc 1re 1lt10 mpbir - ltneii basendx plendx neeq12i setsnid eqid oduval fveq2i 3eqtr4i ) CFGCHI - GZCIGZJZKLMZFGABFGUMUKFCNHFGZUKOPPQRZOPUPSTUBUOPUKUPUCUDUEUAUFEBUNFBULCDU - LUGUHUIUJ $. - $} - - ${ - $d B x y a b c $. $d ph x y a b c $. $d K x y a b c $. $d L x y a b c $. - pospropd.kv $e |- ( ph -> K e. V ) $. - pospropd.lv $e |- ( ph -> L e. W ) $. - pospropd.kb $e |- ( ph -> B = ( Base ` K ) ) $. - pospropd.lb $e |- ( ph -> B = ( Base ` L ) ) $. - pospropd.xy $e |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> - ( x ( le ` K ) y <-> x ( le ` L ) y ) ) $. - $( Posethood is determined only by structure components and only by the - value of the relation within the base set. (Contributed by Stefan - O'Rear, 29-Jan-2015.) $) - pospropd $p |- ( ph -> ( K e. Poset <-> L e. Poset ) ) $= - ( va vb vc wbr wa wral wb cvv wcel cv cple cfv weq w3a cbs cpo ralrimivva - simp1 jca breq1 bibi12d breq2 rspc2va sylan 3adantl3 3simpb 3comr anbi12d - wi imbi1d 3adantl1 3anbi123d sylan2 ancoms 3exp2 imp42 ralbidva 2ralbidva - imbi12d wceq raleq raleqbi1dv 3bitr3d elexd biantrurd eqid ispos 3bitr4g - syl ) AEUAUBZNUCZWDEUDUEZQZWDOUCZWEQZWGWDWEQZRZNOUFZVBZWHWGPUCZWEQZRZWDWM - WEQZVBZUGZPEUHUEZSZOWSSZNWSSZRZFUAUBZWDWDFUDUEZQZWDWGXEQZWGWDXEQZRZWKVBZX - GWGWMXEQZRZWDWMXEQZVBZUGZPFUHUEZSZOXPSZNXPSZRZEUIUBFUIUBAXBXSXCXTAWRPDSZO - DSZNDSZXOPDSZODSZNDSZXBXSAYAYDNODDAWDDUBZWGDUBZRRWRXOPDAYGYHWMDUBZWRXOTZA - YGYHYIYJYGYHYIUGZAYJAYKBUCZCUCZWEQZYLYMXEQZTZCDSBDSZYJAYPBCDDMUJYKYQRZWFX - FWLXJWQXNYKYGYGRYQWFXFTZYKYGYGYGYHYIUKZYTULYPYSWDYMWEQZWDYMXEQZTZBCWDWDDD - BNUFYNUUAYOUUBYLWDYMWEUMYLWDYMXEUMUNZCNUFZUUAWFUUBXFYMWDWDWEUOYMWDWDXEUOU - NUPUQYRWJXIWKYRWHXGWIXHYGYHYQWHXGTZYIYPUUFUUCBCWDWGDDUUDCOUFUUAWHUUBXGYMW - GWDWEUOYMWGWDXEUOUNUPURZYKYHYGRZYQWIXHTZYHYIYGUUHYHYIYGUSUTYPUUIWGYMWEQZW - GYMXEQZTZBCWGWDDDBOUFYNUUJYOUUKYLWGYMWEUMYLWGYMXEUMUNZUUEUUJWIUUKXHYMWDWG - WEUOYMWDWGXEUOUNUPUQVAVCYRWOXLWPXMYRWHXGWNXKUUGYHYIYQWNXKTZYGYPUUNUULBCWG - WMDDUUMCPUFZUUJWNUUKXKYMWMWGWEUOYMWMWGXEUOUNUPVDVAYKYGYIRYQWPXMTZYGYHYIUS - YPUUPUUCBCWDWMDDUUDUUOUUAWPUUBXMYMWMWDWEUOYMWMWDXEUOUNUPUQVLVEVFVGVHVIVJV - KADWSVMYCXBTKYBXANDWSYAWTODWSWRPDWSVNVOVOWBADXPVMYFXSTLYEXRNDXPYDXQODXPXO - PDXPVNVOVOWBVPAWCXBAEGIVQVRAXDXSAFHJVQVRVPNOPWSEWEWSVSWEVSVTNOPXPFXEXPVSX - EVSVTWA $. - $} - - ${ - $d D a b c $. $d O a b c $. $d V a b c $. - odupos.d $e |- D = ( ODual ` O ) $. - $( Being a poset is a self-dual property. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) - odupos $p |- ( O e. Poset -> D e. Poset ) $= - ( va vb vc wcel cbs cfv cple cvv a1i wceq eqid cv wa wbr vex brcnv w3a wi - cpo ccnv fvexi odubas oduleval posref sylibr weq anbi12ci posasymb biimpd - codu syl5bi 3anrev postr sylan2b 3imtr4g isposd ) BUBGZDEFBHIZABJIZUCZKAK - GUTABUMCUDLVAAHIMUTVAABCVANZUELVCAJIMUTAVBBCVBNZUFLUTDOZVAGZPVFVFVBQVFVFV - CQVABVBVFVDVEUGVFVFVBDRZVHSUHVFEOZVCQZVIVFVCQZPVFVIVBQZVIVFVBQZPZUTVGVIVA - GZTZDEUIZVJVMVKVLVFVIVBVHERZSZVIVFVBVRVHSUJVPVNVQVABVBVFVIVDVEUKULUNUTVGV - OFOZVAGZTZPVTVIVBQZVMPZVTVFVBQZVJVIVTVCQZPVFVTVCQWBUTWAVOVGTWDWEUAVGVOWAU - OVABVBVTVIVFVDVEUPUQVJVMWFWCVSVIVTVBVRFRZSUJVFVTVBVHWGSURUS $. + $c DLat $. - $( Being a poset is a self-dual property. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) - oduposb $p |- ( O e. V -> ( O e. Poset <-> D e. Poset ) ) $= - ( va vb wcel cpo odupos codu cfv eqid cbs odubas a1i cv cple wbr wa ccnv - fvexd id wceq eqidd wb oduleval eqcomi breqi brcnv 3bitri pospropd syl5ib - cvv vex impbid2 ) BCGZBHGZAHGZABDIURAJKZHGUPUQUSAUSLZIUPEFBMKZUSBUMCUPAJU - AUPUBVAUSMKUCUPVAUSAUTVAABDVALNNOUPVAUDEPZFPZUSQKZRZVBVCBQKZRZUEUPVBVAGVC - VAGSSVEVBVCVFTZTZRVCVBVHRVGVBVCVDVIVIVDUSVHAUTAVFBDVFLUFUFUGUHVBVCVHEUNZF - UNZUIVCVBVFVKVJUIUJOUKULUO $. - $} + $( The class of distributive lattices. $) + cdlat $a class DLat $. ${ - $d x y z w $. - $( Lemma for ~ odujoin . (Contributed by Stefan O'Rear, 29-Jan-2015.) - TODO ( ~ df-riota update): This proof increased from 152 bytes to 547 - bytes after the ~ df-riota change. Any way to shorten it? ~ join0 - also. $) - meet0 $p |- ( meet ` (/) ) = (/) $= - ( vx vy vz vw c0 cfv cv wbr cvv wceq 0ex eqid ax-mp cop wa wex wral eqtri - cab nex cmee cpr cglb coprab wcel meetfval df-oprab br0 cple wi crio cmpt - cpw wreu cres base0 biid glbfval reu0 abf reseq2i res0 breqi mtbir intnan - id ) EUAFZAGZBGZUBZCGZEUCFZHZABCUDZEEIUEZVGVNJKABCVLEVGIVLLZVGLUFMVNDGZVH - VINVKNJZVMOZCPZBPZAPZDSEVMABCDUGWBDWAAVTBVSCVMVRVMVJVKEHVJVKUHVJVKVLEVLAE - UMVIVKEUIFZHCVHQVQVKWCHCVHQVQVIWCHUJDEQOZBEUKULZWDBEUNZASZUOZEVOVLWHJKVOW - DBCDEVLEWCIAUPWCLVPWDUQVOVFURMWHWEEUOEWGEWEWFAWDBUSUTVAWEVBRRVCVDVETTTUTR - R $. - - $( Lemma for ~ odumeet . (Contributed by Stefan O'Rear, 29-Jan-2015.) $) - join0 $p |- ( join ` (/) ) = (/) $= - ( vx vy vz vw c0 cfv cv wbr cvv wceq 0ex eqid ax-mp cop wa wex wral eqtri - cab nex cjn cpr club coprab wcel joinfval df-oprab br0 cpw cple crio cmpt - wi wreu cres base0 biid lubfval reu0 abf reseq2i res0 breqi mtbir intnan - id ) EUAFZAGZBGZUBZCGZEUCFZHZABCUDZEEIUEZVGVNJKABCVLVGEIVLLZVGLUFMVNDGZVH - VINVKNJZVMOZCPZBPZAPZDSEVMABCDUGWBDWAAVTBVSCVMVRVMVJVKEHVJVKUHVJVKVLEVLDE - UIVHVKEUJFZHAVQQVHVIWCHAVQQVKVIWCHUMBEQOZCEUKULZWDCEUNZDSZUOZEVOVLWHJKVOW - DCABEVLEWCIDUPWCLVPWDUQVOVFURMWHWEEUOEWGEWEWFDWDCUSUTVAWEVBRRVCVDVETTTUTR - R $. + $d k b j m x y z $. + $( A _distributive lattice_ is a lattice in which meets distribute over + joins, or equivalently ( ~ latdisd ) joins distribute over meets. + (Contributed by Stefan O'Rear, 30-Jan-2015.) $) + df-dlat $a |- DLat = { k e. Lat | [. ( Base ` k ) / b ]. + [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b + A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) } $. $} ${ - $d D a b c d $. $d L a b c d $. $d U a b c d $. $d O a b c d $. - $d V a b c d $. $d .\/ a b $. $d ./\ a b $. - oduglb.d $e |- D = ( ODual ` O ) $. - - ${ - oduglb.l $e |- U = ( lub ` O ) $. - $( Greatest lower bounds in a dual order are least upper bounds in the - original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) $) - oduglb $p |- ( O e. V -> U = ( glb ` D ) ) $= - ( va vc vb vd wcel cfv cv wbr wral wi vex brcnv ralbii eqid club cbs wa - cglb cpw cple crio cmpt wreu cab cres ccnv wb imbi12i anbi12i riotabiia - a1i mpteq2i reubii abbii reseq12i eqcomi biid id lubfval cvv wceq fvexi - codu odubas oduleval glbfval mp1i 3eqtr4a syl5eq ) CDKZBCUALZAUDLZFVPGC - UBLZUEZHMZIMZCUFLZNZHGMZOZWAJMZWCNZHWEOZWBWGWCNZPZJVSOZUCZIVSUGZUHZWMIV - SUIZGUJZUKZGVTWBWAWCULZNZHWEOZWGWAWSNZHWEOZWGWBWSNZPZJVSOZUCZIVSUGZUHZX - GIVSUIZGUJZUKZVQVRXLWRXIWOXKWQGVTXHWNXGWMIVSXGWMUMWBVSKXAWFXFWLWTWDHWEW - BWAWCIQZHQZRSXEWKJVSXCWIXDWJXBWHHWEWGWAWCJQZXNRSWGWBWCXOXMRUNSUOZUQUPUR - XJWPGXGWMIVSXPUSUTVAVBVPWMIHJVSVQCWCDGVSTZWCTZVQTWMVCVPVDVEAVFKZVRXLVGV - PACVIEVHXSXGIHJVSVRAWSVFGVSACEXQVJAWCCEXRVKVRTXGVCXSVDVLVMVNVO $. - $} - - ${ - odumeet.j $e |- .\/ = ( join ` O ) $. - $( Meets in a dual order are joins in the original. (Contributed by - Stefan O'Rear, 29-Jan-2015.) $) - odumeet $p |- .\/ = ( meet ` D ) $= - ( va vb vc cjn cfv cmee cvv wcel wceq cv wbr coprab eqid codu c0 oduglb - club cglb breqd oprabbidv joinfval fvexi meetfval mp1i 3eqtr4d wn fvprc - cpr syl5eq fveq2d meet0 eqtrdi eqtr4d pm2.61i eqtri ) BCIJZAKJZECLMZVAV - BNVCFOGOUMZHOZCUBJZPZFGHQVDVEAUCJZPZFGHQZVAVBVCVGVIFGHVCVFVHVDVEAVFCLDV - FRZUAUDUEFGHVFVACLVKVARUFALMVBVJNVCACSDUGFGHVHAVBLVHRVBRUHUIUJVCUKZVATV - BCIULVLVBTKJTVLATKVLACSJTDCSULUNUOUPUQURUSUT $. - $} - - ${ - odulub.l $e |- L = ( glb ` O ) $. - $( Least upper bounds in a dual order are greatest lower bounds in the - original order. (Contributed by Stefan O'Rear, 29-Jan-2015.) $) - odulub $p |- ( O e. V -> L = ( lub ` D ) ) $= - ( va vb vc vd wcel cfv cv wbr wral wi vex brcnv ralbii eqid cglb cbs wa - club cpw cple crio cmpt wreu cab cres ccnv wb imbi12i anbi12i riotabiia - a1i mpteq2i reubii abbii reseq12i eqcomi biid id glbfval cvv wceq fvexi - codu odubas oduleval lubfval mp1i 3eqtr4a syl5eq ) CDKZBCUALZAUDLZFVPGC - UBLZUEZHMZIMZCUFLZNZIGMZOZJMZWBWCNZIWEOZWGWAWCNZPZJVSOZUCZHVSUGZUHZWMHV - SUIZGUJZUKZGVTWBWAWCULZNZIWEOZWBWGWSNZIWEOZWAWGWSNZPZJVSOZUCZHVSUGZUHZX - GHVSUIZGUJZUKZVQVRXLWRXIWOXKWQGVTXHWNXGWMHVSXGWMUMWAVSKXAWFXFWLWTWDIWEW - BWAWCIQZHQZRSXEWKJVSXCWIXDWJXBWHIWEWBWGWCXMJQZRSWAWGWCXNXORUNSUOZUQUPUR - XJWPGXGWMHVSXPUSUTVAVBVPWMHIJVSVQCWCDGVSTZWCTZVQTWMVCVPVDVEAVFKZVRXLVGV - PACVIEVHXSXGHIJVSVRAWSVFGVSACEXQVJAWCCEXRVKVRTXGVCXSVDVLVMVNVO $. - $} - - ${ - odujoin.m $e |- ./\ = ( meet ` O ) $. - $( Joins in a dual order are meets in the original. (Contributed by - Stefan O'Rear, 29-Jan-2015.) $) - odujoin $p |- ./\ = ( join ` D ) $= - ( va vb vc cmee cfv cjn cvv wcel wceq cv wbr coprab eqid codu c0 odulub - cglb club breqd oprabbidv meetfval fvexi joinfval mp1i 3eqtr4d wn fvprc - cpr syl5eq fveq2d join0 eqtrdi eqtr4d pm2.61i eqtri ) BCIJZAKJZECLMZVAV - BNVCFOGOUMZHOZCUBJZPZFGHQVDVEAUCJZPZFGHQZVAVBVCVGVIFGHVCVFVHVDVEAVFCLDV - FRZUAUDUEFGHVFCVALVKVARUFALMVBVJNVCACSDUGFGHVHVBALVHRVBRUHUIUJVCUKZVATV - BCIULVLVBTKJTVLATKVLACSJTDCSULUNUOUPUQURUSUT $. - $} - - $( Being a lattice is self-dual. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) - odulatb $p |- ( O e. V -> ( O e. Lat <-> D e. Lat ) ) $= - ( wcel cpo cjn cfv cdm cbs cxp wceq cmee wa clat oduposb ancom eqid islat - wb a1i anbi12d odubas odujoin odumeet 3bitr4g ) BCEZBFEZBGHZIBJHZUJKZLZBM - HZIUKLZNZNAFEZUNULNZNBOEAOEUGUHUPUOUQABCDPUOUQTUGULUNQUAUBUJUIBUMUJRZUIRZ - UMRZSUJUMAUIUJABDURUCAUMBDUTUDAUIBDUSUESUF $. - - $( Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) - oduclatb $p |- ( O e. CLat <-> D e. CLat ) $= - ( ccla wcel cvv c0 club cfv eqid codu cpo cdm wceq cglb wa eqeq1d anbi12d - dmeqd isclat elex wn noel wss ssid base0 clatlubcl mpan2 mto fvprc syl5eq - eleq1d mtbiri con4i cbs oduposb ancom odulub oduglb syl5bb odubas 3bitr4g - cpw pm5.21nii ) BDEZBFEZADEZBDUAVFVGVFUBZVGGDEZVIGGHIZIZGEZVKUCVIGGUDVLGU - EGGVJGUFVJJUGUHUIVHAGDVHABKIGCBKUJUKULUMUNVFBLEZBHIZMZBUOIZVCZNZBOIZMZVQN - ZPZPALEZAHIZMZVQNZAOIZMZVQNZPZPVEVGVFVMWCWBWJABFCUPWBWAVRPVFWJVRWAUQVFWAW - FVRWIVFVTWEVQVFVSWDAVSBFCVSJZURSQVFVOWHVQVFVNWGAVNBFCVNJZUSSQRUTRVPVNVSBV - PJZWLWKTVPWDWGAVPABCWMVAWDJWGJTVBVD $. - - $( Being a lattice is self-dual. (Contributed by Stefan O'Rear, - 29-Jan-2015.) $) - odulat $p |- ( O e. Lat -> D e. Lat ) $= - ( clat wcel odulatb ibi ) BDEADEABDCFG $. - $} + $d k b j m x y z K $. $d k b j m x y z B $. $d k b j m x y z .\/ $. + $d k b j m x y z ./\ $. + isdlat.b $e |- B = ( Base ` K ) $. + isdlat.j $e |- .\/ = ( join ` K ) $. + isdlat.m $e |- ./\ = ( meet ` K ) $. + $( Property of being a distributive lattice. (Contributed by Stefan + O'Rear, 30-Jan-2015.) $) + isdlat $p |- ( K e. DLat <-> ( K e. Lat /\ A. x e. B A. y e. B A. z e. B + ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) ) $= + ( vj vm vb cv co wceq wral cmee cfv wsbc cjn cbs clat cdlat fveq2 eqtr4di + vk sbceqbid fvexi wb wa raleq raleqbi1dv simpr eqidd simpl oveqd oveq123d + sbceq1d eqeq12d ralbidv 2ralbidv sylan9bb sbc3ie bitrdi df-dlat elrab2 + 3impb ) ANZBNZCNZKNZOZLNZOZVIVJVNOZVIVKVNOZVLOZPZCMNZQZBVTQZAVTQZLUGNZRSZ + TZKWDUASZTZMWDUBSZTZVIVJVKEOZGOZVIVJGOZVIVKGOZEOZPZCDQZBDQADQZUGFUCUDWDFP + ZWJWCLGTZKETZMDTWRWSWHXAMWIDWSWIFUBSDWDFUBUEHUFWSWFWTKWGEWSWGFUASEWDFUAUE + IUFWSWCLWEGWSWEFRSGWDFRUEJUFUSUHUHWCWRMKLDEGDFUBHUIEFUAIUIGFRJUIVTDPZVLEP + ZVNGPZWCWRUJXBWCVSCDQZBDQZADQXCXDUKZWRWBXFAVTDWAXEBVTDVSCVTDULUMUMXGXEWQA + BDDXGVSWPCDXGVOWLVRWOXGVIVIVMWKVNGXCXDUNZXGVIUOXGVLEVJVKXCXDUPZUQURXGVPWM + VQWNVLEXIXGVNGVIVJXHUQXGVNGVIVKXHUQURUTVAVBVCVHVDVEABCKUGLMVFVG $. - ${ - $d .<_ x y z w $. $d B x y z w $. $d K x y z w $. $d S x y z w $. - poslubmo.l $e |- .<_ = ( le ` K ) $. - poslubmo.b $e |- B = ( Base ` K ) $. - $( Least upper bounds in a poset are unique if they exist. (Contributed by - Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.) $) - poslubmo $p |- ( ( K e. Poset /\ S C_ B ) -> E* x e. B - ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) $= - ( vw wcel wa cv wbr wral wi weq breq2 ralbidv imbi12d cpo simprrl simprlr - wss wrmo simplrr rspcdva mpd simprll simprrr simplrl wb posasymb ad4ant13 - 3expb mpbi2and ex ralrimivva breq1 imbi2d anbi12d rmo4 sylibr ) FUAKZEDUD - ZLZBMZAMZGNZBEOZVGCMZGNZBEOZVHVKGNZPZCDOZLZVGJMZGNZBEOZVMVRVKGNZPZCDOZLZL - ZAJQZPZJDOADOVQADUEVFWGAJDDVFVHDKZVRDKZLZLZWEWFWKWELZVHVRGNZVRVHGNZWFWLVT - WMWKVQVTWCUBWLVOVTWMPCDVRCJQZVMVTVNWMWOVLVSBEVKVRVGGRSVKVRVHGRTWKVJVPWDUC - VFWHWIWEUFUGUHWLVJWNWKVJVPWDUIWLWBVJWNPCDVHCAQZVMVJWAWNWPVLVIBEVKVHVGGRSV - KVHVRGRTWKVQVTWCUJVFWHWIWEUKUGUHVDWJWMWNLWFULZVEWEVDWHWIWQDFGVHVRIHUMUOUN - UPUQURVQWDAJDWFVJVTVPWCWFVIVSBEVHVRVGGRSWFVOWBCDWFVNWAVMVHVRVKGUSUTSVAVBV - C $. + $d X x y z $. $d Y x y z $. $d Z x y z $. - $( Greatest lower bounds in a poset are unique if they exist. (Contributed - by NM, 20-Sep-2018.) $) - posglbmo $p |- ( ( K e. Poset /\ S C_ B ) -> E* x e. B - ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) ) $= - ( vw wcel wa cv wbr wral wi weq breq1 ralbidv imbi12d cpo simprrl simprlr - wss wrmo simplrr rspcdva simprll simprrr simplrl wb ancom posasymb syl5bb - mpd w3a 3expb ad4ant13 mpbi2and ex ralrimivva breq2 imbi2d anbi12d sylibr - rmo4 ) FUAKZEDUDZLZAMZBMZGNZBEOZCMZVKGNZBEOZVNVJGNZPZCDOZLZJMZVKGNZBEOZVP - VNWAGNZPZCDOZLZLZAJQZPZJDOADOVTADUEVIWJAJDDVIVJDKZWADKZLZLZWHWIWNWHLZWAVJ - GNZVJWAGNZWIWOWCWPWNVTWCWFUBWOVRWCWPPCDWACJQZVPWCVQWPWRVOWBBEVNWAVKGRSVNW - AVJGRTWNVMVSWGUCVIWKWLWHUFUGUOWOVMWQWNVMVSWGUHWOWEVMWQPCDVJCAQZVPVMWDWQWS - VOVLBEVNVJVKGRSVNVJWAGRTWNVTWCWFUIVIWKWLWHUJUGUOVGWMWPWQLZWIUKZVHWHVGWKWL - XAWTWQWPLVGWKWLUPWIWPWQULDFGVJWAIHUMUNUQURUSUTVAVTWGAJDWIVMWCVSWFWIVLWBBE - VJWAVKGRSWIVRWECDWIVQWDVPVJWAVNGVBVCSVDVFVE $. + $( In a distributive lattice, meets distribute over joins. (Contributed by + Stefan O'Rear, 30-Jan-2015.) $) + dlatmjdi $p |- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> + ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) $= + ( vx vy vz wcel cv co wceq wral oveq1 eqeq12d clat isdlat simprbi oveq12d + cdlat w3a oveq2d oveq2 oveq1d rspc3v mpan9 ) CUENZKOZLOZMOZBPZDPZUMUNDPZU + MUODPZBPZQZMARLARKARZEANFANGANUFEFGBPZDPZEFDPZEGDPZBPZQZULCUANVBKLMABCDHI + JUBUCVAVHEUPDPZEUNDPZEUODPZBPZQEFUOBPZDPZVEVKBPZQKLMEFGAAAUMEQZUQVIUTVLUM + EUPDSVPURVJUSVKBUMEUNDSUMEUODSUDTUNFQZVIVNVLVOVQUPVMEDUNFUOBSUGVQVJVEVKBU + NFEDUHUITUOGQZVNVDVOVGVRVMVCEDUOGFBUHUGVRVKVFVEBUOGEDUHUGTUJUK $. $} ${ - $d .<_ x y z $. $d B x y z $. $d K x y z $. $d S x y z $. $d U x y z $. - $d T x y z $. $d ph x y z $. - poslubd.l $e |- .<_ = ( le ` K ) $. - poslubd.b $e |- B = ( Base ` K ) $. - poslubd.u $e |- U = ( lub ` K ) $. - poslubd.k $e |- ( ph -> K e. Poset ) $. - poslubd.s $e |- ( ph -> S C_ B ) $. - poslubd.t $e |- ( ph -> T e. B ) $. - poslubd.ub $e |- ( ( ph /\ x e. S ) -> x .<_ T ) $. - poslubd.le $e |- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y ) $. - $( Properties which determine the least upper bound in a poset. - (Contributed by Stefan O'Rear, 31-Jan-2015.) $) - poslubd $p |- ( ph -> ( U ` S ) = T ) $= - ( vz wbr wral cfv cv wi wa crio cpo biid lubval wceq ralrimiva 3expia jca - wcel wreu wrex wrmo breq2 ralbidv breq1 imbi2d anbi12d rspcev syl2anc wss - wb poslubmo reu5 sylanbrc riota2 mpbid eqtrd ) AEGUABUBZRUBZISZBETZVLCUBZ - ISBETZVMVPISZUCZCDTZUDZRDUEZFAWARBCDEGHIUFKJLWAUGMNUHAVLFISZBETZVQFVPISZU - CZCDTZUDZWBFUIZAWDWGAWCBEPUJAWFCDAVPDUMVQWEQUKUJULZAFDUMZWARDUNZWHWIVEOAW - ARDUOZWARDUPZWLAWKWHWMOWJWAWHRFDVMFUIZVOWDVTWGWOVNWCBEVMFVLIUQURWOVSWFCDW - OVRWEVQVMFVPIUSUTURVAZVBVCAHUFUMEDVDWNMNRBCDEHIJKVFVCWARDVGVHWAWHRDFWPVIV - CVJVK $. + $d K x y z $. + $( A distributive lattice is a lattice. (Contributed by Stefan O'Rear, + 30-Jan-2015.) $) + dlatl $p |- ( K e. DLat -> K e. Lat ) $= + ( vx vy vz cdlat wcel clat cjn cfv cmee wceq cbs wral eqid isdlat simplbi + cv co ) AEFAGFBQZCQZDQZAHIZRAJIZRSTUCRSUAUCRUBRKDALIZMCUDMBUDMBCDUDUBAUCU + DNUBNUCNOP $. $} ${ - $d .<_ x y $. $d B x y $. $d K x y $. $d S x y $. $d U x y $. - $d T x y $. $d ph x y $. - poslubdg.l $e |- .<_ = ( le ` K ) $. - poslubdg.b $e |- ( ph -> B = ( Base ` K ) ) $. - poslubdg.u $e |- ( ph -> U = ( lub ` K ) ) $. - poslubdg.k $e |- ( ph -> K e. Poset ) $. - poslubdg.s $e |- ( ph -> S C_ B ) $. - poslubdg.t $e |- ( ph -> T e. B ) $. - poslubdg.ub $e |- ( ( ph /\ x e. S ) -> x .<_ T ) $. - poslubdg.le $e |- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y ) $. - $( Properties which determine the least upper bound in a poset. - (Contributed by Stefan O'Rear, 31-Jan-2015.) $) - poslubdg $p |- ( ph -> ( U ` S ) = T ) $= - ( cfv eqid cv club fveq1d cbs sseqtrd eleqtrd wcel eleq2d biimpar 3adant3 - wbr wral syld3an2 poslubd eqtrd ) AEGREHUARZRFAEGUOLUBABCHUCRZEFUOHIJUPSU - OSMAEDUPNKUDAFDUPOKUEPACTZDUFZUQUPUFZBTUQIUJBEUKZFUQIUJAUSURUTAURUSADUPUQ - KUGUHUIQULUMUN $. + $d K x y z $. $d D x y z $. $d V x y z $. + odudlat.d $e |- D = ( ODual ` K ) $. + $( The dual of a distributive lattice is a distributive lattice and + conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.) $) + odudlatb $p |- ( K e. V -> ( K e. DLat <-> D e. DLat ) ) $= + ( vx vy vz wcel clat cv cjn cfv co cmee wceq wral wa cdlat eqid isdlat + cbs latdisd bicomd pm5.32i odulatb anbi1d syl5bb odujoin odumeet 3bitr4g + odubas ) BCHZBIHZEJZFJZGJZBKLZMBNLZMUNUOURMUNUPURMUQMOGBUALZPFUSPEUSPZQZA + IHZUNUOUPURMUQMUNUOUQMUNUPUQMURMOGUSPFUSPEUSPZQZBRHARHVAUMVCQULVDUMUTVCUM + VCUTEFGUSUQBURUSSZUQSZURSZUBUCUDULUMVBVCABCDUEUFUGEFGUSUQBURVEVFVGTEFGUSU + RAUQUSABDVEUKAURBDVGUHAUQBDVFUITUJ $. $} ${ - $d .<_ x y $. $d B x y $. $d K x y $. $d S x y $. $d G x y $. - $d T x y $. $d ph x y $. - posglbd.l $e |- .<_ = ( le ` K ) $. - posglbd.b $e |- ( ph -> B = ( Base ` K ) ) $. - posglbd.g $e |- ( ph -> G = ( glb ` K ) ) $. - posglbd.k $e |- ( ph -> K e. Poset ) $. - posglbd.s $e |- ( ph -> S C_ B ) $. - posglbd.t $e |- ( ph -> T e. B ) $. - posglbd.lb $e |- ( ( ph /\ x e. S ) -> T .<_ x ) $. - posglbd.gt $e |- ( ( ph /\ y e. B /\ A. x e. S y .<_ x ) -> y .<_ T ) $. - $( Properties which determine the greatest lower bound in a poset. - (Contributed by Stefan O'Rear, 31-Jan-2015.) $) - posglbd $p |- ( ph -> ( G ` S ) = T ) $= - ( cfv wcel wbr codu ccnv eqid oduleval cbs odubas eqtrdi cglb club odulub - cpo wceq syl eqtrd odupos cv wa cvv vex brcnvg sylancr adantr mpbird wral - wb w3a brcnv ralbii syl3an3b sylancl 3ad2ant1 poslubdg ) ABCDEFGHUARZIUBZ - VMIHVMUCZJUDADHUERZVMUERKVPVMHVOVPUCUFUGAGHUHRZVMUIRZLAHUKSZVQVRULMVMVQHU - KVOVQUCUJUMUNAVSVMUKSMVMHVOUOUMNOABUPZESZUQVTFVNTZFVTITZPAWBWCVEZWAAVTURS - FDSZWDBUSZOVTFURDIUTVAVBVCACUPZDSZVTWGVNTZBEVDZVFFWGVNTZWGFITZWJAWHWGVTIT - ZBEVDWLWIWMBEVTWGIWFCUSZVGVHQVIAWHWKWLVEZWJAWEWGURSWOOWNFWGDURIUTVJVKVCVL - $. + dlatjmdi.b $e |- B = ( Base ` K ) $. + dlatjmdi.j $e |- .\/ = ( join ` K ) $. + dlatjmdi.m $e |- ./\ = ( meet ` K ) $. + $( In a distributive lattice, joins distribute over meets. (Contributed by + Stefan O'Rear, 30-Jan-2015.) $) + dlatjmdi $p |- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> + ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ ( X .\/ Z ) ) ) $= + ( cdlat wcel codu cfv w3a co wceq eqid odudlatb ibi odujoin odumeet sylan + odubas dlatmjdi ) CKLZCMNZKLZEALFALGALOEFGDPBPEFBPEGBPDPQUFUHUGCKUGRZSTAD + UGBEFGAUGCUIHUDUGDCUIJUAUGBCUIIUBUEUC $. $} @@ -218692,22 +218869,22 @@ net proof size (existence part)? $) ( vx vy cfv wcel wss w3a wceq 3ad2ant1 wa wbr wb ipole syl3anc cmre wne c0 cint cple eqid cbs ipobas cglb a1i cpo ipopos mreintcl intss1 adantl simp2 cv simpl1 adantr sselda mpbird wral simplr simpl2 biimpd ralimdva - simpll1 3impia ssint sylibr simp11 posglbd ) AEUAJZKZBALZBUCUBZMZHIABBU - DZCDDUEJZVSUFZVNVOADUGJNVPADVMFUHOCDUIJNVQGUJDUKKVQADFULUJVNVOVPUPZABEU - MZVQHUQZBKZPZVRWCVSQZVRWCLZWDWGVQWCBUNUOWEVNVRAKZWCAKZWFWGRVNVOVPWDURVQ - WHWDWBUSVQBAWCWAUTADVSVMVRWCFVTSTVAVQIUQZAKZWJWCVSQZHBVBZMZWJVRVSQZWJVR - LZWNWJWCLZHBVBZWPVQWKWMWRVQWKPZWLWQHBWSWDPZWLWQWTVNWKWIWLWQRVNVOVPWKWDV - GVQWKWDVCWSBAWCVNVOVPWKVDUTADVSVMWJWCFVTSTVEVFVHHWJBVIVJWNVNWKWHWOWPRVN - VOVPWKWMVKVQWKWMUPVQWKWHWMWBOADVSVMWJVRFVTSTVAVL $. + simpll1 3impia ssint sylibr simp11 posglbdg ) AEUAJZKZBALZBUCUBZMZHIABB + UDZCDDUEJZVSUFZVNVOADUGJNVPADVMFUHOCDUIJNVQGUJDUKKVQADFULUJVNVOVPUPZABE + UMZVQHUQZBKZPZVRWCVSQZVRWCLZWDWGVQWCBUNUOWEVNVRAKZWCAKZWFWGRVNVOVPWDURV + QWHWDWBUSVQBAWCWAUTADVSVMVRWCFVTSTVAVQIUQZAKZWJWCVSQZHBVBZMZWJVRVSQZWJV + RLZWNWJWCLZHBVBZWPVQWKWMWRVQWKPZWLWQHBWSWDPZWLWQWTVNWKWIWLWQRVNVOVPWKWD + VGVQWKWDVCWSBAWCVNVOVPWKVDUTADVSVMWJWCFVTSTVEVFVHHWJBVIVJWNVNWKWHWOWPRV + NVOVPWKWMVKVQWKWMUPVQWKWHWMWBOADVSVMWJVRFVTSTVAVL $. $( The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) $) mrelatglb0 $p |- ( C e. ( Moore ` X ) -> ( G ` (/) ) = X ) $= ( vx vy cmre cfv wcel c0 cple eqid ipobas cglb a1i wss cv wbr wceq ral0 cpo ipopos 0ss mre1cl rspec adantl wral wa mress wb adantr ipole mpbird - mpd3an3 3adant3 posglbd ) ADIJZKZGHALDBCCMJZVANZACUSEOBCPJUAUTFQCUCKUTA - CEUDQLARUTAUEQADUFZGSZLKDVDVATZUTVEGLVEGUBUGUHUTHSZAKZVFDVATZVFVDVATGLU - IUTVGUJVHVFDRZAVFDUKUTVGDAKZVHVIULUTVJVGVCUMACVAUSVFDEVBUNUPUOUQUR $. + mpd3an3 3adant3 posglbdg ) ADIJZKZGHALDBCCMJZVANZACUSEOBCPJUAUTFQCUCKUT + ACEUDQLARUTAUEQADUFZGSZLKDVDVATZUTVEGLVEGUBUGUHUTHSZAKZVFDVATZVFVDVATGL + UIUTVGUJVHVFDRZAVFDUKUTVGDAKZVHVIULUTVJVGVCUMACVAUSVFDEVBUNUPUOUQUR $. $} ${ @@ -218777,166 +218954,19 @@ net proof size (existence part)? $) $( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - Distributive lattices -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Posets, directed sets, and lattices as relations +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# $) - ${ - latmass.b $e |- B = ( Base ` K ) $. - latmass.m $e |- ./\ = ( meet ` K ) $. - $( Lattice meet is associative. (Contributed by Stefan O'Rear, - 30-Jan-2015.) $) - latmass $p |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> - ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) ) $= - ( clat wcel codu cfv w3a co wceq eqid odulat odubas odujoin latjass sylan - ) BIJBKLZIJDAJEAJFAJMDECNFCNDEFCNCNOUBBUBPZQACUBDEFAUBBUCGRUBCBUCHSTUA $. - $} - - ${ - $d u v w x y z K $. $d u v w x y z B $. $d u v w x y z .\/ $. - $d u v w x y z ./\ $. - latdisd.b $e |- B = ( Base ` K ) $. - latdisd.j $e |- .\/ = ( join ` K ) $. - latdisd.m $e |- ./\ = ( meet ` K ) $. - $( Lemma for ~ latdisd . (Contributed by Stefan O'Rear, 30-Jan-2015.) $) - latdisdlem $p |- ( K e. Lat -> - ( A. u e. B A. v e. B A. w e. B ( u .\/ ( v ./\ w ) ) = - ( ( u .\/ v ) ./\ ( u .\/ w ) ) -> - A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = - ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) ) $= - ( wcel cv co wceq oveq1 oveq2d syl3anc clat wa wi latmcl 3adant3r3 simpr1 - wral w3a simpr3 oveq12d eqeq12d weq oveq2 oveq1d rspc3v imp simpl latjcom - latabs1 eqtrd adantr simpr2 latjcl latmass syl13anc latabs2 3eqtrrd an32s - eqtr3d ralrimivvva ex ) IUANZFOZEOZDOZJPZHPZVMVNHPZVMVOHPZJPZQZDGUGEGUGFG - UGZAOZBOZCOZHPZJPZWCWDJPZWCWEJPZHPZQZCGUGBGUGAGUGVLWBUBWKABCGGGVLWCGNZWDG - NZWEGNZUHZWBWKVLWOUBZWBUBZWJWHWCHPZWHWEHPZJPZWCWEWHHPZJPZWGWPWBWJWTQZWPWH - GNZWLWNWBXCUCVLWLWMXDWNGIJWCWDKMUDUEZVLWLWMWNUFZVLWLWMWNUIZWAXCWHVPHPZWHV - NHPZWHVOHPZJPZQWHWCVOJPZHPZWRXJJPZQFEDWHWCWEGGGVMWHQZVQXHVTXKVMWHVPHRXOVR - XIVSXJJVMWHVNHRVMWHVOHRUJUKEAULZXHXMXKXNXPVPXLWHHVNWCVOJRZSXPXIWRXJJVNWCW - HHUMUNUKDCULZXMWJXNWTXRXLWIWHHVOWEWCJUMSXRXJWSWRJVOWEWHHUMSUKUOTUPWPWTXBQ - WBWPWRWCWSXAJWPWRWCWHHPZWCWPVLXDWLWRXSQVLWOUQZXEXFGHIWHWCKLURTVLWLWMXSWCQ - WNGHIJWCWDKLMUSUEUTWPVLXDWNWSXAQXTXEXGGHIWHWEKLURTUJVAWQXBWCWEWCHPZWEWDHP - ZJPZJPZWGWQXAYCWCJWPWBXAYCQZWPWNWLWMWBYEUCXGXFVLWLWMWNVBZWAYEWEVPHPZWEVNH - PZWEVOHPZJPZQWEXLHPZYAYIJPZQFEDWEWCWDGGGFCULZVQYGVTYJVMWEVPHRYMVRYHVSYIJV - MWEVNHRVMWEVOHRUJUKXPYGYKYJYLXPVPXLWEHXQSXPYHYAYIJVNWCWEHUMUNUKDBULZYKXAY - LYCYNXLWHWEHVOWDWCJUMSYNYIYBYAJVOWDWEHUMSUKUOTUPSWPYDWGQWBWPWCYAJPZYBJPZY - DWGWPVLWLYAGNZYBGNZYPYDQXTXFWPVLWNWLYQXTXGXFGHIWEWCKLVCTWPVLWNWMYRXTXGYFG - HIWEWDKLVCTGIJWCYAYBKMVDVEWPYOWCYBWFJWPYOWCWCWEHPZJPZWCWPYAYSWCJWPVLWNWLY - AYSQXTXGXFGHIWEWCKLURTSWPVLWLWNYTWCQXTXFXGGHIJWCWEKLMVFTUTWPVLWNWMYBWFQXT - XGYFGHIWEWDKLURTUJVIVAUTVGVHVJVK $. - - $( In a lattice, joins distribute over meets if and only if meets - distribute over joins; the distributive property is self-dual. - (Contributed by Stefan O'Rear, 29-Jan-2015.) $) - latdisd $p |- ( K e. Lat -> - ( A. x e. B A. y e. B A. z e. B ( x .\/ ( y ./\ z ) ) = - ( ( x .\/ y ) ./\ ( x .\/ z ) ) <-> - A. x e. B A. y e. B A. z e. B ( x ./\ ( y .\/ z ) ) = - ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) ) $= - ( vu vv vw cv co wceq wral weq oveq1 eqeq12d clat wcel latdisdlem codu wi - cfv eqid odulat odubas odujoin odumeet impbid oveq12d oveq2d oveq2 oveq1d - syl cbvral3vw bitrdi ) FUAUBZANZBNZCNZGOEOVAVBEOVAVCEOGOPCDQBDQADQZKNZLNZ - MNZEOZGOZVEVFGOZVEVGGOZEOZPZMDQLDQKDQZVAVBVCEOZGOZVAVBGOZVAVCGOZEOZPZCDQB - DQADQUTVDVNKLMCBADEFGHIJUCUTFUDUFZUAUBVNVDUEWAFWAUGZUHABCMLKDGWAEDWAFWBHU - IWAGFWBJUJWAEFWBIUKUCUQULVMVTVAVHGOZVAVFGOZVAVGGOZEOZPVAVBVGEOZGOZVQWEEOZ - PKLMABCDDDKARZVIWCVLWFVEVAVHGSWJVJWDVKWEEVEVAVFGSVEVAVGGSUMTLBRZWCWHWFWIW - KVHWGVAGVFVBVGESUNWKWDVQWEEVFVBVAGUOUPTMCRZWHVPWIVSWLWGVOVAGVGVCVBEUOUNWL - WEVRVQEVGVCVAGUOUNTURUS $. - $} - - $c DLat $. - - $( The class of distributive lattices. $) - cdlat $a class DLat $. - - ${ - $d k b j m x y z $. - $( A _distributive lattice_ is a lattice in which meets distribute over - joins, or equivalently ( ~ latdisd ) joins distribute over meets. - (Contributed by Stefan O'Rear, 30-Jan-2015.) $) - df-dlat $a |- DLat = { k e. Lat | [. ( Base ` k ) / b ]. - [. ( join ` k ) / j ]. [. ( meet ` k ) / m ]. A. x e. b A. y e. b - A. z e. b ( x m ( y j z ) ) = ( ( x m y ) j ( x m z ) ) } $. - $} - - ${ - $d k b j m x y z K $. $d k b j m x y z B $. $d k b j m x y z .\/ $. - $d k b j m x y z ./\ $. - isdlat.b $e |- B = ( Base ` K ) $. - isdlat.j $e |- .\/ = ( join ` K ) $. - isdlat.m $e |- ./\ = ( meet ` K ) $. - $( Property of being a distributive lattice. (Contributed by Stefan - O'Rear, 30-Jan-2015.) $) - isdlat $p |- ( K e. DLat <-> ( K e. Lat /\ A. x e. B A. y e. B A. z e. B - ( x ./\ ( y .\/ z ) ) = ( ( x ./\ y ) .\/ ( x ./\ z ) ) ) ) $= - ( vj vm vb cv co wceq wral cmee cfv wsbc cjn cbs clat cdlat fveq2 eqtr4di - vk sbceqbid fvexi wb wa raleq raleqbi1dv simpr eqidd simpl oveqd oveq123d - sbceq1d eqeq12d ralbidv 2ralbidv sylan9bb sbc3ie bitrdi df-dlat elrab2 - 3impb ) ANZBNZCNZKNZOZLNZOZVIVJVNOZVIVKVNOZVLOZPZCMNZQZBVTQZAVTQZLUGNZRSZ - TZKWDUASZTZMWDUBSZTZVIVJVKEOZGOZVIVJGOZVIVKGOZEOZPZCDQZBDQADQZUGFUCUDWDFP - ZWJWCLGTZKETZMDTWRWSWHXAMWIDWSWIFUBSDWDFUBUEHUFWSWFWTKWGEWSWGFUASEWDFUAUE - IUFWSWCLWEGWSWEFRSGWDFRUEJUFUSUHUHWCWRMKLDEGDFUBHUIEFUAIUIGFRJUIVTDPZVLEP - ZVNGPZWCWRUJXBWCVSCDQZBDQZADQXCXDUKZWRWBXFAVTDWAXEBVTDVSCVTDULUMUMXGXEWQA - BDDXGVSWPCDXGVOWLVRWOXGVIVIVMWKVNGXCXDUNZXGVIUOXGVLEVJVKXCXDUPZUQURXGVPWM - VQWNVLEXIXGVNGVIVJXHUQXGVNGVIVKXHUQURUTVAVBVCVHVDVEABCKUGLMVFVG $. - - $d X x y z $. $d Y x y z $. $d Z x y z $. - - $( In a distributive lattice, meets distribute over joins. (Contributed by - Stefan O'Rear, 30-Jan-2015.) $) - dlatmjdi $p |- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> - ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) ) $= - ( vx vy vz wcel cv co wceq wral oveq1 eqeq12d clat isdlat simprbi oveq12d - cdlat w3a oveq2d oveq2 oveq1d rspc3v mpan9 ) CUENZKOZLOZMOZBPZDPZUMUNDPZU - MUODPZBPZQZMARLARKARZEANFANGANUFEFGBPZDPZEFDPZEGDPZBPZQZULCUANVBKLMABCDHI - JUBUCVAVHEUPDPZEUNDPZEUODPZBPZQEFUOBPZDPZVEVKBPZQKLMEFGAAAUMEQZUQVIUTVLUM - EUPDSVPURVJUSVKBUMEUNDSUMEUODSUDTUNFQZVIVNVLVOVQUPVMEDUNFUOBSUGVQVJVEVKBU - NFEDUHUITUOGQZVNVDVOVGVRVMVCEDUOGFBUHUGVRVKVFVEBUOGEDUHUGTUJUK $. - $} - - ${ - $d K x y z $. - $( A distributive lattice is a lattice. (Contributed by Stefan O'Rear, - 30-Jan-2015.) $) - dlatl $p |- ( K e. DLat -> K e. Lat ) $= - ( vx vy vz cdlat wcel clat cjn cfv cmee wceq cbs wral eqid isdlat simplbi - cv co ) AEFAGFBQZCQZDQZAHIZRAJIZRSTUCRSUAUCRUBRKDALIZMCUDMBUDMBCDUDUBAUCU - DNUBNUCNOP $. - $} - - ${ - $d K x y z $. $d D x y z $. $d V x y z $. - odudlat.d $e |- D = ( ODual ` K ) $. - $( The dual of a distributive lattice is a distributive lattice and - conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.) $) - odudlatb $p |- ( K e. V -> ( K e. DLat <-> D e. DLat ) ) $= - ( vx vy vz wcel clat cv cjn cfv co cmee wceq wral wa cdlat eqid isdlat - cbs latdisd bicomd pm5.32i odulatb anbi1d syl5bb odujoin odumeet 3bitr4g - odubas ) BCHZBIHZEJZFJZGJZBKLZMBNLZMUNUOURMUNUPURMUQMOGBUALZPFUSPEUSPZQZA - IHZUNUOUPURMUQMUNUOUQMUNUPUQMURMOGUSPFUSPEUSPZQZBRHARHVAUMVCQULVDUMUTVCUM - VCUTEFGUSUQBURUSSZUQSZURSZUBUCUDULUMVBVCABCDUEUFUGEFGUSUQBURVEVFVGTEFGUSU - RAUQUSABDVEUKAURBDVGUHAUQBDVFUITUJ $. - $} - - ${ - dlatjmdi.b $e |- B = ( Base ` K ) $. - dlatjmdi.j $e |- .\/ = ( join ` K ) $. - dlatjmdi.m $e |- ./\ = ( meet ` K ) $. - $( In a distributive lattice, joins distribute over meets. (Contributed by - Stefan O'Rear, 30-Jan-2015.) $) - dlatjmdi $p |- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> - ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ ( X .\/ Z ) ) ) $= - ( cdlat wcel codu cfv w3a co wceq eqid odudlatb ibi odujoin odumeet sylan - odubas dlatmjdi ) CKLZCMNZKLZEALFALGALOEFGDPBPEFBPEGBPDPQUFUHUGCKUGRZSTAD - UGBEFGAUGCUIHUDUGDCUIJUAUGBCUIIUBUEUC $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Posets and lattices as relations =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + + See commented-out notes for lattices as relations. + $) $c PosetRel $. @@ -779848,13 +779878,13 @@ separated by (open) neighborhoods. See ~ sepnsepo for the equivalence ( vx vy vz wcel cfv wceq cv wbr wral wa cdm cbs wss cple wi cpo glbelss wrex eqid sstrd sseldd adantr sselda glble ralrimiva w3a breq2 3ad2ant1 simp3 rspcdva 3expia breq1 ralbidv imbi2d rspcev syl12anc biid glbeldm2 - anbi12d mpbir2and eqidd cglb a1i posglbd jca ) ACDUAZNZCDOBDOZPAVQCEUBO - ZUCKQZLQZEUDOZRZLCSZMQZWAWBRZLCSZWEVTWBRZUEZMVSSZTZKVSUHZACBVSGAVSBDEWB - UFVSUIZWBUIZHFIUGUJZAVRVSNVRWAWBRZLCSZWGWEVRWBRZUEZMVSSZWLACVSVRWOJUKZA - WPLCAWACNZTVSBDEWBUFWAWMWNHAEUFNXBFULABVPNXBIULACBWAGUMUNZUOAWSMVSAWEVS - NZWGWRAXDWGUPWFWRLCVRWAVRWEWBUQAXDWGUSAXDVRCNWGJURUTZVAUOWKWQWTTKVRVSVT - VRPZWDWQWJWTXFWCWPLCVTVRWAWBVBVCXFWIWSMVSXFWHWRWGVTVRWEWBUQVDVCVIVEVFAW - KKLMVSCDEWBWMWNHWKVGFVHVJALMVSCVRDEWBWNAVSVKDEVLOPAHVMFWOXAXCXEVNVO $. + anbi12d mpbir2and eqidd cglb a1i posglbdg jca ) ACDUAZNZCDOBDOZPAVQCEUB + OZUCKQZLQZEUDOZRZLCSZMQZWAWBRZLCSZWEVTWBRZUEZMVSSZTZKVSUHZACBVSGAVSBDEW + BUFVSUIZWBUIZHFIUGUJZAVRVSNVRWAWBRZLCSZWGWEVRWBRZUEZMVSSZWLACVSVRWOJUKZ + AWPLCAWACNZTVSBDEWBUFWAWMWNHAEUFNXBFULABVPNXBIULACBWAGUMUNZUOAWSMVSAWEV + SNZWGWRAXDWGUPWFWRLCVRWAVRWEWBUQAXDWGUSAXDVRCNWGJURUTZVAUOWKWQWTTKVRVSV + TVRPZWDWQWJWTXFWCWPLCVTVRWAWBVBVCXFWIWSMVSXFWHWRWGVTVRWEWBUQVDVCVIVEVFA + WKKLMVSCDEWBWMWNHWKVGFVHVJALMVSCVRDEWBWNAVSVKDEVLOPAHVMFWOXAXCXEVNVO $. $} $} @@ -780182,20 +780212,20 @@ have GLB (expanded version). (Contributed by Zhi Wang, ipoglb.t $e |- ( ph -> T e. F ) $. $( The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with ` S e. dom G ` .) Could be significantly - shortened if ~ posglbd is in quantified form. ~ mrelatglb could + shortened if ~ posglbdg is in quantified form. ~ mrelatglb could potentially be shortened using this. See ~ mrelatglbALT . (Contributed by Zhi Wang, 29-Sep-2024.) $) ipoglb $p |- ( ph -> ( G ` S ) = T ) $= ( vy vz wcel cv wbr wral vv vw cple cfv eqid cbs wceq ipobas syl ipopos cpo a1i wa breq2 wi cint crab cuni unilbeu biimpar syl2anc wb ipoglblem mpdan mpbid simpld adantr simpr rspcdva ralbidv cbvralvw bitrdi imbi12d - wss breq1 simprd 3impia posglbd ) AUAUBECDFGGUCUDZVSUEZAEHQEGUFUDUGJEGH - IUHUILGUKQAEGIUJULKNAUARZCQZUMDORZVSSZDWAVSSOCWAWCWADVSUNAWDOCTZWBAWEPR - ZWCVSSZOCTZWFDVSSZUOZPETZADCUPZVNWFWLVNWFDVNUOPETUMZWEWKUMZADEQZDBRWLVN - BEUQURUGZWMNMWOWMWPBPWLEDUSUTVAAWOWMWNVBNAOPCEGVSHDIJKVTVCVDVEZVFVGAWBV - HVIAUBRZEQZWRWAVSSZUACTZWRDVSSZAWSUMWJXAXBUOPEWRWFWRUGZWHXAWIXBXCWHWRWC - VSSZOCTXAXCWGXDOCWFWRWCVSVOVJXDWTOUACWCWAWRVSUNVKVLWFWRDVSVOVMAWKWSAWEW - KWQVPVGAWSVHVIVQVR $. + wss breq1 simprd 3impia posglbdg ) AUAUBECDFGGUCUDZVSUEZAEHQEGUFUDUGJEG + HIUHUILGUKQAEGIUJULKNAUARZCQZUMDORZVSSZDWAVSSOCWAWCWADVSUNAWDOCTZWBAWEP + RZWCVSSZOCTZWFDVSSZUOZPETZADCUPZVNWFWLVNWFDVNUOPETUMZWEWKUMZADEQZDBRWLV + NBEUQURUGZWMNMWOWMWPBPWLEDUSUTVAAWOWMWNVBNAOPCEGVSHDIJKVTVCVDVEZVFVGAWB + VHVIAUBRZEQZWRWAVSSZUACTZWRDVSSZAWSUMWJXAXBUOPEWRWFWRUGZWHXAWIXBXCWHWRW + CVSSZOCTXAXCWGXDOCWFWRWCVSVOVJXDWTOUACWCWAWRVSUNVKVLWFWRDVSVOVMAWKWSAWE + WKWQVPVGAWSVHVIVQVR $. $} $}