Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Directed Sets, Nets, Ideals, Filters, and Maps

**by****Grzegorz Bancerek**- Received September 12, 1996
- MML identifier: WAYBEL_0

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, QUANTAL1, RELAT_2, FINSET_1, LATTICE3, BOOLE, SUBSET_1, LATTICES, YELLOW_0, CAT_1, PRE_TOPC, FUNCT_1, RELAT_1, SEQM_3, FUNCOP_1, TARSKI, SETFAM_1, ORDINAL2, FILTER_2, FILTER_0, BHSP_3, REALSET1, WAYBEL_0; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FINSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, REALSET1, PRE_TOPC, LATTICE3, YELLOW_0, ORDERS_1, ORDERS_3; constructors LATTICE3, YELLOW_0, ORDERS_3, MEMBERED, PRE_TOPC; clusters STRUCT_0, FINSET_1, RELSET_1, ORDERS_1, LATTICE3, YELLOW_0, FUNCOP_1, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Directed subsets definition let L be RelStr; let X be Subset of L; attr X is directed means :: WAYBEL_0:def 1 :: Definition 1.1 for x,y being Element of L st x in X & y in X ex z being Element of L st z in X & x <= z & y <= z; attr X is filtered means :: WAYBEL_0:def 2 :: Definition 1.1 for x,y being Element of L st x in X & y in X ex z being Element of L st z in X & z <= x & z <= y; end; :: Original "directed subset" is equivalent to "non empty directed subset" :: in our terminology. It is shown bellow. theorem :: WAYBEL_0:1 for L being non empty transitive RelStr, X being Subset of L holds X is non empty directed iff for Y being finite Subset of X ex x being Element of L st x in X & x is_>=_than Y; :: Original "filtered subset" is equivalent to "non empty filtered subset" :: in our terminology. It is shown bellow. theorem :: WAYBEL_0:2 for L being non empty transitive RelStr, X being Subset of L holds X is non empty filtered iff for Y being finite Subset of X ex x being Element of L st x in X & x is_<=_than Y; definition let L be RelStr; cluster {}L -> directed filtered; end; definition let L be RelStr; cluster directed filtered Subset of L; end; theorem :: WAYBEL_0:3 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 for X1 being Subset of L1, X2 being Subset of L2 st X1 = X2 & X1 is directed holds X2 is directed; theorem :: WAYBEL_0:4 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 for X1 being Subset of L1, X2 being Subset of L2 st X1 = X2 & X1 is filtered holds X2 is filtered; theorem :: WAYBEL_0:5 for L being non empty reflexive RelStr, x being Element of L holds {x} is directed filtered; definition let L be non empty reflexive RelStr; cluster directed filtered non empty finite Subset of L; end; definition let L be with_suprema RelStr; cluster [#]L -> directed; end; definition let L be upper-bounded non empty RelStr; cluster [#]L -> directed; end; definition let L be with_infima RelStr; cluster [#]L -> filtered; end; definition let L be lower-bounded non empty RelStr; cluster [#]L -> filtered; end; definition let L be non empty RelStr; let S be SubRelStr of L; attr S is filtered-infs-inheriting means :: WAYBEL_0:def 3 for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds "/\"(X,L) in the carrier of S; attr S is directed-sups-inheriting means :: WAYBEL_0:def 4 for X being directed Subset of S st X <> {} & ex_sup_of X,L holds "\/"(X,L) in the carrier of S; end; definition let L be non empty RelStr; cluster infs-inheriting -> filtered-infs-inheriting SubRelStr of L; cluster sups-inheriting -> directed-sups-inheriting SubRelStr of L; end; definition let L be non empty RelStr; cluster infs-inheriting sups-inheriting non empty full strict SubRelStr of L; end; theorem :: WAYBEL_0:6 for L being non empty transitive RelStr for S being filtered-infs-inheriting non empty full SubRelStr of L for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds ex_inf_of X,S & "/\"(X,S) = "/\"(X,L); theorem :: WAYBEL_0:7 for L being non empty transitive RelStr for S being directed-sups-inheriting non empty full SubRelStr of L for X being directed Subset of S st X <> {} & ex_sup_of X,L holds ex_sup_of X,S & "\/"(X,S) = "\/"(X,L); begin :: Nets definition let L1,L2 be non empty 1-sorted; let f be map of L1,L2; let x be Element of L1; redefine func f.x -> Element of L2; end; definition let L1,L2 be RelStr; let f be map of L1,L2; attr f is antitone means :: WAYBEL_0:def 5 for x,y being Element of L1 st x <= y for a,b being Element of L2 st a = f.x & b = f.y holds a >= b; end; :: Definition 1.2 definition let L be 1-sorted; struct (RelStr) NetStr over L (# carrier -> set, InternalRel -> (Relation of the carrier), mapping -> Function of the carrier, the carrier of L #); end; definition let L be 1-sorted; let X be non empty set; let O be Relation of X; let F be Function of X, the carrier of L; cluster NetStr(#X,O,F#) -> non empty; end; definition let N be RelStr; attr N is directed means :: WAYBEL_0:def 6 [#]N is directed; end; definition let L be 1-sorted; cluster non empty reflexive transitive antisymmetric directed (strict NetStr over L); end; definition let L be 1-sorted; mode prenet of L is directed non empty NetStr over L; end; definition let L be 1-sorted; mode net of L is transitive prenet of L; end; definition let L be non empty 1-sorted; let N be non empty NetStr over L; func netmap(N,L) -> map of N,L equals :: WAYBEL_0:def 7 the mapping of N; let i be Element of N; func N.i -> Element of L equals :: WAYBEL_0:def 8 (the mapping of N).i; end; definition let L be non empty RelStr; let N be non empty NetStr over L; attr N is monotone means :: WAYBEL_0:def 9 netmap(N,L) is monotone; attr N is antitone means :: WAYBEL_0:def 10 netmap(N,L) is antitone; end; definition let L be non empty 1-sorted; let N be non empty NetStr over L; let X be set; pred N is_eventually_in X means :: WAYBEL_0:def 11 ex i being Element of N st for j being Element of N st i <= j holds N.j in X; pred N is_often_in X means :: WAYBEL_0:def 12 for i being Element of N ex j being Element of N st i <= j & N.j in X; end; theorem :: WAYBEL_0:8 for L being non empty 1-sorted, N being non empty NetStr over L for X,Y being set st X c= Y holds (N is_eventually_in X implies N is_eventually_in Y) & (N is_often_in X implies N is_often_in Y); theorem :: WAYBEL_0:9 for L being non empty 1-sorted, N being non empty NetStr over L for X being set holds N is_eventually_in X iff not N is_often_in (the carrier of L) \ X; theorem :: WAYBEL_0:10 for L being non empty 1-sorted, N being non empty NetStr over L for X being set holds N is_often_in X iff not N is_eventually_in (the carrier of L) \ X; definition let L be non empty RelStr; let N be non empty NetStr over L; attr N is eventually-directed means :: WAYBEL_0:def 13 for i being Element of N holds N is_eventually_in {N.j where j is Element of N: N.i <= N.j}; attr N is eventually-filtered means :: WAYBEL_0:def 14 for i being Element of N holds N is_eventually_in {N.j where j is Element of N: N.i >= N.j}; end; theorem :: WAYBEL_0:11 for L being non empty RelStr, N being non empty NetStr over L holds N is eventually-directed iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N.i <= N.k; theorem :: WAYBEL_0:12 for L being non empty RelStr, N being non empty NetStr over L holds N is eventually-filtered iff for i being Element of N ex j being Element of N st for k being Element of N st j <= k holds N.i >= N.k; definition let L be non empty RelStr; cluster monotone -> eventually-directed prenet of L; cluster antitone -> eventually-filtered prenet of L; end; definition let L be non empty reflexive RelStr; cluster monotone antitone strict prenet of L; end; begin :: Closure by lower elements and finite sups :: Definition 1.3 definition let L be RelStr; let X be Subset of L; func downarrow X -> Subset of L means :: WAYBEL_0:def 15 for x being Element of L holds x in it iff ex y being Element of L st y >= x & y in X; func uparrow X -> Subset of L means :: WAYBEL_0:def 16 for x being Element of L holds x in it iff ex y being Element of L st y <= x & y in X; end; theorem :: WAYBEL_0:13 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 for X being Subset of L1 for Y being Subset of L2 st X = Y holds downarrow X = downarrow Y & uparrow X = uparrow Y; theorem :: WAYBEL_0:14 for L being non empty RelStr, X being Subset of L holds downarrow X = {x where x is Element of L: ex y being Element of L st x <= y & y in X}; theorem :: WAYBEL_0:15 for L being non empty RelStr, X being Subset of L holds uparrow X = {x where x is Element of L: ex y being Element of L st x >= y & y in X}; definition let L be non empty reflexive RelStr; let X be non empty Subset of L; cluster downarrow X -> non empty; cluster uparrow X -> non empty; end; theorem :: WAYBEL_0:16 for L being reflexive RelStr, X being Subset of L holds X c= downarrow X & X c= uparrow X; definition let L be non empty RelStr; let x be Element of L; func downarrow x -> Subset of L equals :: WAYBEL_0:def 17 :: Definition 1.3 (iii) downarrow {x}; func uparrow x -> Subset of L equals :: WAYBEL_0:def 18 :: Definition 1.3 (iv) uparrow {x}; end; theorem :: WAYBEL_0:17 for L being non empty RelStr, x,y being Element of L holds y in downarrow x iff y <= x; theorem :: WAYBEL_0:18 for L being non empty RelStr, x,y being Element of L holds y in uparrow x iff x <= y; theorem :: WAYBEL_0:19 for L being non empty reflexive antisymmetric RelStr for x,y being Element of L st downarrow x = downarrow y holds x = y; theorem :: WAYBEL_0:20 for L being non empty reflexive antisymmetric RelStr for x,y being Element of L st uparrow x = uparrow y holds x = y; theorem :: WAYBEL_0:21 for L being non empty transitive RelStr for x,y being Element of L st x <= y holds downarrow x c= downarrow y; theorem :: WAYBEL_0:22 for L being non empty transitive RelStr for x,y being Element of L st x <= y holds uparrow y c= uparrow x; definition let L be non empty reflexive RelStr; let x be Element of L; cluster downarrow x -> non empty directed; cluster uparrow x -> non empty filtered; end; definition let L be RelStr; let X be Subset of L; attr X is lower means :: WAYBEL_0:def 19 :: Definition 1.3 (v) for x,y being Element of L st x in X & y <= x holds y in X; attr X is upper means :: WAYBEL_0:def 20 :: Definition 1.3 (vi) for x,y being Element of L st x in X & x <= y holds y in X; end; definition let L be RelStr; cluster lower upper Subset of L; end; theorem :: WAYBEL_0:23 for L being RelStr, X being Subset of L holds X is lower iff downarrow X c= X; theorem :: WAYBEL_0:24 for L being RelStr, X being Subset of L holds X is upper iff uparrow X c= X; theorem :: WAYBEL_0:25 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 for X1 being Subset of L1, X2 being Subset of L2 st X1 = X2 holds (X1 is lower implies X2 is lower) & (X1 is upper implies X2 is upper); theorem :: WAYBEL_0:26 for L being RelStr, A being Subset of bool the carrier of L st for X being Subset of L st X in A holds X is lower holds union A is lower Subset of L; theorem :: WAYBEL_0:27 for L being RelStr, X,Y being Subset of L st X is lower & Y is lower holds X /\ Y is lower & X \/ Y is lower; theorem :: WAYBEL_0:28 for L being RelStr, A being Subset of bool the carrier of L st for X being Subset of L st X in A holds X is upper holds union A is upper Subset of L; theorem :: WAYBEL_0:29 for L being RelStr, X,Y being Subset of L st X is upper & Y is upper holds X /\ Y is upper & X \/ Y is upper; definition let L be non empty transitive RelStr; let X be Subset of L; cluster downarrow X -> lower; cluster uparrow X -> upper; end; definition let L be non empty transitive RelStr; let x be Element of L; cluster downarrow x -> lower; cluster uparrow x -> upper; end; definition let L be non empty RelStr; cluster [#]L -> lower upper; end; definition let L be non empty RelStr; cluster non empty lower upper Subset of L; end; definition let L be non empty reflexive transitive RelStr; cluster non empty lower directed Subset of L; cluster non empty upper filtered Subset of L; end; definition let L be with_infima with_suprema Poset; cluster non empty directed filtered lower upper Subset of L; end; theorem :: WAYBEL_0:30 for L being non empty transitive reflexive RelStr, X be Subset of L holds X is directed iff downarrow X is directed; definition let L be non empty transitive reflexive RelStr; let X be directed Subset of L; cluster downarrow X -> directed; end; theorem :: WAYBEL_0:31 for L being non empty transitive reflexive RelStr, X be Subset of L for x be Element of L holds x is_>=_than X iff x is_>=_than downarrow X; theorem :: WAYBEL_0:32 for L being non empty transitive reflexive RelStr, X be Subset of L holds ex_sup_of X,L iff ex_sup_of downarrow X,L; theorem :: WAYBEL_0:33 for L being non empty transitive reflexive RelStr, X be Subset of L st ex_sup_of X,L holds sup X = sup downarrow X; theorem :: WAYBEL_0:34 for L being non empty Poset, x being Element of L holds ex_sup_of downarrow x, L & sup downarrow x = x; theorem :: WAYBEL_0:35 for L being non empty transitive reflexive RelStr, X be Subset of L holds X is filtered iff uparrow X is filtered; definition let L be non empty transitive reflexive RelStr; let X be filtered Subset of L; cluster uparrow X -> filtered; end; theorem :: WAYBEL_0:36 for L being non empty transitive reflexive RelStr, X be Subset of L for x be Element of L holds x is_<=_than X iff x is_<=_than uparrow X; theorem :: WAYBEL_0:37 for L being non empty transitive reflexive RelStr, X be Subset of L holds ex_inf_of X,L iff ex_inf_of uparrow X,L; theorem :: WAYBEL_0:38 for L being non empty transitive reflexive RelStr, X be Subset of L st ex_inf_of X,L holds inf X = inf uparrow X; theorem :: WAYBEL_0:39 for L being non empty Poset, x being Element of L holds ex_inf_of uparrow x, L & inf uparrow x = x; begin :: Ideals and filters definition let L be non empty reflexive transitive RelStr; mode Ideal of L is directed lower non empty Subset of L; :: Definition 1.3 (vii) mode Filter of L is filtered upper non empty Subset of L; :: Definition 1.3 (viii) end; theorem :: WAYBEL_0:40 for L being with_suprema antisymmetric RelStr, X being lower Subset of L holds X is directed iff for x,y being Element of L st x in X & y in X holds x"\/" y in X; theorem :: WAYBEL_0:41 for L being with_infima antisymmetric RelStr, X being upper Subset of L holds X is filtered iff for x,y being Element of L st x in X & y in X holds x"/\" y in X; theorem :: WAYBEL_0:42 for L being with_suprema Poset for X being non empty lower Subset of L holds X is directed iff for Y being finite Subset of X st Y <> {} holds "\/" (Y,L) in X; theorem :: WAYBEL_0:43 for L being with_infima Poset for X being non empty upper Subset of L holds X is filtered iff for Y being finite Subset of X st Y <> {} holds "/\" (Y,L) in X; theorem :: WAYBEL_0:44 for L being non empty antisymmetric RelStr st L is with_suprema or L is with_infima for X,Y being Subset of L st X is lower directed & Y is lower directed holds X /\ Y is directed; theorem :: WAYBEL_0:45 for L being non empty antisymmetric RelStr st L is with_suprema or L is with_infima for X,Y being Subset of L st X is upper filtered & Y is upper filtered holds X /\ Y is filtered; theorem :: WAYBEL_0:46 for L being RelStr, A being Subset of bool the carrier of L st (for X being Subset of L st X in A holds X is directed) & (for X,Y being Subset of L st X in A & Y in A ex Z being Subset of L st Z in A & X \/ Y c= Z) for X being Subset of L st X = union A holds X is directed; theorem :: WAYBEL_0:47 for L being RelStr, A being Subset of bool the carrier of L st (for X being Subset of L st X in A holds X is filtered) & (for X,Y being Subset of L st X in A & Y in A ex Z being Subset of L st Z in A & X \/ Y c= Z) for X being Subset of L st X = union A holds X is filtered; definition let L be non empty reflexive transitive RelStr; let I be Ideal of L; attr I is principal means :: WAYBEL_0:def 21 ex x being Element of L st x in I & x is_>=_than I; end; definition let L be non empty reflexive transitive RelStr; let F be Filter of L; attr F is principal means :: WAYBEL_0:def 22 ex x being Element of L st x in F & x is_<=_than F; end; theorem :: WAYBEL_0:48 for L being non empty reflexive transitive RelStr, I being Ideal of L holds I is principal iff ex x being Element of L st I = downarrow x; theorem :: WAYBEL_0:49 for L being non empty reflexive transitive RelStr, F being Filter of L holds F is principal iff ex x being Element of L st F = uparrow x; definition let L be non empty reflexive transitive RelStr; func Ids L -> set equals :: WAYBEL_0:def 23 :: Definition 1.3 (xi) {X where X is Ideal of L: not contradiction}; func Filt L -> set equals :: WAYBEL_0:def 24 :: Definition 1.3 (xi) {X where X is Filter of L: not contradiction}; end; definition let L be non empty reflexive transitive RelStr; func Ids_0 L -> set equals :: WAYBEL_0:def 25 :: Definition 1.3 (xii) Ids L \/ {{}}; func Filt_0 L -> set equals :: WAYBEL_0:def 26 :: Definition 1.3 (xiii) Filt L \/ {{}}; end; definition let L be non empty RelStr; let X be Subset of L; func finsups X -> Subset of L equals :: WAYBEL_0:def 27 {"\/"(Y,L) where Y is finite Subset of X: ex_sup_of Y,L}; func fininfs X -> Subset of L equals :: WAYBEL_0:def 28 {"/\"(Y,L) where Y is finite Subset of X: ex_inf_of Y,L}; end; definition let L be non empty antisymmetric lower-bounded RelStr; let X be Subset of L; cluster finsups X -> non empty; end; definition let L be non empty antisymmetric upper-bounded RelStr; let X be Subset of L; cluster fininfs X -> non empty; end; definition let L be non empty reflexive antisymmetric RelStr; let X be non empty Subset of L; cluster finsups X -> non empty; cluster fininfs X -> non empty; end; theorem :: WAYBEL_0:50 for L being non empty reflexive antisymmetric RelStr for X being Subset of L holds X c= finsups X & X c= fininfs X; theorem :: WAYBEL_0:51 for L being non empty transitive RelStr for X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F) holds F is directed; definition let L be with_suprema Poset; let X be Subset of L; cluster finsups X -> directed; end; theorem :: WAYBEL_0:52 for L being non empty transitive reflexive RelStr, X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F) for x being Element of L holds x is_>=_than X iff x is_>=_than F; theorem :: WAYBEL_0:53 for L being non empty transitive reflexive RelStr, X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F) holds ex_sup_of X,L iff ex_sup_of F,L; theorem :: WAYBEL_0:54 for L being non empty transitive reflexive RelStr, X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_sup_of Y,L & x = "\/"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F) & ex_sup_of X,L holds sup F = sup X; theorem :: WAYBEL_0:55 for L being with_suprema Poset, X being Subset of L st ex_sup_of X,L or L is complete holds sup X = sup finsups X; theorem :: WAYBEL_0:56 for L being non empty transitive RelStr for X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F) holds F is filtered; definition let L be with_infima Poset; let X be Subset of L; cluster fininfs X -> filtered; end; theorem :: WAYBEL_0:57 for L being non empty transitive reflexive RelStr, X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F) for x being Element of L holds x is_<=_than X iff x is_<=_than F; theorem :: WAYBEL_0:58 for L being non empty transitive reflexive RelStr, X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F) holds ex_inf_of X,L iff ex_inf_of F,L; theorem :: WAYBEL_0:59 for L being non empty transitive reflexive RelStr, X,F being Subset of L st (for Y being finite Subset of X st Y <> {} holds ex_inf_of Y,L) & (for x being Element of L st x in F ex Y being finite Subset of X st ex_inf_of Y,L & x = "/\"(Y,L)) & (for Y being finite Subset of X st Y <> {} holds "/\"(Y,L) in F) & ex_inf_of X, L holds inf F = inf X; theorem :: WAYBEL_0:60 for L being with_infima Poset, X being Subset of L st ex_inf_of X,L or L is complete holds inf X = inf fininfs X; theorem :: WAYBEL_0:61 for L being with_suprema Poset, X being Subset of L holds X c= downarrow finsups X & for I being Ideal of L st X c= I holds downarrow finsups X c= I; theorem :: WAYBEL_0:62 for L being with_infima Poset, X being Subset of L holds X c= uparrow fininfs X & for F being Filter of L st X c= F holds uparrow fininfs X c= F; begin :: Chains definition let L be non empty RelStr; attr L is connected means :: WAYBEL_0:def 29 for x,y being Element of L holds x <= y or y <= x; end; definition cluster trivial -> connected (non empty reflexive RelStr); end; definition cluster connected (non empty Poset); end; definition mode Chain is connected (non empty Poset); end; definition let L be Chain; cluster L~ -> connected; end; begin :: Semilattices definition mode Semilattice is with_infima Poset; mode sup-Semilattice is with_suprema Poset; mode LATTICE is with_infima with_suprema Poset; end; theorem :: WAYBEL_0:63 for L being Semilattice for X being upper non empty Subset of L holds X is Filter of L iff subrelstr X is meet-inheriting; theorem :: WAYBEL_0:64 for L being sup-Semilattice for X being lower non empty Subset of L holds X is Ideal of L iff subrelstr X is join-inheriting; begin :: Maps definition let S,T be non empty RelStr; let f be map of S,T; let X be Subset of S; pred f preserves_inf_of X means :: WAYBEL_0:def 30 ex_inf_of X,S implies ex_inf_of f.:X,T & inf (f.:X) = f.inf X; pred f preserves_sup_of X means :: WAYBEL_0:def 31 ex_sup_of X,S implies ex_sup_of f.:X,T & sup (f.:X) = f.sup X; end; theorem :: WAYBEL_0:65 for S1,S2, T1,T2 being non empty RelStr st the RelStr of S1 = the RelStr of T1 & the RelStr of S2 = the RelStr of T2 for f being map of S1,S2, g being map of T1,T2 st f = g for X being Subset of S1, Y being Subset of T1 st X = Y holds (f preserves_sup_of X implies g preserves_sup_of Y) & (f preserves_inf_of X implies g preserves_inf_of Y); definition let L1,L2 be non empty RelStr; let f be map of L1,L2; attr f is infs-preserving means :: WAYBEL_0:def 32 for X being Subset of L1 holds f preserves_inf_of X; attr f is sups-preserving means :: WAYBEL_0:def 33 for X being Subset of L1 holds f preserves_sup_of X; attr f is meet-preserving means :: WAYBEL_0:def 34 for x,y being Element of L1 holds f preserves_inf_of {x,y}; attr f is join-preserving means :: WAYBEL_0:def 35 for x,y being Element of L1 holds f preserves_sup_of {x,y}; attr f is filtered-infs-preserving means :: WAYBEL_0:def 36 for X being Subset of L1 st X is non empty filtered holds f preserves_inf_of X; attr f is directed-sups-preserving means :: WAYBEL_0:def 37 for X being Subset of L1 st X is non empty directed holds f preserves_sup_of X; end; definition let L1,L2 be non empty RelStr; cluster infs-preserving -> filtered-infs-preserving meet-preserving map of L1,L2; cluster sups-preserving -> directed-sups-preserving join-preserving map of L1,L2; end; definition let S,T be RelStr; let f be map of S,T; attr f is isomorphic means :: WAYBEL_0:def 38 f is one-to-one monotone & ex g being map of T,S st g = f" & g is monotone if S is non empty & T is non empty otherwise S is empty & T is empty; end; theorem :: WAYBEL_0:66 for S,T being non empty RelStr, f being map of S,T holds f is isomorphic iff f is one-to-one & rng f = the carrier of T & for x,y being Element of S holds x <= y iff f.x <= f.y; definition let S,T be non empty RelStr; cluster isomorphic -> one-to-one monotone map of S,T; end; theorem :: WAYBEL_0:67 for S,T being non empty RelStr, f being map of S,T st f is isomorphic holds f" is map of T,S & rng (f") = the carrier of S; theorem :: WAYBEL_0:68 for S,T being non empty RelStr, f being map of S,T st f is isomorphic for g being map of T,S st g = f" holds g is isomorphic; theorem :: WAYBEL_0:69 for S,T being non empty Poset, f being map of S,T st for X being Filter of S holds f preserves_inf_of X holds f is monotone; theorem :: WAYBEL_0:70 for S,T being non empty Poset, f being map of S,T st for X being Filter of S holds f preserves_inf_of X holds f is filtered-infs-preserving; theorem :: WAYBEL_0:71 for S being Semilattice, T being non empty Poset, f being map of S,T st (for X being finite Subset of S holds f preserves_inf_of X) & (for X being non empty filtered Subset of S holds f preserves_inf_of X) holds f is infs-preserving; theorem :: WAYBEL_0:72 for S,T being non empty Poset, f being map of S,T st for X being Ideal of S holds f preserves_sup_of X holds f is monotone; theorem :: WAYBEL_0:73 for S,T being non empty Poset, f being map of S,T st for X being Ideal of S holds f preserves_sup_of X holds f is directed-sups-preserving; theorem :: WAYBEL_0:74 for S being sup-Semilattice, T being non empty Poset, f being map of S,T st (for X being finite Subset of S holds f preserves_sup_of X) & (for X being non empty directed Subset of S holds f preserves_sup_of X) holds f is sups-preserving; begin :: Complete Semilattice definition let L be non empty reflexive RelStr; attr L is up-complete means :: WAYBEL_0:def 39 for X being non empty directed Subset of L ex x being Element of L st x is_>=_than X & for y being Element of L st y is_>=_than X holds x <= y; end; definition cluster up-complete -> upper-bounded (with_suprema reflexive RelStr); end; theorem :: WAYBEL_0:75 for L being non empty reflexive antisymmetric RelStr holds L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L; definition let L be non empty reflexive RelStr; attr L is /\-complete means :: WAYBEL_0:def 40 for X being non empty Subset of L ex x being Element of L st x is_<=_than X & for y being Element of L st y is_<=_than X holds x >= y; end; theorem :: WAYBEL_0:76 for L being non empty reflexive antisymmetric RelStr holds L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L; definition cluster complete -> up-complete /\-complete (non empty reflexive RelStr); cluster /\-complete -> lower-bounded (non empty reflexive RelStr); cluster up-complete with_suprema lower-bounded -> complete (non empty Poset); :: cluster up-complete /\-complete upper-bounded -> complete (non empty Poset); :: to appear in YELLOW_2 end; definition cluster /\-complete -> with_infima (non empty reflexive antisymmetric RelStr); end; definition cluster /\-complete -> with_suprema (non empty reflexive antisymmetric upper-bounded RelStr); end; definition cluster complete strict LATTICE; end;

Back to top