Copyright (c) 1996 Association of Mizar Users
environ vocabulary ORDERS_1, WAYBEL_0, LATTICE3, RELAT_2, YELLOW_0, BOOLE, LATTICES, RELAT_1, WELLORD1, CAT_1, QUANTAL1, PRE_TOPC, FUNCT_1, GROUP_6, SEQM_3, ORDINAL2, BINOP_1, BHSP_3, SETFAM_1, FILTER_2, YELLOW_1, SUBSET_1, WELLORD2, YELLOW_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, LATTICE3, WELLORD1, STRUCT_0, ORDERS_1, PRE_TOPC, QUANTAL1, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0, GRCAT_1; constructors WAYBEL_0, YELLOW_1, TOLER_1, ORDERS_3, QUANTAL1, TOPS_2, GRCAT_1; clusters STRUCT_0, LATTICE3, RELSET_1, YELLOW_0, YELLOW_1, WAYBEL_0, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, LATTICE3, QUANTAL1, ORDERS_3, WAYBEL_0; theorems TARSKI, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, LATTICE3, WELLORD1, ORDERS_1, PRE_TOPC, TMAP_1, ORDERS_3, YELLOW_0, YELLOW_1, WAYBEL_0, GRCAT_1, RELSET_1, XBOOLE_0, XBOOLE_1; schemes FUNCT_2, SUPINF_2; begin :: Basic Facts reserve x, X, Y for set; scheme RelStrSubset{L() -> non empty RelStr, P[set]}: {x where x is Element of L(): P[x]} is Subset of L() proof {x where x is Element of L(): P[x]} c= the carrier of L() proof let x be set; assume x in {l where l is Element of L(): P[l]}; then ex l being Element of L() st x = l & P[l]; hence thesis; end; hence thesis; end; theorem 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 proof let L be non empty RelStr, x be Element of L, X be Subset of L; hereby assume A1: X c= downarrow x; thus X is_<=_than x proof let a be Element of L; assume a in X; hence a <= x by A1,WAYBEL_0:17; end; end; assume A2: for a being Element of L st a in X holds a <= x; let a be set; assume A3: a in X; then reconsider a as Element of L; a <= x by A2,A3; hence thesis by WAYBEL_0:17; end; theorem 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 proof let L be non empty RelStr, x be Element of L, X be Subset of L; hereby assume A1: X c= uparrow x; thus x is_<=_than X proof let a be Element of L; assume a in X; hence x <= a by A1,WAYBEL_0:18; end; end; assume A2: for a being Element of L st a in X holds x <= a; let a be set; assume A3: a in X; then reconsider a as Element of L; x <= a by A2,A3; hence thesis by WAYBEL_0:18; end; theorem 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) proof let L be antisymmetric transitive with_suprema RelStr; let X, Y be set such that A1: ex_sup_of X,L and A2: ex_sup_of Y,L; set a = "\/"(X, L) "\/" "\/"(Y, L); A3: X \/ Y is_<=_than a proof let x be Element of L; assume A4: x in X \/ Y; per cases by A4,XBOOLE_0:def 2; suppose A5: x in X; X is_<=_than "\/"(X, L) by A1,YELLOW_0:30; then x <= "\/"(X, L) & "\/"(X, L) <= a by A5,LATTICE3:def 9,YELLOW_0:22; hence x <= a by ORDERS_1:26; suppose A6: x in Y; Y is_<=_than "\/"(Y, L) by A2,YELLOW_0:30; then x <= "\/"(Y, L) & "\/"(Y, L) <= a by A6,LATTICE3:def 9,YELLOW_0:22; hence x <= a by ORDERS_1:26; end; for b being Element of L st X \/ Y is_<=_than b holds a <= b proof let b be Element of L; assume A7: X \/ Y is_<=_than b; X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7; then X is_<=_than b & Y is_<=_than b by A7,YELLOW_0:9; then "\/"(X, L) <= b & "\/"(Y, L) <= b by A1,A2,YELLOW_0:30; hence a <= b by YELLOW_0:22; end; hence thesis by A3,YELLOW_0:30; end; theorem 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) proof let L be antisymmetric transitive with_infima RelStr; let X, Y be set such that A1: ex_inf_of X,L and A2: ex_inf_of Y,L; set a = "/\"(X, L) "/\" "/\"(Y, L); A3: X \/ Y is_>=_than a proof let x be Element of L; assume A4: x in X \/ Y; per cases by A4,XBOOLE_0:def 2; suppose A5: x in X; X is_>=_than "/\"(X, L) by A1,YELLOW_0:31; then x >= "/\"(X, L) & "/\"(X, L) >= a by A5,LATTICE3:def 8,YELLOW_0:23; hence x >= a by ORDERS_1:26; suppose A6: x in Y; Y is_>=_than "/\"(Y, L) by A2,YELLOW_0:31; then x >= "/\"(Y, L) & "/\"(Y, L) >= a by A6,LATTICE3:def 8,YELLOW_0:23; hence x >= a by ORDERS_1:26; end; for b being Element of L st X \/ Y is_>=_than b holds a >= b proof let b be Element of L; assume A7: X \/ Y is_>=_than b; X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7; then X is_>=_than b & Y is_>=_than b by A7,YELLOW_0:9; then "/\"(X, L) >= b & "/\"(Y, L) >= b by A1,A2,YELLOW_0:31; hence a >= b by YELLOW_0:23; end; hence thesis by A3,YELLOW_0:31; end; begin :: Relational Substructures theorem Th5: for R being Relation for X, Y being set holds X c= Y implies R |_2 X c= R |_2 Y proof let R be Relation, X,Y be set; assume A1: X c= Y; then X|R c= Y|R by RELAT_1:131; then A2: X|R|X c= Y|R|X by RELAT_1:105; Y|R|X c= Y|R|Y by A1,RELAT_1:104; then X|R|X c= Y|R|Y by A2,XBOOLE_1:1; then R|_2 X c= Y|R|Y by WELLORD1:17; hence R|_2 X c= R|_2 Y by WELLORD1:17; end; theorem 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 proof let L be RelStr, S1,S2 be full SubRelStr of L; the InternalRel of S1 = (the InternalRel of L)|_2 the carrier of S1 & the InternalRel of S2 = (the InternalRel of L)|_2 the carrier of S2 by YELLOW_0:def 14; hence thesis by Th5; end; theorem Th7: 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) proof let L be non empty RelStr; let S be non empty SubRelStr of L; thus X is directed Subset of S implies X is directed Subset of L proof assume A1: X is directed Subset of S; the carrier of S c= the carrier of L by YELLOW_0:def 13; then X c= the carrier of L by A1,XBOOLE_1:1; then reconsider X as Subset of L; 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 proof let x, y be Element of L; assume A2: x in X & y in X; then reconsider x'= x, y'= y as Element of S by A1; consider z being Element of S such that A3: z in X and A4: x' <= z & y' <= z by A1,A2,WAYBEL_0:def 1; reconsider z as Element of L by YELLOW_0:59; take z; thus thesis by A3,A4,YELLOW_0:60; end; hence thesis by WAYBEL_0:def 1; end; thus X is filtered Subset of S implies X is filtered Subset of L proof assume A5: X is filtered Subset of S; the carrier of S c= the carrier of L by YELLOW_0:def 13; then X c= the carrier of L by A5,XBOOLE_1:1; then reconsider X as Subset of L; 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 proof let x, y be Element of L; assume A6: x in X & y in X; then reconsider x'= x, y'= y as Element of S by A5; consider z being Element of S such that A7: z in X and A8: z <= x' & z <= y' by A5,A6,WAYBEL_0:def 2; reconsider z as Element of L by YELLOW_0:59; take z; thus thesis by A7,A8,YELLOW_0:60; end; hence thesis by WAYBEL_0:def 2; end; end; theorem 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) proof let L be non empty RelStr, S1,S2 be non empty full SubRelStr of L; assume A1: the carrier of S1 c= the carrier of S2; let X be Subset of S1; X is Subset of S2 by A1,XBOOLE_1:1; hence X is Subset of S2; let X2 be Subset of S2 such that A2: X = X2; hereby assume A3: X is filtered; thus X2 is filtered proof let x, y be Element of S2; assume A4: x in X2 & y in X2; then reconsider x'= x, y'= y as Element of S1 by A2; consider z being Element of S1 such that A5: z in X & z <= x' & z <= y' by A2,A3,A4,WAYBEL_0:def 2; reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:59; reconsider z as Element of S2 by A2,A5; take z; z1 <= x1 & z1 <= y1 by A5,YELLOW_0:60; hence z in X2 & z <= x & z <= y by A2,A5,YELLOW_0:61; end; end; assume A6: X is directed; let x, y be Element of S2; assume A7: x in X2 & y in X2; then reconsider x'= x, y'= y as Element of S1 by A2; consider z being Element of S1 such that A8: z in X & x' <= z & y' <= z by A2,A6,A7,WAYBEL_0:def 1; reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:59; reconsider z as Element of S2 by A2,A8; take z; x1 <= z1 & y1 <= z1 by A8,YELLOW_0:60; hence z in X2 & x <= z & y <= z by A2,A8,YELLOW_0:61; end; begin :: Maps scheme LambdaMD{X, Y() -> non empty RelStr, F(set) -> Element of Y()}: ex f being map of X(), Y() st for x being Element of X() holds f.x = F(x) proof deffunc f(set) = F($1); consider f being Function of the carrier of X(),the carrier of Y() such that A1: for s being Element of X() holds f.s = f(s) from LambdaD; reconsider f as map of X(),Y(); take f; thus thesis by A1; end; scheme KappaMD{X, Y() -> non empty RelStr, F(set) -> set}: ex f being map of X(), Y() st for x being Element of X() holds f.x = F(x) provided A1: for x being Element of X() holds F(x) is Element of Y() proof reconsider X = the carrier of X(),Y = the carrier of Y() as non empty set; deffunc f(set) = F($1); A2: now let x be Element of X; F(x) is Element of Y() by A1; hence f(x) in Y; end; consider f being Function of X, Y such that A3: for x being Element of X holds f.x = f(x) from FunctR_ealEx(A2); reconsider f as map of X(),Y(); take f; thus thesis by A3; end; scheme NonUniqExMD{X, Y() -> non empty RelStr, P[set,set]}: ex f being map of X(), Y() st for x being Element of X() holds P[x, f.x] provided A1: for x being Element of X() ex y being Element of Y() st P[x, y] proof defpred p[set,set] means P[$1,$2]; A2: for x being set st x in the carrier of X() ex y being set st y in the carrier of Y() & p[x,y] proof let x be set; assume x in the carrier of X(); then reconsider x as Element of X(); ex y being Element of Y() st p[x,y] by A1; hence thesis; end; consider f being Function of the carrier of X(),the carrier of Y() such that A3: for x being set st x in the carrier of X() holds p[x,f.x] from FuncEx1(A2); reconsider f as map of X(),Y(); take f; thus thesis by A3; end; definition let S, T be 1-sorted; let f be map of S, T; redefine func rng f -> Subset of T; coherence by RELSET_1:12; end; theorem Th9: for S, T being non empty 1-sorted for f, g being map of S, T holds (for s being Element of S holds f.s = g.s) implies f = g by FUNCT_2:113; definition let J be set, L be RelStr; let f, g be Function of J, the carrier of L; pred f <= g means :Def1: for j being set st j in J ex a, b being Element of L st a = f.j & b = g.j & a <= b; synonym g >= f; end; theorem for L, M being non empty RelStr, f,g being map of L, M holds f <= g iff for x being Element of L holds f.x <= g.x proof let L, M be non empty RelStr, f,g be map of L, M; hereby assume A1: f <= g; let x be Element of L; ex m1,m2 being Element of M st m1 = f.x & m2 = g.x & m1 <= m2 by A1,Def1; hence f.x <= g.x; end; assume A2: for x being Element of L holds f.x <= g.x; let x be set; assume x in the carrier of L; then reconsider x as Element of L; take f.x, g.x; thus thesis by A2; end; begin :: The Image of a Map definition let L, M be non empty RelStr; let f be map of L, M; func Image f -> strict full SubRelStr of M equals :Def2: subrelstr rng f; correctness; end; theorem Th11: for L, M being non empty RelStr for f being map of L, M holds rng f = the carrier of Image f proof let L1, L2 be non empty RelStr, g be map of L1,L2; Image g = subrelstr(rng g) by Def2; hence the carrier of Image g = rng g by YELLOW_0:def 15; end; theorem for L, M being non empty RelStr for f being map of L, M for y being Element of Image f ex x being Element of L st f.x = y proof let L1, L2 be non empty RelStr, g be map of L1,L2; let s be Element of Image g; A1: dom g = the carrier of L1 by FUNCT_2:def 1; then rng g is non empty & rng g = the carrier of Image g by Th11,RELAT_1:65; then consider l being set such that A2: l in dom g and A3: s = g.l by FUNCT_1:def 5; reconsider l as Element of L1 by A1,A2; take l; thus thesis by A3; end; definition let L be non empty RelStr; let X be non empty Subset of L; cluster subrelstr X -> non empty; coherence proof the carrier of subrelstr X = X by YELLOW_0:def 15; hence thesis by STRUCT_0:def 1; end; end; definition let L, M be non empty RelStr; let f be map of L, M; cluster Image f -> non empty; coherence proof dom f = the carrier of L by FUNCT_2:def 1; then rng f is non empty & rng f = the carrier of Image f by Th11,RELAT_1:65; hence Image f is non empty by STRUCT_0:def 1; end; end; begin :: Monotone Maps theorem for L being non empty RelStr holds id L is monotone proof let L be non empty RelStr; let l1,l2 be Element of L; assume l1 <= l2; then l1 <= (id L).l2 by TMAP_1:91; hence thesis by TMAP_1:91; end; theorem for L, M, N being non empty RelStr for f being map of L, M, g being map of M, N holds f is monotone & g is monotone implies g*f is monotone proof let L1,L2,L3 be non empty RelStr; let g1 be map of L1,L2, g2 be map of L2,L3 such that A1: g1 is monotone and A2: g2 is monotone; let s1,s2 be Element of L1; assume s1 <= s2; then g1.s1 <= g1.s2 by A1,ORDERS_3:def 5; then g2.(g1.s1) <= g2.(g1.s2) by A2,ORDERS_3:def 5; then (g2*g1).s1 <= g2.(g1.s2) by FUNCT_2:21; hence thesis by FUNCT_2:21; end; theorem for L, M being non empty RelStr for f being map 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 proof let L1,L2 be non empty RelStr, g be map of L1,L2; let X be Subset of L1, x be Element of L1 such that A1: g is monotone and A2: x is_<=_than X; let y2 be Element of L2; assume y2 in g.:X; then consider x2 being Element of L1 such that A3: x2 in X and A4: y2 = g.x2 by FUNCT_2:116; reconsider x2 as Element of L1; x <= x2 by A2,A3,LATTICE3:def 8; hence g.x <= y2 by A1,A4,ORDERS_3:def 5; end; theorem for L, M being non empty RelStr for f being map 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 proof let L1,L2 be non empty RelStr, g be map of L1,L2; let X be Subset of L1, x be Element of L1 such that A1: g is monotone and A2: x is_>=_than X; let y2 be Element of L2; assume y2 in g.:X; then consider x2 being Element of L1 such that A3: x2 in X and A4: y2 = g.x2 by FUNCT_2:116; reconsider x2 as Element of L1; x >= x2 by A2,A3,LATTICE3:def 9; hence g.x >= y2 by A1,A4,ORDERS_3:def 5; end; theorem for S, T being non empty RelStr for f being map of S, T for X being directed Subset of S holds f is monotone implies f.:X is directed proof let S, T be non empty RelStr; let f be map of S, T; let X be directed Subset of S; assume A1: f is monotone; set Y = f.:X; for y1, y2 being Element of T st y1 in Y & y2 in Y ex z being Element of T st z in Y & y1 <= z & y2 <= z proof let y1, y2 be Element of T; assume A2: y1 in Y & y2 in Y; then consider x1 being set such that x1 in dom f and A3: x1 in X and A4: y1 = f.x1 by FUNCT_1:def 12; consider x2 being set such that x2 in dom f and A5: x2 in X and A6: y2 = f.x2 by A2,FUNCT_1:def 12; reconsider x1, x2 as Element of S by A3,A5; consider z being Element of S such that A7: z in X & x1 <= z & x2 <= z by A3,A5,WAYBEL_0:def 1; take f.z; thus f.z in Y by A7,FUNCT_2:43; thus y1 <= f.z & y2 <= f.z by A1,A4,A6,A7,ORDERS_3:def 5; end; hence f.:X is directed by WAYBEL_0:def 1; end; theorem Th18: for L being with_suprema Poset for f being map of L, L holds f is directed-sups-preserving implies f is monotone proof let L be with_suprema Poset; let f be map of L, L; assume A1: f is directed-sups-preserving; let x, y be Element of L such that A2: x <= y; let afx, bfy be Element of L such that A3: afx = f.x & bfy = f.y; A4: y = y"\/"x by A2,YELLOW_0:24; x <= y & y <= y by A2; then A5: {x, y} is_<=_than y by YELLOW_0:8; for b being Element of L st {x, y} is_<=_than b holds y <= b by YELLOW_0:8; then A6: ex_sup_of {x, y},L by A5,YELLOW_0:30; for a, b being Element of L st a in {x, y} & b in {x, y} ex z being Element of L st z in {x, y} & a <= z & b <= z proof let a, b be Element of L such that A7: a in {x, y} & b in {x, y}; take y; thus y in {x, y} by TARSKI:def 2; thus a <= y & b <= y by A2,A7,TARSKI:def 2; end; then {x, y} is directed non empty by WAYBEL_0:def 1; then f preserves_sup_of {x, y} by A1,WAYBEL_0:def 37; then A8: sup(f.:{x, y}) = f.sup{x, y} by A6,WAYBEL_0:def 31 .= f.y by A4,YELLOW_0:41; dom f = the carrier of L by FUNCT_2:def 1; then f.y = sup{f.x, f.y} by A8,FUNCT_1:118 .= f.y"\/"f.x by YELLOW_0:41; hence afx <= bfy by A3,YELLOW_0:22; end; theorem for L being with_infima Poset for f being map of L, L holds f is filtered-infs-preserving implies f is monotone proof let L be with_infima Poset; let f be map of L, L; assume A1: f is filtered-infs-preserving; let x, y be Element of L such that A2: x <= y; let a, b be Element of L such that A3: a = f.x & b = f.y; A4: x = x"/\"y by A2,YELLOW_0:25; x <= x & x <= y by A2; then A5: x is_<=_than {x, y} by YELLOW_0:8; for c being Element of L st c is_<=_than {x, y} holds c <= x by YELLOW_0:8 ; then A6: ex_inf_of {x, y},L by A5,YELLOW_0:31; for c, d being Element of L st c in {x, y} & d in {x, y} ex z being Element of L st z in {x, y} & z <= c & z <= d proof let c, d be Element of L such that A7: c in {x, y} & d in {x, y}; take x; thus x in {x, y} by TARSKI:def 2; thus x <= c & x <= d by A2,A7,TARSKI:def 2; end; then {x, y} is filtered non empty by WAYBEL_0:def 2; then f preserves_inf_of {x, y} by A1,WAYBEL_0:def 36; then A8: inf(f.:{x, y}) = f.inf{x, y} by A6,WAYBEL_0:def 30 .= f.x by A4,YELLOW_0:40; dom f = the carrier of L by FUNCT_2:def 1; then f.x = inf{f.x, f.y} by A8,FUNCT_1:118 .= f.x"/\"f.y by YELLOW_0:40; hence a <= b by A3,YELLOW_0:23; end; begin :: Idempotent Maps theorem for S being non empty 1-sorted for f being map of S, S holds f is idempotent implies for x being Element of S holds f.(f.x) = f.x proof let L be non empty 1-sorted, p be map of L,L; assume A1: p*p = p; let l be Element of L; thus p.(p.l) = p.l by A1,FUNCT_2:21; end; theorem Th21: for S being non empty 1-sorted for f being map of S, S holds f is idempotent implies rng f = {x where x is Element of S: x = f.x} proof let S be non empty 1-sorted; let f be map of S, S; assume A1: f = f*f; set M = {x where x is Element of S: x = f.x}; A2: rng f c= M proof let y be set; assume A3: y in rng f; then consider x being set such that A4: x in dom f and A5: y = f.x by FUNCT_1:def 5; reconsider y'= y as Element of S by A3; y'= f.y' by A1,A4,A5,FUNCT_1:23; hence y in M; end; M c= rng f proof let y be set; assume y in M; then consider y' being Element of S such that A6: y' = y and A7: y' = f.y'; dom f = the carrier of S by FUNCT_2:def 1; hence y in rng f by A6,A7,FUNCT_1:def 5; end; hence rng f = {x where x is Element of S: x = f.x} by A2,XBOOLE_0:def 10; end; theorem Th22: for S being non empty 1-sorted for f being map of S, S st f is idempotent holds X c= rng f implies f.:X = X proof let S be non empty 1-sorted; let f be map of S, S such that A1: f is idempotent; set M = {x where x is Element of S: x = f.x}; assume X c= rng f; then A2: X c= M by A1,Th21; A3: f.:X c= X proof let y be set; assume y in f.:X; then consider x being set such that x in dom f and A4: x in X and A5: y = f.x by FUNCT_1:def 12; x in M by A2,A4; then consider x' being Element of S such that A6: x' = x and A7: x' = f.x'; thus y in X by A4,A5,A6,A7; end; X c= f.:X proof let y be set; assume A8: y in X; then y in M by A2; then consider x being Element of S such that A9: x = y and A10: x = f.x; thus y in f.:X by A8,A9,A10,FUNCT_2:43; end; hence f.:X = X by A3,XBOOLE_0:def 10; end; theorem for L being non empty RelStr holds id L is idempotent proof let L be non empty RelStr; id L = id the carrier of L by GRCAT_1:def 11; hence (id L)*(id L) = id ((the carrier of L) /\ (the carrier of L)) by FUNCT_1:43 .= (id L) by GRCAT_1:def 11; end; begin :: Complete Lattices (CCL Chapter 0, Section 2, pp. 8 -- 9) reserve L for complete LATTICE, a for Element of L; theorem Th24: a in X implies a <= "\/"(X, L) & "/\"(X, L) <= a proof assume A1: a in X; X is_<=_than "\/"(X, L) by YELLOW_0:32; hence a <= "\/"(X, L) by A1,LATTICE3:def 9; X is_>=_than "/\"(X, L) by YELLOW_0:33; hence "/\"(X, L) <= a by A1,LATTICE3:def 8; end; theorem Th25: for L being (non empty RelStr) holds (for X holds ex_sup_of X,L) iff (for Y holds ex_inf_of Y,L) proof let L be (non empty RelStr); hereby assume A1: for X holds ex_sup_of X,L; let Y; set X = {x where x is Element of L: x is_<=_than Y}; ex_sup_of X,L by A1; then consider a being Element of L such that A2: X is_<=_than a and A3: for b being Element of L st X is_<=_than b holds b >= a and A4: for c being Element of L st X is_<=_than c & for b being Element of L st X is_<=_than b holds b >= c holds c = a by YELLOW_0:def 7; A5: a is_<=_than Y proof let b be Element of L; assume A6: b in Y; b is_>=_than X proof let c be Element of L; assume c in X; then ex x being Element of L st c = x & x is_<=_than Y; hence c <= b by A6,LATTICE3:def 8; end; hence a <= b by A3; end; A7: for b being Element of L st Y is_>=_than b holds a >= b proof let b be Element of L; assume b is_<=_than Y; then b in X; hence b <= a by A2,LATTICE3:def 9; end; for c being Element of L st Y is_>=_than c & for b being Element of L st Y is_>=_than b holds b <= c holds c = a proof let c be Element of L such that A8: Y is_>=_than c and A9: for b being Element of L st Y is_>=_than b holds b <= c; A10: X is_<=_than c proof let b be Element of L; assume b in X; then ex x being Element of L st b = x & x is_<=_than Y; hence b <= c by A9; end; for b being Element of L st X is_<=_than b holds b >= c proof let b be Element of L; assume A11: X is_<=_than b; c in X by A8; hence c <= b by A11,LATTICE3:def 9; end; hence thesis by A4,A10; end; hence ex_inf_of Y,L by A5,A7,YELLOW_0:def 8; end; assume A12: for Y holds ex_inf_of Y,L; let X; set Y = {y where y is Element of L: X is_<=_than y}; ex_inf_of Y,L by A12; then consider a being Element of L such that A13: Y is_>=_than a and A14: for b being Element of L st Y is_>=_than b holds b <= a and A15: for c being Element of L st Y is_>=_than c & for b being Element of L st Y is_>=_than b holds b <= c holds c = a by YELLOW_0:def 8; A16: X is_<=_than a proof let b be Element of L; assume A17: b in X; b is_<=_than Y proof let c be Element of L; assume c in Y; then ex y being Element of L st c = y & X is_<=_than y; hence b <= c by A17,LATTICE3:def 9; end; hence b <= a by A14; end; A18: for b being Element of L st X is_<=_than b holds a <= b proof let b be Element of L; assume X is_<=_than b; then b in Y; hence a <= b by A13,LATTICE3:def 8; end; for c being Element of L st X is_<=_than c & for b being Element of L st X is_<=_than b holds b >= c holds c = a proof let c be Element of L such that A19: X is_<=_than c and A20: for b being Element of L st X is_<=_than b holds b >= c; A21: Y is_>=_than c proof let b be Element of L; assume b in Y; then ex x being Element of L st b = x & x is_>=_than X; hence c <= b by A20; end; for b being Element of L st Y is_>=_than b holds b <= c proof let b be Element of L; assume A22: Y is_>=_than b; c in Y by A19; hence b <= c by A22,LATTICE3:def 8; end; hence c = a by A15,A21; end; hence ex_sup_of X,L by A16,A18,YELLOW_0:def 7; end; theorem Th26: ::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 proof let L be (non empty RelStr); assume A1: for X holds ex_sup_of X,L; L is complete proof let X be set; take a = "\/"(X, L); A2: ex_sup_of X,L by A1; hence X is_<=_than a by YELLOW_0:def 9; thus thesis by A2,YELLOW_0:def 9; end; hence thesis; end; theorem Th27: ::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 proof let L be (non empty RelStr); assume for X holds ex_inf_of X,L; then for X holds ex_sup_of X,L by Th25; hence thesis by Th26; end; theorem Th28: 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) proof let L be (non empty RelStr); assume A1: for A being Subset of L holds ex_inf_of A, L; let X; set Y = X /\ the carrier of L; set a = "/\"(Y, L); Y c= the carrier of L by XBOOLE_1:17; then reconsider Y as Subset of L; A2: ex_inf_of Y,L by A1; then A3: ex_inf_of X,L by YELLOW_0:50; A4: a is_<=_than X proof let x be Element of L; assume x in X; then A5: x in Y by XBOOLE_0:def 3; a is_<=_than Y by A2,YELLOW_0:def 10; hence a <= x by A5,LATTICE3:def 8; end; for b being Element of L st b is_<=_than X holds b <= a proof let b be Element of L; assume A6: b is_<=_than X; Y c= X by XBOOLE_1:17; then b is_<=_than Y by A6,YELLOW_0:9; hence b <= a by A2,YELLOW_0:def 10; end; hence thesis by A3,A4,YELLOW_0:def 10; end; theorem 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) proof let L be (non empty RelStr); assume A1: for A being Subset of L holds ex_sup_of A, L; let X; set Y = X /\ the carrier of L; set a = "\/"(Y, L); Y c= the carrier of L by XBOOLE_1:17; then reconsider Y as Subset of L; A2: ex_sup_of Y,L by A1; then A3: ex_sup_of X,L by YELLOW_0:50; A4: X is_<=_than a proof let x be Element of L; assume x in X; then A5: x in Y by XBOOLE_0:def 3; Y is_<=_than a by A2,YELLOW_0:def 9; hence x <= a by A5,LATTICE3:def 9; end; for b being Element of L st X is_<=_than b holds a <= b proof let b be Element of L; assume A6: X is_<=_than b; Y c= X by XBOOLE_1:17; then Y is_<=_than b by A6,YELLOW_0:9; hence a <= b by A2,YELLOW_0:def 9; end; hence thesis by A3,A4,YELLOW_0:def 9; end; theorem Th30: ::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 proof let L be (non empty RelStr); assume for A being Subset of L holds ex_inf_of A,L; then for X holds ex_inf_of X, L by Th28; hence thesis by Th27; end; Lm1: for L being non empty Poset holds L is up-complete /\-complete upper-bounded implies L is complete (non empty Poset) proof let L be non empty Poset; assume A1: L is up-complete /\-complete upper-bounded; for A being Subset of L holds ex_inf_of A,L proof let A be Subset of L; per cases; suppose A is empty; hence ex_inf_of A,L by A1,YELLOW_0:43; suppose A is non empty; hence ex_inf_of A,L by A1,WAYBEL_0:76; end; hence thesis by Th30; end; definition cluster up-complete /\-complete upper-bounded -> complete (non empty Poset); correctness by Lm1; end; theorem Th31: :: Theorem 2.3 (The Fixed-Point Theorem) for f being map 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 proof let f be map of L, L such that A1: f is monotone; let M be Subset of L such that A2: M = {x where x is Element of L: x = f.x}; set S = subrelstr M; A3: for X being Subset of S for Y being Subset of L st Y = {y where y is Element of L: X is_<=_than f.y & f.y <= y} holds inf Y in M proof let X be Subset of S; let Y be Subset of L such that A4: Y = {y where y is Element of L: X is_<=_than f.y & f.y <= y}; set z = inf Y; A5: ex_inf_of Y,L by YELLOW_0:17; f.z is_<=_than Y proof let u be Element of L; assume A6: u in Y; then consider y being Element of L such that A7: y = u and X is_<=_than f.y and A8: f.y <= y by A4; z <= u by A6,Th24; then f.z <= f.y by A1,A7,ORDERS_3:def 5; hence f.z <= u by A7,A8,ORDERS_1:26; end; then A9: f.z <= z by A5,YELLOW_0:31; then A10: f.(f.z) <= f.z by A1,ORDERS_3:def 5; X is_<=_than f.(f.z) proof let m be Element of L; assume A11: m in X; X c= the carrier of S; then X c= M by YELLOW_0:def 15; then m in M by A11; then consider x being Element of L such that A12: x = m and A13: x = f.x by A2; m is_<=_than Y proof let u be Element of L; assume u in Y; then consider y being Element of L such that A14: y = u and A15: X is_<=_than f.y and A16: f.y <= y by A4; m <= f.y by A11,A15,LATTICE3:def 9; hence m <= u by A14,A16,ORDERS_1:26; end; then m <= z by YELLOW_0:33; then f.m <= f.z by A1,ORDERS_3:def 5; hence m <= f.(f.z) by A1,A12,A13,ORDERS_3:def 5; end; then f.z in Y by A4,A10; then z <= f.z by Th24; then z = f.z by A9,ORDERS_1:25; hence inf Y in M by A2; end; M c= the carrier of S by YELLOW_0:def 15; then reconsider M as Subset of S; defpred P[Element of L] means M is_<=_than f.$1 & f.$1 <= $1; reconsider Y = {y where y is Element of L: P[y]} as Subset of L from RelStrSubset; inf Y in M by A3; then reconsider S as non empty Poset by STRUCT_0:def 1; for X being Subset of S holds ex_sup_of X, S proof let X be Subset of S; defpred Q[Element of L] means X is_<=_than f.$1 & f.$1 <= $1; reconsider Y = {y where y is Element of L: Q[y]} as Subset of L from RelStrSubset; set z = inf Y; z in M & M = the carrier of S by A3,YELLOW_0:def 15; then reconsider z as Element of S; A17: X is_<=_than z proof let x be Element of S; assume A18: x in X; x in the carrier of S; then x in M by YELLOW_0:def 15; then consider m being Element of L such that A19: x = m and m = f.m by A2; m is_<=_than Y proof let u be Element of L; assume u in Y; then consider y being Element of L such that A20: y = u and A21: X is_<=_than f.y and A22: f.y <= y; m <= f.y by A18,A19,A21,LATTICE3:def 9; hence m <= u by A20,A22,ORDERS_1:26; end; then m <= inf Y & x in the carrier of S & z in the carrier of S by YELLOW_0:33; hence x <= z by A19,YELLOW_0:61; end; for b being Element of S st X is_<=_than b holds z <= b proof let b be Element of S; b in the carrier of S; then b in M by YELLOW_0:def 15; then consider x being Element of L such that A23: x = b and A24: x = f.x by A2; assume X is_<=_than b; then X is_<=_than f.x & f.x <= x by A23,A24,YELLOW_0:63; then x in Y; then inf Y <= x & z in the carrier of S & b in the carrier of S by Th24; hence z <= b by A23,YELLOW_0:61; end; hence thesis by A17,YELLOW_0:30; end; then reconsider S as complete (non empty Poset) by YELLOW_0:53; S is complete LATTICE; hence thesis; end; theorem Th32: for S being infs-inheriting non empty full SubRelStr of L holds S is complete LATTICE proof let S be infs-inheriting non empty full SubRelStr of L; for X being Subset of S holds ex_inf_of X,S proof let X be Subset of S; A1: ex_inf_of X,L by YELLOW_0:17; then "/\"(X,L) in the carrier of S by YELLOW_0:def 18; hence ex_inf_of X,S by A1,YELLOW_0:64; end; then S is complete by Th30; hence S is complete LATTICE by LATTICE3:12; end; theorem Th33: for S being sups-inheriting non empty full SubRelStr of L holds S is complete LATTICE proof let S be sups-inheriting non empty full SubRelStr of L; for X being Subset of S holds ex_sup_of X, S proof let X be Subset of S; A1: ex_sup_of X,L by YELLOW_0:17; then "\/"(X,L) in the carrier of S by YELLOW_0:def 19; hence ex_sup_of X,S by A1,YELLOW_0:65; end; then S is complete by YELLOW_0:53; hence S is complete LATTICE by LATTICE3:12; end; theorem Th34: ::Remark 2.4 (Part I, variant 1) for M being non empty RelStr for f being map of L, M st f is sups-preserving holds Image f is sups-inheriting proof let M be non empty RelStr; let f be map of L, M such that A1: f is sups-preserving; set S = subrelstr(rng f); for Y being Subset of S st ex_sup_of Y,M holds "\/"(Y, M) in the carrier of S proof let Y be Subset of S; assume ex_sup_of Y,M; A2: f preserves_sup_of (f"Y) by A1,WAYBEL_0:def 33; A3: ex_sup_of f"Y,L by YELLOW_0:17; Y c= the carrier of S; then Y c= rng f by YELLOW_0:def 15; then "\/"(Y, M) = sup(f.:(f"Y)) by FUNCT_1:147 .= f.sup(f"Y) by A2,A3,WAYBEL_0:def 31; then "\/"(Y, M) in rng f by FUNCT_2:6; hence "\/"(Y, M) in the carrier of S by YELLOW_0:def 15; end; then S is sups-inheriting by YELLOW_0:def 19; hence thesis by Def2; end; theorem Th35: ::Remark 2.4 (Part I, variant 2) for M being non empty RelStr for f being map of L, M st f is infs-preserving holds Image f is infs-inheriting proof let M be non empty RelStr; let f be map of L, M such that A1: f is infs-preserving; set S = subrelstr(rng f); for Y being Subset of S st ex_inf_of Y,M holds "/\"(Y, M) in the carrier of S proof let Y be Subset of S; assume ex_inf_of Y,M; A2: f preserves_inf_of (f"Y) by A1,WAYBEL_0:def 32; A3: ex_inf_of f"Y,L by YELLOW_0:17; Y c= the carrier of S; then Y c= rng f by YELLOW_0:def 15; then "/\"(Y, M) = inf(f.:(f"Y)) by FUNCT_1:147 .= f.inf(f"Y) by A2,A3,WAYBEL_0:def 30; then "/\"(Y, M) in rng f by FUNCT_2:6; hence "/\"(Y, M) in the carrier of S by YELLOW_0:def 15; end; then S is infs-inheriting by YELLOW_0:def 18; hence thesis by Def2; end; theorem ::Remark 2.4 (Part II) for L, M being complete LATTICE for f being map of L, M st f is sups-preserving or f is infs-preserving holds Image f is complete LATTICE proof let L, M be complete LATTICE; let f be map of L, M such that A1: f is sups-preserving or f is infs-preserving; per cases by A1; suppose f is sups-preserving; then Image f is sups-inheriting by Th34; hence Image f is complete LATTICE by Th33; suppose f is infs-preserving; then Image f is infs-inheriting by Th35; hence Image f is complete LATTICE by Th32; end; theorem ::Remark 2.5 for f being map of L, L st f is idempotent directed-sups-preserving holds Image f is directed-sups-inheriting & Image f is complete LATTICE proof let f be map of L, L; assume A1: f is idempotent directed-sups-preserving; then A2: f is monotone by Th18; set S = subrelstr(rng f); consider a being Element of L; dom f = the carrier of L by FUNCT_2:def 1; then f.a in rng f by FUNCT_1:def 5; then the carrier of S is non empty by YELLOW_0:def 15; then reconsider S'= S as non empty full SubRelStr of L by STRUCT_0:def 1; for X being directed Subset of S st X <> {} & ex_sup_of X,L holds "\/"(X,L) in the carrier of S proof let X be directed Subset of S; assume X <> {}; then X is non empty directed Subset of S'; then reconsider X'= X as non empty directed Subset of L by Th7; A3: f preserves_sup_of X' by A1,WAYBEL_0:def 37; assume ex_sup_of X,L; then A4: ex_sup_of f.:X',L & sup(f.:X') = f.sup X' by A3,WAYBEL_0:def 31; X c= the carrier of S; then X c= rng f by YELLOW_0:def 15; then sup X' = f.sup X' & the carrier of L <> {} by A1,A4,Th22; then "\/"(X, L) in rng f by FUNCT_2:6; hence "\/"(X, L) in the carrier of S by YELLOW_0:def 15; end; then S is directed-sups-inheriting by WAYBEL_0:def 4; hence Image f is directed-sups-inheriting by Def2; rng f = {x where x is Element of L: x = f.x} by A1,Th21; then S is complete LATTICE by A2,Th31; hence Image f is complete LATTICE by Def2; end; begin :: A Lattice of Ideals theorem Th38: for L being RelStr for F being Subset of bool the carrier 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 proof let L be RelStr; let F be Subset of bool the carrier of L; reconsider F' = F as Subset-Family of L by SETFAM_1:def 7; assume A1: for X being Subset of L st X in F holds X is lower; reconsider M = meet F' as Subset of L; per cases; suppose F = {}; then for x, y being Element of L st x in M & y <= x holds y in M by SETFAM_1:def 1; hence thesis by WAYBEL_0:def 19; suppose A2: F <> {}; for x, y being Element of L st x in M & y <= x holds y in M proof let x, y be Element of L; assume that A3: x in M and A4: y <= x; for Y being set st Y in F holds y in Y proof let Y be set; assume A5: Y in F; then reconsider X = Y as Subset of L; A6: X is lower by A1,A5; x in X by A3,A5,SETFAM_1:def 1; hence y in Y by A4,A6,WAYBEL_0:def 19; end; hence y in M by A2,SETFAM_1:def 1; end; hence thesis by WAYBEL_0:def 19; end; theorem for L being RelStr for F being Subset of bool the carrier 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 proof let L be RelStr; let F be Subset of bool the carrier of L; reconsider F' = F as Subset-Family of L by SETFAM_1:def 7; assume A1: for X being Subset of L st X in F holds X is upper; reconsider M = meet F' as Subset of L; per cases; suppose F = {}; then for x, y being Element of L st x in M & x <= y holds y in M by SETFAM_1:def 1; hence thesis by WAYBEL_0:def 20; suppose A2: F <> {}; for x, y being Element of L st x in M & x <= y holds y in M proof let x, y be Element of L; assume that A3: x in M and A4: x <= y; for Y being set st Y in F holds y in Y proof let Y be set; assume A5: Y in F; then reconsider X = Y as Subset of L; A6: X is upper by A1,A5; x in X by A3,A5,SETFAM_1:def 1; hence y in Y by A4,A6,WAYBEL_0:def 20; end; hence y in M by A2,SETFAM_1:def 1; end; hence thesis by WAYBEL_0:def 20; end; theorem Th40: for L being with_suprema antisymmetric RelStr for F being Subset of bool the carrier 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 proof let L be with_suprema antisymmetric RelStr; let F be Subset of bool the carrier of L; assume A1: for X being Subset of L st X in F holds X is lower directed; reconsider F' = F as Subset-Family of L by SETFAM_1:def 7; reconsider M = meet F' as Subset of L; per cases; suppose A2: F = {}; M is directed proof let x, y be Element of L; assume x in M & y in M; hence thesis by A2,SETFAM_1:def 1; end; hence thesis; suppose A3: F <> {}; M is directed proof let x, y be Element of L such that A4: x in M & y in M; take z = x"\/"y; for Y being set st Y in F holds z in Y proof let Y be set; assume A5: Y in F; then reconsider X = Y as Subset of L; A6: X is lower directed by A1,A5; x in X & y in X by A4,A5,SETFAM_1:def 1; hence z in Y by A6,WAYBEL_0:40; end; hence z in M by A3,SETFAM_1:def 1; thus x <= z & y <= z by YELLOW_0:22; end; hence thesis; end; theorem for L being with_infima antisymmetric RelStr for F being Subset of bool the carrier 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 proof let L be with_infima antisymmetric RelStr; let F be Subset of bool the carrier of L; assume A1: for X being Subset of L st X in F holds X is upper filtered; reconsider F' = F as Subset-Family of L by SETFAM_1:def 7; reconsider M = meet F' as Subset of L; per cases; suppose A2: F = {}; M is filtered proof let x, y be Element of L; assume x in M & y in M; hence thesis by A2,SETFAM_1:def 1; end; hence thesis; suppose A3: F <> {}; M is filtered proof let x, y be Element of L such that A4: x in M & y in M; take z = x"/\"y; for Y being set st Y in F holds z in Y proof let Y be set; assume A5: Y in F; then reconsider X = Y as Subset of L; A6: X is upper filtered by A1,A5; x in X & y in X by A4,A5,SETFAM_1:def 1; hence z in Y by A6,WAYBEL_0:41; end; hence z in M by A3,SETFAM_1:def 1; thus z <= x & z <= y by YELLOW_0:23; end; hence thesis; end; theorem Th42: for L being with_infima Poset for I, J being Ideal of L holds I /\ J is Ideal of L proof let L be with_infima Poset; let I, J be Ideal of L; consider i being Element of I, j being Element of J; set a = i"/\"j; a <= i & a <= j by YELLOW_0:23; then a in I & a in J by WAYBEL_0:def 19; hence I /\ J is Ideal of L by WAYBEL_0:27,44,XBOOLE_0:def 3; end; definition let L be non empty reflexive transitive RelStr; cluster Ids L -> non empty; correctness proof consider x being Element of L; downarrow x in {Y where Y is Ideal of L: not contradiction}; hence Ids L is non empty by WAYBEL_0:def 23; end; end; theorem Th43: for L being non empty reflexive transitive RelStr holds (x is Element of InclPoset(Ids L) iff x is Ideal of L) proof let L be non empty reflexive transitive RelStr; hereby assume x is Element of InclPoset(Ids L); then x in the carrier of InclPoset(Ids L); then x in Ids L by YELLOW_1:1; then x in {Y where Y is Ideal of L: not contradiction} by WAYBEL_0:def 23; then consider J being Ideal of L such that A1: J = x; thus x is Ideal of L by A1; end; assume x is Ideal of L; then x in {Y where Y is Ideal of L: not contradiction}; then x in Ids L by WAYBEL_0:def 23; then x in the carrier of InclPoset(Ids L) by YELLOW_1:1; hence x is Element of InclPoset(Ids L); end; theorem Th44: 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 proof let L be non empty reflexive transitive RelStr; let I be Element of InclPoset(Ids L); reconsider I'= I as non empty Subset of L by Th43; assume x in I; then reconsider x'= x as Element of I'; x' in the carrier of L; hence x is Element of L; end; theorem for L being with_infima Poset for x, y being Element of InclPoset(Ids L) holds x "/\" y = x /\ y proof let L be with_infima Poset; let x, y be Element of InclPoset(Ids L); reconsider x'= x, y'= y as Ideal of L by Th43; x' /\ y' is Ideal of L by Th42; then x' /\ y' in {X where X is Ideal of L: not contradiction}; then x /\ y in Ids L by WAYBEL_0:def 23; hence x /\ y = x "/\" y by YELLOW_1:9; end; definition let L be with_infima Poset; cluster InclPoset(Ids L) -> with_infima; correctness proof for x, y be set st (x in Ids L & y in Ids L) holds x /\ y in Ids L proof let x, y be set; assume A1: x in Ids L & y in Ids L; then x in {X where X is Ideal of L: not contradiction} by WAYBEL_0:def 23; then consider I being Ideal of L such that A2: I = x; y in {X where X is Ideal of L: not contradiction} by A1,WAYBEL_0:def 23 ; then consider J being Ideal of L such that A3: J = y; I /\ J is Ideal of L by Th42; then I /\ J in {X where X is Ideal of L: not contradiction}; hence x /\ y in Ids L by A2,A3,WAYBEL_0:def 23; end; hence InclPoset(Ids L) is with_infima by YELLOW_1:12; end; end; theorem Th46: 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 proof let L be with_suprema Poset; set P = InclPoset(Ids L); let x, y be Element of P; reconsider x'= x, y'= y as Ideal of L by Th43; defpred P[Element of L] means $1 in x or $1 in y or ex a, b being Element of L st a in x & b in y & $1 = a "\/" b; reconsider Z = {z where z is Element of L: P[z]} as Subset of L from RelStrSubset; take Z; consider z being Element of x'; z in Z; then reconsider Z as non empty Subset of L; set DZ = downarrow Z; for u, v being Element of L st u in Z & v in Z ex z being Element of L st z in Z & u <= z & v <= z proof let u, v be Element of L such that A1: u in Z and A2: v in Z; consider p being Element of L such that A3: p = u and A4: p in x or p in y or ex a, b being Element of L st a in x & b in y & p = a "\/" b by A1; consider q being Element of L such that A5: q = v and A6: q in x or q in y or ex a, b being Element of L st a in x & b in y & q = a "\/" b by A2; A7: for p, q being Element of L st p in x & ex a, b being Element of L st a in x & b in y & q = a "\/" b holds ex z being Element of L st z in Z & p <= z & q <= z proof let p, q be Element of L such that A8: p in x and A9: ex a, b being Element of L st a in x & b in y & q = a "\/" b; consider a, b being Element of L such that A10: a in x and A11: b in y and A12: q = a "\/" b by A9; reconsider c = a "\/" p as Element of L; take z = c "\/" b; c in x' by A8,A10,WAYBEL_0:40; hence z in Z by A11; A13: a <= c & p <= c & c <= z & b <= z by YELLOW_0:22; then a <= z & b <= z by ORDERS_1:26; hence p <= z & q <= z by A12,A13,ORDERS_1:26,YELLOW_0:22; end; A14: for p, q being Element of L st p in y & ex a, b being Element of L st a in x & b in y & q = a "\/" b holds ex z being Element of L st z in Z & p <= z & q <= z proof let p, q be Element of L such that A15: p in y and A16: ex a, b being Element of L st a in x & b in y & q = a "\/" b; consider a, b being Element of L such that A17: a in x and A18: b in y and A19: q = a "\/" b by A16; reconsider c = b "\/" p as Element of L; take z = a "\/" c; c in y' by A15,A18,WAYBEL_0:40; hence z in Z by A17; A20: b <= c & p <= c & a <= z & c <= z by YELLOW_0:22; then a <= z & b <= z by ORDERS_1:26; hence p <= z & q <= z by A19,A20,ORDERS_1:26,YELLOW_0:22; end; per cases by A4,A6; suppose p in x & q in x; then consider z being Element of L such that A21: z in x' & p <= z & q <= z by WAYBEL_0:def 1; take z; thus thesis by A3,A5,A21; suppose A22: p in x & q in y; take p "\/" q; thus thesis by A3,A5,A22,YELLOW_0:22; suppose p in x & ex a, b being Element of L st a in x & b in y & q = a "\/" b; then consider z being Element of L such that A23: z in Z & p <= z & q <= z by A7; take z; thus thesis by A3,A5,A23; suppose A24: p in y & q in x; take q "\/" p; thus thesis by A3,A5,A24,YELLOW_0:22; suppose p in y & q in y; then consider z being Element of L such that A25: z in y' & p <= z & q <= z by WAYBEL_0:def 1; take z; thus thesis by A3,A5,A25; suppose p in y & ex a, b being Element of L st a in x & b in y & q = a "\/" b; then consider z being Element of L such that A26: z in Z & p <= z & q <= z by A14; take z; thus thesis by A3,A5,A26; suppose q in x & ex a, b being Element of L st a in x & b in y & p = a "\/" b; then consider z being Element of L such that A27: z in Z & q <= z & p <= z by A7; take z; thus thesis by A3,A5,A27; suppose q in y & ex a, b being Element of L st a in x & b in y & p = a "\/" b; then consider z being Element of L such that A28: z in Z & q <= z & p <= z by A14; take z; thus thesis by A3,A5,A28; suppose (ex a, b being Element of L st a in x & b in y & p = a "\/" b) & (ex a, b being Element of L st a in x & b in y & q = a "\/" b); then consider a, b, c, d being Element of L such that A29: a in x & b in y & p = a "\/" b and A30: c in x & d in y & q = c "\/" d; reconsider ac = a "\/" c, bd = b "\/" d as Element of L; take z = ac "\/" bd; ac in x' & bd in y' by A29,A30,WAYBEL_0:40; hence z in Z; A31: a <= ac & c <= ac & b <= bd & d <= bd & ac <= z & bd <= z by YELLOW_0:22; then a <= z & b <= z by ORDERS_1:26; hence u <= z by A3,A29,YELLOW_0:22; c <= z & d <= z by A31,ORDERS_1:26; hence v <= z by A5,A30,YELLOW_0:22; end; then Z is directed by WAYBEL_0:def 1; then DZ is Ideal of L by WAYBEL_0:30; then reconsider DZ as Element of P by Th43; x c= DZ proof let a be set; assume A32: a in x; then reconsider a'= a as Element of L by Th44; a' in Z & Z c= DZ by A32,WAYBEL_0:16; hence a in DZ; end; then A33: x <= DZ by YELLOW_1:3; y c= DZ proof let a be set; assume A34: a in y; then reconsider a'= a as Element of L by Th44; a' in Z & Z c= DZ by A34,WAYBEL_0:16; hence a in DZ; end; then A35: y <= DZ by YELLOW_1:3; for d being Element of P st d >= x & d >= y holds DZ <= d proof let d be Element of P; assume x <= d & y <= d; then A36: x c= d & y c= d by YELLOW_1:3; DZ c= d proof let p be set; assume p in DZ; then p in {q where q is Element of L: ex u being Element of L st q <= u & u in Z} by WAYBEL_0:14; then consider p' being Element of L such that A37: p' = p and A38: ex u being Element of L st p' <= u & u in Z; consider u being Element of L such that A39: p' <= u and A40: u in Z by A38; consider z being Element of L such that A41: z = u and A42: 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 by A40; per cases by A42; suppose z in x; then p in x' by A37,A39,A41,WAYBEL_0:def 19; hence p in d by A36; suppose z in y; then p in y' by A37,A39,A41,WAYBEL_0:def 19; hence p in d by A36; suppose ex a, b being Element of L st a in x & b in y & z = a "\/" b; then consider a, b being Element of L such that A43: a in x and A44: b in y and A45: z = a "\/" b; reconsider d'= d as Ideal of L by Th43; u in d' by A36,A41,A43,A44,A45,WAYBEL_0:40; hence p in d by A37,A39,WAYBEL_0:def 19; end; hence DZ <= d by YELLOW_1:3; end; hence thesis by A33,A35,YELLOW_0:18; end; definition let L be with_suprema Poset; cluster InclPoset(Ids L) -> with_suprema; correctness proof set P = InclPoset(Ids L); for x, y being Element of P ex z being Element of P st x <= z & y <= z & for z' being Element of P st x <= z' & y <= z' holds z <= z' proof let x, y be Element of P; consider Z being Subset of L such that 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} and A1: ex_sup_of {x, y},InclPoset(Ids L) and x "\/" y = downarrow Z by Th46; take x "\/" y; thus thesis by A1,YELLOW_0:18; end; hence thesis by LATTICE3:def 10; end; end; theorem Th47: for L being lower-bounded sup-Semilattice for X being non empty Subset of Ids L holds meet X is Ideal of L proof let L be lower-bounded sup-Semilattice; let X be non empty Subset of Ids L; A1: for J being set st J in X holds J is Ideal of L proof let J be set; assume J in X; then J in Ids L; then J in {Y where Y is Ideal of L: not contradiction} by WAYBEL_0:def 23; then ex Y being Ideal of L st Y = J; hence thesis; end; X c= bool the carrier of L proof let x; assume x in X; then x is Ideal of L by A1; hence x in bool the carrier of L; end; then reconsider F = X as Subset of bool the carrier of L; for J being Subset of L st J in F holds J is lower by A1; then reconsider I = meet X as lower Subset of L by Th38; for J being set st J in X holds Bottom L in J proof let J be set; assume J in X; then reconsider J'= J as Ideal of L by A1; consider j being Element of J'; Bottom L <= j by YELLOW_0:44; hence Bottom L in J by WAYBEL_0:def 19; end; then reconsider I as non empty lower Subset of L by SETFAM_1:def 1; for J being Subset of L st J in F holds J is lower directed by A1; then I is Ideal of L by Th40; hence thesis; end; theorem Th48: 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 proof let L be lower-bounded sup-Semilattice; let A be non empty Subset of InclPoset(Ids L); set P = InclPoset(Ids L); A c= the carrier of InclPoset Ids L; then A c= Ids L by YELLOW_1:1; then reconsider A'= A as non empty Subset of Ids L; meet A' is Ideal of L by Th47; then reconsider I = meet A as Element of P by Th43; A1: I is_<=_than A proof let y be Element of P; assume A2: y in A; I c= y proof let x be set; assume x in I; hence x in y by A2,SETFAM_1:def 1; end; hence I <= y by YELLOW_1:3; end; for b being Element of P st b is_<=_than A holds I >= b proof let b be Element of P; assume A3: A is_>=_than b; A4: for J being set st J in A holds b c= J proof let J be set; assume A5: J in A; then J is Element of A; then reconsider y = J as Element of P; b <= y by A3,A5,LATTICE3:def 8; hence b c= J by YELLOW_1:3; end; b c= I proof let c be set; assume A6: c in b; for J being set st J in A holds c in J proof let J be set; assume J in A; then b c= J by A4; hence c in J by A6; end; hence c in I by SETFAM_1:def 1; end; hence I >= b by YELLOW_1:3; end; hence thesis by A1,YELLOW_0:31; end; theorem Th49: for L being with_suprema Poset holds ex_inf_of {},InclPoset(Ids L) & "/\"({}, InclPoset(Ids L)) = [#]L proof let L be with_suprema Poset; set P = InclPoset(Ids L); reconsider I = [#]L as Element of P by Th43; A1: I is_<=_than {} proof let y be Element of P; assume y in {}; hence thesis; end; for b being Element of P st b is_<=_than {} holds I >= b proof let b be Element of P; assume {} is_>=_than b; reconsider b'= b as Ideal of L by Th43; b' c= the carrier of L; then b' c= [#]L by PRE_TOPC:12; hence I >= b by YELLOW_1:3; end; hence thesis by A1,YELLOW_0:31; end; theorem Th50: for L being lower-bounded sup-Semilattice holds InclPoset(Ids L) is complete proof let L be lower-bounded sup-Semilattice; set P = InclPoset(Ids L); for A being Subset of P holds ex_inf_of A,InclPoset(Ids L) proof let A be Subset of P; per cases; suppose A = {}; hence thesis by Th49; suppose A <> {}; hence thesis by Th48; end; hence InclPoset(Ids L) is complete by Th30; end; definition let L be lower-bounded sup-Semilattice; cluster InclPoset(Ids L) -> complete; correctness by Th50; end; begin :: Special Maps definition let L be non empty Poset; func SupMap L -> map of InclPoset(Ids L), L means :Def3: for I being Ideal of L holds it.I = sup I; existence proof set P = InclPoset(Ids L); deffunc F(set) = "\/"($1, L); A1: for I being set st I in the carrier of P holds F(I) in the carrier of L; ex f being Function of the carrier of P, the carrier of L st for I being set st I in the carrier of P holds f.I = F(I) from Lambda1(A1); then consider f being Function of the carrier of P, the carrier of L such that A2: for I being set st I in the carrier of P holds f.I = "\/"(I, L); reconsider f as map of P, L; take f; for I being Ideal of L holds f.I = sup I proof let I be Ideal of L; I in {X where X is Ideal of L: not contradiction}; then I in the carrier of RelStr(#Ids L, RelIncl Ids L#) by WAYBEL_0:def 23; then I in the carrier of P by YELLOW_1:def 1; hence f.I = sup I by A2; end; hence thesis; end; uniqueness proof let f, g be map of InclPoset(Ids L), L; assume that A3: for I being Ideal of L holds f.I = sup I and A4: for I being Ideal of L holds g.I = sup I; set P = InclPoset(Ids L); A5: dom f = the carrier of P & dom g = the carrier of P by FUNCT_2:def 1; A6: the carrier of P = the carrier of RelStr(#Ids L, RelIncl(Ids L)#) by YELLOW_1:def 1 .= Ids L; now let x be set; assume x in the carrier of P; then x in {X where X is Ideal of L: not contradiction} by A6,WAYBEL_0:def 23; then ex I being Ideal of L st x = I; then reconsider I = x as Ideal of L; f.I = sup I & g.I = sup I by A3,A4; hence f.x = g.x; end; hence f = g by A5,FUNCT_1:9; end; end; theorem Th51: for L being non empty Poset holds dom SupMap L = Ids L & rng SupMap L is Subset of L proof let L be non empty Poset; set P = InclPoset(Ids L); thus dom(SupMap L) = the carrier of P by FUNCT_2:def 1 .= the carrier of RelStr(#Ids L, RelIncl(Ids L)#) by YELLOW_1:def 1 .= Ids L; thus rng(SupMap L) is Subset of L; end; theorem for L being non empty Poset holds x in dom SupMap L iff x is Ideal of L proof let L be non empty Poset; hereby assume x in dom SupMap L; then x in Ids L by Th51; then x in {X where X is Ideal of L: not contradiction} by WAYBEL_0:def 23; then ex I being Ideal of L st x = I; hence x is Ideal of L; end; assume x is Ideal of L; then x in {X where X is Ideal of L: not contradiction}; then x in Ids L by WAYBEL_0:def 23; hence x in dom(SupMap L) by Th51; end; theorem Th53: for L being up-complete (non empty Poset) holds SupMap L is monotone proof let L be up-complete (non empty Poset); set P = InclPoset Ids L; set f = SupMap L; for x, y being Element of P st x <= y for a, b being Element of L st a = f.x & b = f.y holds a <= b proof let x, y be Element of P such that A1: x <= y; let a, b be Element of L such that A2: a = f.x & b = f.y; reconsider I = x, J = y as Ideal of L by Th43; A3: ex_sup_of I,L & ex_sup_of J,L by WAYBEL_0:75; A4: I c= J by A1,YELLOW_1:3; f.x = sup I & f.y = sup J by Def3; hence thesis by A2,A3,A4,YELLOW_0:34; end; hence thesis by ORDERS_3:def 5; end; definition let L be up-complete (non empty Poset); cluster SupMap L -> monotone; correctness by Th53; end; definition let L be non empty Poset; func IdsMap L -> map of L, InclPoset(Ids L) means :Def4: for x being Element of L holds it.x = downarrow x; existence proof deffunc F(Element of L) = downarrow $1; A1: for x being Element of L holds F(x) is Element of InclPoset(Ids L) by Th43; thus ex m being map of L, InclPoset Ids L st for x being Element of L holds m.x = F(x) from KappaMD(A1); end; uniqueness proof let f1,f2 be map of L,InclPoset(Ids L) such that A2: for x being Element of L holds f1.x = downarrow x and A3: for x being Element of L holds f2.x = downarrow x; now let x be Element of L; thus f1.x = downarrow x by A2 .= f2.x by A3; end; hence thesis by Th9; end; end; theorem Th54: for L being non empty Poset holds IdsMap L is monotone proof let L be non empty Poset; let x1,x2 be Element of L such that A1: x1 <= x2; let a, b be Element of InclPoset(Ids L) such that A2: a = (IdsMap L).x1 & b = (IdsMap L).x2; downarrow x1 c= downarrow x2 by A1,WAYBEL_0:21; then (IdsMap L).x1 c= downarrow x2 by Def4; then (IdsMap L).x1 c= (IdsMap L).x2 by Def4; hence a <= b by A2,YELLOW_1:3; end; definition let L be non empty Poset; cluster IdsMap L -> monotone; correctness by Th54; 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 :Def5: "\/"(rng F, L); coherence; func //\(F, L) -> Element of L equals :Def6: "/\"(rng F, L); coherence; end; definition let J be set, L be non empty RelStr; let F be Function of J, the carrier of L; redefine func \\/(F, L); synonym Sup F; redefine func //\(F, L); synonym Inf F; end; definition let J be non empty set, S be non empty 1-sorted; let F be Function of J, the carrier of S; let j be Element of J; redefine func F.j -> Element of S; coherence proof F.j in the carrier of S; hence thesis; end; end; definition let J be set, S be non empty 1-sorted; let F be Function of J, the carrier of S; redefine func rng F -> Subset of S; coherence by RELSET_1:12; end; reserve J for non empty set, j for Element of J; theorem for F being Function of J, the carrier of L holds F.j <= Sup F & Inf F <= F.j proof let F be Function of J, the carrier of L; F.j in rng F by FUNCT_2:6; then F.j <= "\/"(rng F, L) & "/\"(rng F, L) <= F.j by Th24; hence F.j <= Sup F & Inf F <= F.j by Def5,Def6; end; theorem for F being Function of J, the carrier of L holds (for j holds F.j <= a) implies Sup F <= a proof let F be Function of J, the carrier of L; assume A1: for j holds F.j <= a; now let c be Element of L; assume c in rng F; then consider j being set such that A2: j in dom F and A3: c = F.j by FUNCT_1:def 5; reconsider j as Element of J by A2,FUNCT_2:def 1; c = F.j by A3; hence c <= a by A1; end; then rng F is_<=_than a by LATTICE3:def 9; then "\/"(rng F, L) <= a by YELLOW_0:32; hence thesis by Def5; end; theorem for F being Function of J, the carrier of L holds (for j holds a <= F.j) implies a <= Inf F proof let F be Function of J, the carrier of L; assume A1: for j holds a <= F.j; now let c be Element of L; assume c in rng F; then consider j being set such that A2: j in dom F and A3: c = F.j by FUNCT_1:def 5; reconsider j as Element of J by A2,FUNCT_2:def 1; c = F.j by A3; hence a <= c by A1; end; then a is_<=_than rng F by LATTICE3:def 8; then a <= "/\"(rng F, L) by YELLOW_0:33; hence thesis by Def6; end;