:: Properties of Relational Structures, Posets, Lattices and Maps :: by Mariusz \.Zynel and Czes{\l}aw Byli\'nski :: :: Received September 20, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, ORDERS_2, SUBSET_1, TARSKI, WAYBEL_0, LATTICE3, XXREAL_0, RELAT_2, YELLOW_0, EQREL_1, LATTICES, RELAT_1, WELLORD1, CAT_1, STRUCT_0, FUNCT_1, GROUP_6, SEQM_3, ORDINAL2, BINOP_1, REWRITE1, SETFAM_1, CARD_FIL, YELLOW_1, ZFMISC_1, WELLORD2, YELLOW_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, LATTICE3, WELLORD1, DOMAIN_1, ORDERS_1, STRUCT_0, ORDERS_2, QUANTAL1, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0; constructors SETFAM_1, DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_0, YELLOW_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1; requirements SUBSET, BOOLE; begin :: Basic Facts reserve x, X, Y for set; theorem :: YELLOW_2:1 for L being non empty RelStr for x being Element of L for X being Subset of L holds X c= downarrow x iff X is_<=_than x; theorem :: YELLOW_2:2 for L being non empty RelStr for x being Element of L for X being Subset of L holds X c= uparrow x iff x is_<=_than X; theorem :: YELLOW_2:3 for L being antisymmetric transitive with_suprema RelStr for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L holds ex_sup_of (X \/ Y),L & "\/"(X \/ Y, L) = "\/"(X, L) "\/" "\/"(Y, L); theorem :: YELLOW_2:4 for L being antisymmetric transitive with_infima RelStr for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L holds ex_inf_of (X \/ Y),L & "/\"(X \/ Y, L) = "/\"(X, L) "/\" "/\"(Y, L); begin :: Relational Substructures theorem :: YELLOW_2:5 for R being Relation for X, Y being set holds X c= Y implies R |_2 X c= R |_2 Y; theorem :: YELLOW_2:6 for L being RelStr for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds the InternalRel of S c= the InternalRel of T; theorem :: YELLOW_2:7 for L being non empty RelStr for S being non empty SubRelStr of L holds (X is directed Subset of S implies X is directed Subset of L) & (X is filtered Subset of S implies X is filtered Subset of L); theorem :: YELLOW_2:8 for L being non empty RelStr for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T for X being Subset of S holds X is Subset of T & for Y being Subset of T st X = Y holds (X is filtered implies Y is filtered) & (X is directed implies Y is directed); begin :: Maps definition let J be set, L be RelStr; let f, g be Function of J, the carrier of L; pred f <= g means :: YELLOW_2:def 1 for j being set st j in J ex a, b being Element of L st a = f.j & b = g.j & a <= b; end; notation let J be set, L be RelStr; let f, g be Function of J, the carrier of L; synonym g >= f for f <= g; end; theorem :: YELLOW_2:9 for L, M being non empty RelStr, f,g being Function of L, M holds f <= g iff for x being Element of L holds f.x <= g.x; begin :: The Image of a Map definition let L, M be non empty RelStr; let f be Function of L, M; func Image f -> strict full SubRelStr of M equals :: YELLOW_2:def 2 subrelstr rng f; end; theorem :: YELLOW_2:10 for L, M being non empty RelStr for f being Function of L, M for y being Element of Image f ex x being Element of L st f.x = y; registration let L be non empty RelStr; let X be non empty Subset of L; cluster subrelstr X -> non empty; end; registration let L, M be non empty RelStr; let f be Function of L, M; cluster Image f -> non empty; end; begin :: Monotone Maps theorem :: YELLOW_2:11 for L being non empty RelStr holds id L is monotone; theorem :: YELLOW_2:12 for L, M, N being non empty RelStr for f being Function of L, M, g being Function of M, N holds f is monotone & g is monotone implies g*f is monotone; theorem :: YELLOW_2:13 for L, M being non empty RelStr for f being Function of L, M for X being Subset of L, x being Element of L holds f is monotone & x is_<=_than X implies f.x is_<=_than f.:X; theorem :: YELLOW_2:14 for L, M being non empty RelStr for f being Function of L, M for X being Subset of L, x being Element of L holds f is monotone & X is_<=_than x implies f.:X is_<=_than f.x; theorem :: YELLOW_2:15 for S, T being non empty RelStr for f being Function of S, T for X being directed Subset of S holds f is monotone implies f.:X is directed; theorem :: YELLOW_2:16 for L being with_suprema Poset for f being Function of L, L holds f is directed-sups-preserving implies f is monotone; theorem :: YELLOW_2:17 for L being with_infima Poset for f being Function of L, L holds f is filtered-infs-preserving implies f is monotone; begin :: Idempotent Maps theorem :: YELLOW_2:18 for S being non empty 1-sorted for f being Function of S, S holds f is idempotent implies for x being Element of S holds f.(f.x) = f.x; theorem :: YELLOW_2:19 for S being non empty 1-sorted for f being Function of S, S holds f is idempotent implies rng f = {x where x is Element of S: x = f.x}; theorem :: YELLOW_2:20 for S being non empty 1-sorted for f being Function of S, S st f is idempotent holds X c= rng f implies f.:X = X; theorem :: YELLOW_2:21 for L being non empty RelStr holds id L is idempotent; begin :: Complete Lattices (CCL Chapter 0, Section 2, pp. 8 -- 9) reserve L for complete LATTICE, a for Element of L; theorem :: YELLOW_2:22 a in X implies a <= "\/"(X, L) & "/\"(X, L) <= a; theorem :: YELLOW_2:23 for L being non empty RelStr holds (for X holds ex_sup_of X,L) iff (for Y holds ex_inf_of Y,L); theorem :: YELLOW_2:24 ::Proposition 2.2 (i) (variant 1) cf YELLOW_0 for L being non empty RelStr holds (for X holds ex_sup_of X,L) implies L is complete; theorem :: YELLOW_2:25 ::Proposition 2.2 (i) (variant 2) cf variant 3 for L being non empty RelStr holds (for X holds ex_inf_of X,L) implies L is complete; theorem :: YELLOW_2:26 for L being non empty RelStr holds (for A being Subset of L holds ex_inf_of A, L) implies for X holds ex_inf_of X,L & "/\"(X, L) = "/\"(X /\ the carrier of L, L); theorem :: YELLOW_2:27 for L being non empty RelStr holds (for A being Subset of L holds ex_sup_of A, L) implies for X holds ex_sup_of X,L & "\/"(X, L) = "\/"(X /\ the carrier of L, L); theorem :: YELLOW_2:28 ::Proposition 2.2 (i) (variant 3) for L being non empty RelStr holds (for A being Subset of L holds ex_inf_of A,L) implies L is complete; registration cluster up-complete /\-complete upper-bounded -> complete for non empty Poset; end; theorem :: YELLOW_2:29 :: Theorem 2.3 (The Fixed-Point Theorem) for f being Function of L, L st f is monotone for M being Subset of L st M = {x where x is Element of L: x = f.x} holds subrelstr M is complete LATTICE; theorem :: YELLOW_2:30 for S being infs-inheriting non empty full SubRelStr of L holds S is complete LATTICE; theorem :: YELLOW_2:31 for S being sups-inheriting non empty full SubRelStr of L holds S is complete LATTICE; theorem :: YELLOW_2:32 ::Remark 2.4 (Part I, variant 1) for M being non empty RelStr for f being Function of L, M st f is sups-preserving holds Image f is sups-inheriting; theorem :: YELLOW_2:33 ::Remark 2.4 (Part I, variant 2) for M being non empty RelStr for f being Function of L, M st f is infs-preserving holds Image f is infs-inheriting; theorem :: YELLOW_2:34 ::Remark 2.4 (Part II) for L, M being complete LATTICE for f being Function of L, M st f is sups-preserving or f is infs-preserving holds Image f is complete LATTICE; theorem :: YELLOW_2:35 ::Remark 2.5 for f being Function of L, L st f is idempotent directed-sups-preserving holds Image f is directed-sups-inheriting & Image f is complete LATTICE; begin :: A Lattice of Ideals theorem :: YELLOW_2:36 for L being RelStr for F being Subset-Family of L st for X being Subset of L st X in F holds X is lower holds meet F is lower Subset of L; theorem :: YELLOW_2:37 for L being RelStr for F being Subset-Family of L st for X being Subset of L st X in F holds X is upper holds meet F is upper Subset of L; theorem :: YELLOW_2:38 for L being with_suprema antisymmetric RelStr for F being Subset-Family of L st for X being Subset of L st X in F holds X is lower directed holds meet F is directed Subset of L; theorem :: YELLOW_2:39 for L being with_infima antisymmetric RelStr for F being Subset-Family of L st for X being Subset of L st X in F holds X is upper filtered holds meet F is filtered Subset of L; theorem :: YELLOW_2:40 for L being with_infima Poset for I, J being Ideal of L holds I /\ J is Ideal of L; registration let L be non empty reflexive transitive RelStr; cluster Ids L -> non empty; end; theorem :: YELLOW_2:41 for L being non empty reflexive transitive RelStr holds (x is Element of InclPoset(Ids L) iff x is Ideal of L); theorem :: YELLOW_2:42 for L being non empty reflexive transitive RelStr for I being Element of InclPoset(Ids L) holds x in I implies x is Element of L; theorem :: YELLOW_2:43 for L being with_infima Poset for x, y being Element of InclPoset(Ids L) holds x "/\" y = x /\ y; registration let L be with_infima Poset; cluster InclPoset(Ids L) -> with_infima; end; theorem :: YELLOW_2:44 for L being with_suprema Poset for x, y being Element of InclPoset(Ids L) holds ex Z being Subset of L st Z = {z where z is Element of L : z in x or z in y or ex a, b being Element of L st a in x & b in y & z = a "\/" b} & ex_sup_of {x, y},InclPoset(Ids L) & x "\/" y = downarrow Z; registration let L be with_suprema Poset; cluster InclPoset(Ids L) -> with_suprema; end; theorem :: YELLOW_2:45 for L being lower-bounded sup-Semilattice for X being non empty Subset of Ids L holds meet X is Ideal of L; theorem :: YELLOW_2:46 for L being lower-bounded sup-Semilattice for A being non empty Subset of InclPoset(Ids L) holds ex_inf_of A,InclPoset(Ids L) & inf A = meet A; theorem :: YELLOW_2:47 for L being with_suprema Poset holds ex_inf_of {},InclPoset(Ids L) & "/\"({}, InclPoset(Ids L)) = [#]L; theorem :: YELLOW_2:48 for L being lower-bounded sup-Semilattice holds InclPoset(Ids L) is complete; registration let L be lower-bounded sup-Semilattice; cluster InclPoset(Ids L) -> complete; end; begin :: Special Maps definition let L be non empty Poset; func SupMap L -> Function of InclPoset(Ids L), L means :: YELLOW_2:def 3 for I being Ideal of L holds it.I = sup I; end; theorem :: YELLOW_2:49 for L being non empty Poset holds dom SupMap L = Ids L & rng SupMap L is Subset of L; theorem :: YELLOW_2:50 for L being non empty Poset holds x in dom SupMap L iff x is Ideal of L; theorem :: YELLOW_2:51 for L being up-complete non empty Poset holds SupMap L is monotone; registration let L be up-complete non empty Poset; cluster SupMap L -> monotone; end; definition let L be non empty Poset; func IdsMap L -> Function of L, InclPoset(Ids L) means :: YELLOW_2:def 4 for x being Element of L holds it.x = downarrow x; end; theorem :: YELLOW_2:52 for L being non empty Poset holds IdsMap L is monotone; registration let L be non empty Poset; cluster IdsMap L -> monotone; end; begin :: A Family of Elements in a Lattice definition let L be non empty RelStr; let F be Relation; func \\/(F, L) -> Element of L equals :: YELLOW_2:def 5 "\/"(rng F, L); func //\(F, L) -> Element of L equals :: YELLOW_2:def 6 "/\"(rng F, L); end; notation let J be set, L be non empty RelStr; let F be Function of J, the carrier of L; synonym Sup F for \\/(F, L); synonym Inf F for //\(F, L); end; reserve J for non empty set, j for Element of J; theorem :: YELLOW_2:53 for F being Function of J, the carrier of L holds F.j <= Sup F & Inf F <= F.j ; theorem :: YELLOW_2:54 for F being Function of J, the carrier of L holds (for j holds F.j <= a) implies Sup F <= a; theorem :: YELLOW_2:55 for F being Function of J, the carrier of L holds (for j holds a <= F. j) implies a <= Inf F;