Copyright (c) 1996 Association of Mizar Users
environ vocabulary FUNCT_1, RELAT_1, PRE_TOPC, ORDERS_1, SEQM_3, RELAT_2, LATTICE3, LATTICES, WAYBEL_0, YELLOW_1, BOOLE, YELLOW_0, CAT_1, WELLORD1, ORDINAL2, BHSP_3, FILTER_0, FILTER_2, BINOP_1, SGRAPH1, GROUP_6, QUANTAL1, YELLOW_2, LATTICE2, ZF_LANG, FILTER_1, WAYBEL_1; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, PRE_TOPC, STRUCT_0, WELLORD1, ORDERS_1, LATTICE3, QUANTAL1, ORDERS_3, YELLOW_0, GRCAT_1, YELLOW_1, WAYBEL_0, YELLOW_2; constructors TOPS_2, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, GRCAT_1; clusters STRUCT_0, RELSET_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, RELAT_1, FUNCT_2, PARTFUN1; requirements SUBSET, BOOLE; definitions TARSKI, LATTICE3, QUANTAL1, ORDERS_3, YELLOW_0, WAYBEL_0, XBOOLE_0; theorems STRUCT_0, ZFMISC_1, ORDERS_1, FUNCT_1, FUNCT_2, LATTICE3, RELAT_1, TARSKI, WELLORD1, TMAP_1, ORDERS_3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, GRCAT_1, RELSET_1, XBOOLE_0, XBOOLE_1; schemes FUNCT_2, YELLOW_2; begin :: Preliminaries definition let L1,L2 be non empty 1-sorted, f be map of L1,L2; redefine attr f is one-to-one means for x,y being Element of L1 st f.x = f.y holds x=y; compatibility proof thus f is one-to-one implies for x,y being Element of L1 st f.x = f.y holds x=y by FUNCT_2:25; assume A1: for x,y being Element of L1 st f.x = f.y holds x=y; for x,y be set st x in the carrier of L1 & y in the carrier of L1 holds f.x = f.y implies x=y by A1; hence thesis by FUNCT_2:25; end; end; theorem Th1: for L being non empty 1-sorted, f being map of L,L st for x being Element of L holds f.x = x holds f = id L by TMAP_1:92; definition let L1,L2 be non empty RelStr, f be map of L1,L2; redefine attr f is monotone means :Def2: for x,y being Element of L1 st x <= y holds f.x <= f.y; compatibility proof thus f is monotone implies for x,y being Element of L1 st x <= y holds f.x <= f.y by ORDERS_3:def 5; assume for x,y being Element of L1 st x <= y holds f.x <= f.y; hence 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; end; theorem Th2: for L being antisymmetric transitive with_infima RelStr, x,y,z being Element of L st x <= y holds x "/\" z <= y "/\" z proof let L be antisymmetric transitive with_infima RelStr; let x,y,z be Element of L; assume A1: x <= y; x"/\"z <= x by YELLOW_0:23; then x"/\"z <= y & x"/\"z <= z by A1,ORDERS_1:26,YELLOW_0:23; hence x"/\"z <= y"/\"z by YELLOW_0:23; end; theorem Th3: for L being antisymmetric transitive with_suprema RelStr, x,y,z being Element of L st x <= y holds x "\/" z <= y "\/" z proof let L be antisymmetric transitive with_suprema RelStr; let x,y,z be Element of L; assume A1: x <= y; y <= y"\/"z by YELLOW_0:22; then x <= y"\/"z & z <= y"\/"z by A1,ORDERS_1:26,YELLOW_0:22; hence x"\/"z <= y"\/"z by YELLOW_0:22; end; theorem Th4: for L being non empty lower-bounded antisymmetric RelStr for x being Element of L holds (L is with_infima implies Bottom L "/\" x = Bottom L) & (L is with_suprema reflexive transitive implies Bottom L "\/" x = x) proof let L be non empty lower-bounded antisymmetric RelStr; let x be Element of L; thus L is with_infima implies Bottom L "/\" x = Bottom L proof assume L is with_infima; then Bottom L <= Bottom L "/\" x & Bottom L "/\" x <= Bottom L by YELLOW_0: 23,44; hence Bottom L "/\" x = Bottom L by ORDERS_1:25; end; assume A1: L is with_suprema; assume L is reflexive transitive; then A2: x <= x by ORDERS_1:24; Bottom L <= x by YELLOW_0:44; then x <= Bottom L "\/" x & Bottom L "\/" x <= x by A1,A2,YELLOW_0:22; hence Bottom L "\/" x = x by ORDERS_1:25; end; theorem Th5: for L being non empty upper-bounded antisymmetric RelStr for x being Element of L holds (L is with_infima transitive reflexive implies Top L "/\" x = x) & (L is with_suprema implies Top L "\/" x = Top L) proof let L be non empty upper-bounded antisymmetric RelStr, x be Element of L; thus L is with_infima transitive reflexive implies Top L "/\" x = x proof assume A1: L is with_infima transitive reflexive; x <= Top L by YELLOW_0:45; then x "/\" x <= Top L "/\" x by A1,Th2; then Top L "/\" x <= x & x <= Top L "/\" x by A1,YELLOW_0:23,25; hence Top L "/\" x = x by ORDERS_1:25; end; assume L is with_suprema; then Top L "\/" x <= Top L & Top L <= Top L "\/" x by YELLOW_0:22,45; hence Top L "\/" x = Top L by ORDERS_1:25; end; definition let L be non empty RelStr; attr L is distributive means :Def3: for x,y,z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z); end; theorem Th6: for L being LATTICE holds L is distributive iff for x,y,z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) proof let L be LATTICE; hereby assume A1: L is distributive; let x,y,z be Element of L; thus x"\/"(y"/\"z) = (x"\/"(z"/\"x))"\/"(y"/\"z) by LATTICE3:17 .= x"\/"((z"/\"x)"\/"(z"/\"y)) by LATTICE3:14 .= x"\/"((x"\/"y)"/\"z) by A1,Def3 .= ((x"\/"y)"/\"x)"\/"((x"\/"y)"/\"z) by LATTICE3:18 .= (x"\/"y)"/\"(x"\/"z) by A1,Def3; end; assume A2: for x,y,z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z); let x,y,z be Element of L; thus x"/\"(y"\/"z) = (x"/\"(x"\/"z))"/\"(y"\/"z) by LATTICE3:18 .= x"/\"((z"\/"x)"/\"(y"\/"z)) by LATTICE3:16 .= x"/\"(z"\/"(x"/\"y)) by A2 .= ((y"/\"x)"\/"x)"/\"((x"/\"y)"\/"z) by LATTICE3:17 .= (x"/\"y)"\/"(x"/\"z) by A2; end; definition let X be set; cluster BoolePoset X -> distributive; coherence proof let x,y,z be Element of BoolePoset X; thus x"/\"(y"\/"z) = x /\ (y"\/"z) by YELLOW_1:17 .= x /\ (y \/ z) by YELLOW_1:17 .= x/\y \/ x/\z by XBOOLE_1:23 .= (x"/\"y)\/(x/\z) by YELLOW_1:17 .= (x"/\"y)\/(x"/\"z) by YELLOW_1:17 .= (x"/\"y)"\/"(x"/\"z) by YELLOW_1:17; end; end; definition let S be non empty RelStr, X be set; pred ex_min_of X,S means ex_inf_of X,S & "/\"(X,S) in X; synonym X has_the_min_in S; pred ex_max_of X,S means :Def5: ex_sup_of X,S & "\/"(X,S) in X; synonym X has_the_max_in S; end; definition let S be non empty RelStr, s be Element of S, X be set; pred s is_minimum_of X means :Def6: ex_inf_of X,S & s = "/\"(X,S) & "/\"(X,S) in X; pred s is_maximum_of X means :Def7: ex_sup_of X,S & s = "\/"(X,S) & "\/"(X,S)in X; end; definition let L be RelStr; cluster id L -> isomorphic; coherence proof per cases; suppose A1: L is non empty; A2: id L = id the carrier of L by GRCAT_1:def 11; then A3: id L is one-to-one; A4: id L is monotone by A1,YELLOW_2:13; A6: id L = (id L)" by A2,FUNCT_1:67; thus thesis by A1,A3,A4,A6,WAYBEL_0:def 38; suppose L is empty; hence thesis by WAYBEL_0:def 38; end; end; definition let L1,L2 be RelStr; pred L1,L2 are_isomorphic means :Def8: ex f being map of L1,L2 st f is isomorphic; reflexivity proof let L be RelStr; take id L; thus thesis; end; end; theorem for L1,L2 be non empty RelStr st L1,L2 are_isomorphic holds L2,L1 are_isomorphic proof let L1,L2 be non empty RelStr; given f being map of L1,L2 such that A1: f is isomorphic; consider g being map of L2,L1 such that A2: g = (f qua Function)" and A3: g is monotone by A1,WAYBEL_0:def 38; A4: f is one-to-one by A1,WAYBEL_0:def 38; then A5: g is one-to-one by A2,FUNCT_1:62; A6: f is monotone by A1,WAYBEL_0:def 38; f = (g qua Function)" by A2,A4,FUNCT_1:65; then g is isomorphic by A3,A5,A6,WAYBEL_0:def 38; hence thesis by Def8; end; theorem for L1,L2,L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds L1,L3 are_isomorphic proof let L1,L2,L3 be RelStr; given f1 being map of L1,L2 such that A1: f1 is isomorphic; given f2 being map of L2,L3 such that A2: f2 is isomorphic; A3: now assume L1 is empty; then the carrier of L1 is empty by STRUCT_0:def 1; then f2*f1 is Function of the carrier of L1,the carrier of L3 by FUNCT_2:19; hence f2*f1 is map of L1,L3; end; per cases; suppose L1 is non empty & L2 is non empty & L3 is non empty; then reconsider L1,L2,L3 as non empty RelStr; reconsider f1 as map of L1,L2; reconsider f2 as map of L2,L3; consider g1 being map of L2,L1 such that A4: g1 = (f1 qua Function)" and A5: g1 is monotone by A1,WAYBEL_0:def 38; A6: f1 is one-to-one by A1,WAYBEL_0:def 38; A7: f1 is monotone by A1,WAYBEL_0:def 38; consider g2 being map of L3,L2 such that A8: g2 = (f2 qua Function)" and A9: g2 is monotone by A2,WAYBEL_0:def 38; A10: f2 is one-to-one by A2,WAYBEL_0:def 38; A11: f2 is monotone by A2,WAYBEL_0:def 38; A12: f2*f1 is one-to-one by A6,A10,FUNCT_1:46; A13: f2*f1 is monotone by A7,A11,YELLOW_2:14; A14: g1*g2 is monotone by A5,A9,YELLOW_2:14; g1*g2 = ((f2*f1) qua Function)" by A4,A6,A8,A10,FUNCT_1:66; then f2*f1 is isomorphic by A12,A13,A14,WAYBEL_0:def 38; hence thesis by Def8; suppose A15: L1 is empty; then L2 is empty by A1,WAYBEL_0:def 38; then A16: L3 is empty by A2,WAYBEL_0:def 38; reconsider f = f2*f1 as map of L1,L3 by A3,A15; f is isomorphic by A15,A16,WAYBEL_0:def 38; hence thesis by Def8; suppose A17: L2 is empty; then A18: L1 is empty & L3 is empty by A1,A2,WAYBEL_0:def 38; reconsider f = f2*f1 as map of L1,L3 by A1,A3,A17,WAYBEL_0:def 38; f is isomorphic by A18,WAYBEL_0:def 38; hence thesis by Def8; suppose A19: L3 is empty; then A20: L2 is empty by A2,WAYBEL_0:def 38; then A21: L1 is empty by A1,WAYBEL_0:def 38; reconsider f = f2*f1 as map of L1,L3 by A1,A3,A20,WAYBEL_0:def 38; f is isomorphic by A19,A21,WAYBEL_0:def 38; hence thesis by Def8; end; begin :: Galois Connections definition let S,T be RelStr; mode Connection of S,T -> set means :Def9: ex g being map of S,T, d being map of T,S st it = [g,d]; existence proof consider g being map of S,T, d being map of T,S; take [g,d]; thus thesis; end; end; definition let S,T be RelStr, g be map of S,T, d be map of T,S; redefine func [g,d] -> Connection of S,T; coherence by Def9; end; :: Definition 3.1 definition let S,T be non empty RelStr, gc be Connection of S,T; attr gc is Galois means :Def10: ex g being map of S,T, d being map of T,S st gc = [g,d] & g is monotone & d is monotone & for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s; end; theorem Th9: for S,T being non empty Poset,g being map of S,T, d being map of T,S holds [g,d] is Galois iff g is monotone & d is monotone & for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; hereby assume [g,d] is Galois; then consider g' being map of S,T, d' being map of T,S such that A1: [g,d] = [g',d'] and A2: g' is monotone & d' is monotone & for t being Element of T, s being Element of S holds t <= g'.s iff d'.t <= s by Def10; g = g' & d = d' by A1,ZFMISC_1:33; hence g is monotone & d is monotone & for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s by A2; end; thus thesis by Def10; end; :: Definition 3.1 definition let S,T be non empty RelStr, g be map of S,T; attr g is upper_adjoint means :Def11: ex d being map of T,S st [g,d] is Galois; synonym g has_a_lower_adjoint; end; :: Definition 3.1 definition let S,T be non empty RelStr, d be map of T,S; attr d is lower_adjoint means :Def12: ex g being map of S,T st [g,d] is Galois; synonym d has_an_upper_adjoint; end; theorem Th10: for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds g is upper_adjoint & d is lower_adjoint proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume A1: [g,d] is Galois; hence ex d being map of T,S st [g,d] is Galois; thus ex g being map of S,T st [g,d] is Galois by A1; end; :: Theorem 3.2 (1) iff (2) theorem Th11: for S,T being non empty Poset,g being map of S,T, d being map of T,S holds [g,d] is Galois iff g is monotone & for t being Element of T holds d.t is_minimum_of g"(uparrow t) proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; hereby assume A1: [g,d] is Galois; hence g is monotone by Th9; let t be Element of T; thus d.t is_minimum_of g"(uparrow t) proof set X = g"(uparrow t); A2: d.t is_<=_than X proof let s be Element of S; assume s in X; then g.s in uparrow t by FUNCT_1:def 13; then t <= g.s by WAYBEL_0:18; hence d.t <= s by A1,Th9; end; t <= g.(d.t) by A1,Th9; then g.(d.t) in uparrow t by WAYBEL_0:18; then A3: d.t in X by FUNCT_2:46; then A4: for s being Element of S st s is_<=_than X holds d.t >= s by LATTICE3:def 8; hence ex_inf_of X,S & d.t = inf X by A2,YELLOW_0:31; thus inf X in X by A2,A3,A4,YELLOW_0:31; end; end; assume that A5: g is monotone and A6: for t being Element of T holds d.t is_minimum_of g"(uparrow t); A7: d is monotone proof let t1,t2 be Element of T; assume A8: t1 <= t2; A9: d.t1 is_minimum_of g"(uparrow t1) by A6; then A10: ex_inf_of g"(uparrow t1),S by Def6; A11: d.t2 is_minimum_of g"(uparrow t2) by A6; then A12: ex_inf_of g"(uparrow t2),S by Def6; uparrow t2 c= uparrow t1 by A8,WAYBEL_0:22; then g"(uparrow t2) c= g"(uparrow t1) by RELAT_1:178; then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A10,A12,YELLOW_0:35; then d.t1 <= inf (g"(uparrow t2)) by A9,Def6; hence d.t1 <= d.t2 by A11,Def6; end; for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s proof let t be Element of T, s be Element of S; set X = g"(uparrow t); A13: d.t is_minimum_of X by A6; hereby assume t <= g.s; then g.s in uparrow t by WAYBEL_0:18; then A14: s in X by FUNCT_2:46; A15: d.t is_minimum_of g"(uparrow t) by A6; then ex_inf_of X,S by Def6; then X is_>=_than inf X by YELLOW_0:def 10; then s >= inf X by A14,LATTICE3:def 8; hence d.t <= s by A15,Def6; end; assume d.t <= s; then A16: g.(d.t) <= g.s by A5,Def2; inf X in X by A13,Def6; then g.(inf X) in uparrow t by FUNCT_1:def 13; then g.(inf X) >= t by WAYBEL_0:18; then g.(d.t) >= t by A13,Def6; hence t <= g.s by A16,ORDERS_1:26; end; hence thesis by A5,A7,Th9; end; :: Theorem 3.2 (1) iff (3) theorem Th12: for S,T being non empty Poset,g being map of S,T, d being map of T,S holds [g,d] is Galois iff d is monotone & for s being Element of S holds g.s is_maximum_of d"(downarrow s) proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; hereby assume A1: [g,d] is Galois; hence d is monotone by Th9; let s be Element of S; thus g.s is_maximum_of d"(downarrow s) proof set X = d"(downarrow s); A2: g.s is_>=_than X proof let t be Element of T; assume t in X; then d.t in downarrow s by FUNCT_1:def 13; then s >= d.t by WAYBEL_0:17; hence g.s >= t by A1,Th9; end; s >= d.(g.s) by A1,Th9; then d.(g.s) in downarrow s by WAYBEL_0:17; then A3: g.s in X by FUNCT_2:46; then A4: for t being Element of T st t is_>=_than X holds g.s <= t by LATTICE3:def 9; hence ex_sup_of X,T & g.s = sup X by A2,YELLOW_0:30; thus sup X in X by A2,A3,A4,YELLOW_0:30; end; end; assume that A5: d is monotone and A6: for s being Element of S holds g.s is_maximum_of d"(downarrow s); A7: g is monotone proof let s1,s2 be Element of S; assume A8: s1 <= s2; A9: g.s1 is_maximum_of d"(downarrow s1) by A6; then A10: ex_sup_of d"(downarrow s1),T by Def7; A11: g.s2 is_maximum_of d"(downarrow s2) by A6; then A12: ex_sup_of d"(downarrow s2),T by Def7; downarrow s1 c= downarrow s2 by A8,WAYBEL_0:21; then d"(downarrow s1) c= d"(downarrow s2) by RELAT_1:178; then sup (d"(downarrow s1)) <= sup (d"(downarrow s2)) by A10,A12,YELLOW_0:34; then g.s1 <= sup (d"(downarrow s2)) by A9,Def7; hence g.s1 <= g.s2 by A11,Def7; end; for t being Element of T, s being Element of S holds s >= d.t iff g.s >= t proof let t be Element of T, s be Element of S; set X = d"(downarrow s); A13: g.s is_maximum_of X by A6; hereby assume s >= d.t; then d.t in downarrow s by WAYBEL_0:17; then A14: t in X by FUNCT_2:46; ex_sup_of X,T by A13,Def7; then X is_<=_than sup X by YELLOW_0:def 9; then t <= sup X by A14,LATTICE3:def 9; hence g.s >= t by A13,Def7; end; assume g.s >= t; then A15: d.(g.s) >= d.t by A5,Def2; sup X in X by A13,Def7; then d.(sup X) in downarrow s by FUNCT_1:def 13; then d.(sup X) <= s by WAYBEL_0:17; then d.(g.s) <= s by A13,Def7; hence s >= d.t by A15,ORDERS_1:26; end; hence thesis by A5,A7,Th9; end; :: Theorem 3.3 (first part) theorem Th13: for S,T being non empty Poset,g being map of S,T st g is upper_adjoint holds g is infs-preserving proof let S,T be non empty Poset,g be map of S,T; given d being map of T,S such that A1: [g,d] is Galois; let X be Subset of S; assume A2: ex_inf_of X,S; set s = inf X; A3: g.s is_<=_than g.:X proof let t be Element of T; A4: g is monotone by A1,Th9; A5: s is_<=_than X by A2,YELLOW_0:31; assume t in g.:X; then consider si being Element of S such that A6: si in X and A7: t = g.si by FUNCT_2:116; reconsider si as Element of S; s <= si by A5,A6,LATTICE3:def 8; hence g.s <= t by A4,A7,Def2; end; for t being Element of T st t is_<=_than g.:X holds g.s >= t proof let t be Element of T; assume A8: t is_<=_than g.:X; d.t is_<=_than X proof let si be Element of S; assume si in X; then g.si in g.:X by FUNCT_2:43; then t <= g.si by A8,LATTICE3:def 8; hence d.t <= si by A1,Th9; end; then d.t <= s by A2,YELLOW_0:31; hence g.s >= t by A1,Th9; end; hence thesis by A3,YELLOW_0:31; end; definition let S,T be non empty Poset; cluster upper_adjoint -> infs-preserving map of S,T; coherence by Th13; end; :: Theorem 3.3 (second part) theorem Th14: for S,T being non empty Poset, d being map of T,S st d is lower_adjoint holds d is sups-preserving proof let S,T be non empty Poset, d be map of T,S; given g being map of S,T such that A1: [g,d] is Galois; let X be Subset of T; assume A2: ex_sup_of X,T; set t = sup X; A3: d.t is_>=_than d.:X proof let s be Element of S; A4: d is monotone by A1,Th9; A5: t is_>=_than X by A2,YELLOW_0:30; assume s in d.:X; then consider ti being Element of T such that A6: ti in X and A7: s = d.ti by FUNCT_2:116; reconsider ti as Element of T; t >= ti by A5,A6,LATTICE3:def 9; hence d.t >= s by A4,A7,Def2; end; for s being Element of S st s is_>=_than d.:X holds d.t <= s proof let s be Element of S; assume A8: s is_>=_than d.:X; g.s is_>=_than X proof let ti be Element of T; assume ti in X; then d.ti in d.:X by FUNCT_2:43; then s >= d.ti by A8,LATTICE3:def 9; hence g.s >= ti by A1,Th9; end; then g.s >= t by A2,YELLOW_0:30; hence d.t <= s by A1,Th9; end; hence thesis by A3,YELLOW_0:30; end; definition let S,T be non empty Poset; cluster lower_adjoint -> sups-preserving map of S,T; coherence by Th14; end; :: Theorem 3.4 theorem Th15: for S,T being non empty Poset,g being map of S,T st S is complete & g is infs-preserving ex d being map of T,S st [g,d] is Galois & for t being Element of T holds d.t is_minimum_of g"(uparrow t) proof let S,T be non empty Poset,g be map of S,T; assume that A1: S is complete and A2: g is infs-preserving; defpred P[set,set] means ex t being Element of T st t = $1 & $2 = inf (g"(uparrow t)); A3: for e being set st e in the carrier of T ex u being set st u in the carrier of S & P[e,u] proof let e be set; assume e in the carrier of T; then reconsider t = e as Element of T; take inf (g"(uparrow t)); thus thesis; end; consider d being Function of the carrier of T, the carrier of S such that A4: for e being set st e in the carrier of T holds P[e,d.e] from FuncEx1(A3); A5: for t being Element of T holds d.t = inf (g"(uparrow t)) proof let t be Element of T; ex t1 being Element of T st t1 = t & d.t = inf (g"(uparrow t1)) by A4; hence thesis; end; reconsider d as map of T,S; take d; for X being Filter of S holds g preserves_inf_of X by A2,WAYBEL_0:def 32; then A6: g is monotone by WAYBEL_0:69; A7: d is monotone proof let t1,t2 be Element of T; A8: ex_inf_of g"(uparrow t1),S by A1,YELLOW_0:17; A9: ex_inf_of g"(uparrow t2),S by A1,YELLOW_0:17; assume t1 <= t2; then uparrow t2 c= uparrow t1 by WAYBEL_0:22; then g"(uparrow t2) c= g"(uparrow t1) by RELAT_1:178; then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A8,A9,YELLOW_0:35; then d.t1 <= inf (g"(uparrow t2)) by A5; hence d.t1 <= d.t2 by A5; end; for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s proof let t be Element of T, s be Element of S; A10: ex_inf_of g"(uparrow t),S by A1,YELLOW_0:17; then inf (g"(uparrow t)) is_<=_than g"(uparrow t) by YELLOW_0:31; then A11: d.t is_<=_than g"(uparrow t) by A5; hereby assume t <= g.s; then g.s in uparrow t by WAYBEL_0:18; then s in g"(uparrow t) by FUNCT_2:46; hence d.t <= s by A11,LATTICE3:def 8; end; assume d.t <= s; then g.(d.t) <= g.s by A6,Def2; then A12: g.(inf (g"(uparrow t))) <= g.s by A5; g preserves_inf_of (g"(uparrow t)) by A2,WAYBEL_0:def 32; then A13: ex_inf_of g.:(g"(uparrow t)),T & g.(inf (g"(uparrow t))) = inf (g.:(g"(uparrow t))) by A10,WAYBEL_0:def 30; A14: ex_inf_of uparrow t,T by WAYBEL_0:39; g.:(g"(uparrow t)) c= uparrow t by FUNCT_1:145; then g.(inf (g"(uparrow t))) >= inf(uparrow t) by A13,A14,YELLOW_0:35; then g.(inf (g"(uparrow t))) >= t by WAYBEL_0:39; hence t <= g.s by A12,ORDERS_1:26; end; hence [g,d] is Galois by A6,A7,Th9; let t be Element of T; thus A15: ex_inf_of g"(uparrow t),S by A1,YELLOW_0:17; thus A16: d.t = inf (g"(uparrow t)) by A5; g preserves_inf_of (g"(uparrow t)) by A2,WAYBEL_0:def 32; then A17: ex_inf_of g.:(g"(uparrow t)),T & g.(inf (g"(uparrow t))) = inf (g.:(g"(uparrow t))) by A15,WAYBEL_0:def 30; A18: ex_inf_of uparrow t,T by WAYBEL_0:39; g.:(g"(uparrow t)) c= uparrow t by FUNCT_1:145; then g.(inf (g"(uparrow t))) >= inf(uparrow t) by A17,A18,YELLOW_0:35; then g.(inf (g"(uparrow t))) >= t by WAYBEL_0:39; then g.(d.t) >= t by A5; then g.(d.t) in uparrow t by WAYBEL_0:18; hence inf (g"(uparrow t)) in g"(uparrow t) by A16,FUNCT_2:46; end; :: Theorem 3.4 (dual) theorem Th16: for S,T being non empty Poset, d being map of T,S st T is complete & d is sups-preserving ex g being map of S,T st [g,d] is Galois & for s being Element of S holds g.s is_maximum_of d"(downarrow s) proof let S,T be non empty Poset, d be map of T,S; assume that A1: T is complete and A2: d is sups-preserving; defpred P[set,set] means ex s being Element of S st s = $1 & $2 = sup (d"(downarrow s)); A3: for e being set st e in the carrier of S ex u being set st u in the carrier of T & P[e,u] proof let e be set; assume e in the carrier of S; then reconsider s = e as Element of S; take sup (d"(downarrow s)); thus thesis; end; consider g being Function of the carrier of S, the carrier of T such that A4: for e being set st e in the carrier of S holds P[e,g.e] from FuncEx1(A3); A5: for s being Element of S holds g.s = sup (d"(downarrow s)) proof let s be Element of S; ex s1 being Element of S st s1 = s & g.s = sup (d"(downarrow s1)) by A4 ; hence thesis; end; reconsider g as map of S,T; take g; for X being Ideal of T holds d preserves_sup_of X by A2,WAYBEL_0:def 33; then A6: d is monotone by WAYBEL_0:72; A7: g is monotone proof let s1,s2 be Element of S; A8: ex_sup_of d"(downarrow s1),T by A1,YELLOW_0:17; A9: ex_sup_of d"(downarrow s2),T by A1,YELLOW_0:17; assume s1 <= s2; then downarrow s1 c= downarrow s2 by WAYBEL_0:21; then d"(downarrow s1) c= d"(downarrow s2) by RELAT_1:178; then sup (d"(downarrow s1)) <= sup (d"(downarrow s2)) by A8,A9,YELLOW_0:34; then g.s1 <= sup (d"(downarrow s2)) by A5; hence g.s1 <= g.s2 by A5; end; for t being Element of T, s being Element of S holds s >= d.t iff g.s >= t proof let t be Element of T, s be Element of S; A10: ex_sup_of d"(downarrow s),T by A1,YELLOW_0:17; then sup (d"(downarrow s)) is_>=_than d"(downarrow s) by YELLOW_0:30; then A11: g.s is_>=_than d"(downarrow s) by A5; hereby assume s >= d.t; then d.t in downarrow s by WAYBEL_0:17; then t in d"(downarrow s) by FUNCT_2:46; hence g.s >= t by A11,LATTICE3:def 9; end; assume g.s >= t; then d.(g.s) >= d.t by A6,Def2; then A12: d.(sup (d"(downarrow s))) >= d.t by A5; d preserves_sup_of (d"(downarrow s)) by A2,WAYBEL_0:def 33; then A13: ex_sup_of d.:(d"(downarrow s)),S & d.(sup (d"(downarrow s))) = sup (d.:(d"(downarrow s))) by A10,WAYBEL_0:def 31; A14: ex_sup_of downarrow s,S by WAYBEL_0:34; d.:(d"(downarrow s)) c= downarrow s by FUNCT_1:145; then d.(sup (d"(downarrow s))) <= sup(downarrow s) by A13,A14,YELLOW_0:34; then d.(sup (d"(downarrow s))) <= s by WAYBEL_0:34; hence s >= d.t by A12,ORDERS_1:26; end; hence [g,d] is Galois by A6,A7,Th9; let s be Element of S; thus A15: ex_sup_of d"(downarrow s),T by A1,YELLOW_0:17; thus A16: g.s = sup (d"(downarrow s)) by A5; d preserves_sup_of (d"(downarrow s)) by A2,WAYBEL_0:def 33; then A17: ex_sup_of d.:(d"(downarrow s)),S & d.(sup (d"(downarrow s))) = sup (d.:(d"(downarrow s))) by A15,WAYBEL_0:def 31; A18: ex_sup_of downarrow s,S by WAYBEL_0:34; d.:(d"(downarrow s)) c= downarrow s by FUNCT_1:145; then d.(sup (d"(downarrow s))) <= sup(downarrow s) by A17,A18,YELLOW_0:34; then d.(sup (d"(downarrow s))) <= s by WAYBEL_0:34; then d.(g.s) <= s by A5; then d.(g.s) in downarrow s by WAYBEL_0:17; hence sup (d"(downarrow s)) in d"(downarrow s) by A16,FUNCT_2:46; end; :: Corollary 3.5 (i) theorem for S,T being non empty Poset, g being map of S,T st S is complete holds (g is infs-preserving iff g is monotone & g has_a_lower_adjoint) proof let S,T be non empty Poset,g be map of S,T; assume A1: S is complete; hereby assume g is infs-preserving; then ex d being map of T,S st[g,d] is Galois & for t being Element of T holds d.t is_minimum_of g"(uparrow t) by A1,Th15; hence g is monotone & g has_a_lower_adjoint by Def11,Th11; end; assume g is monotone; assume ex d being map of T,S st [g,d] is Galois; then g is upper_adjoint by Def11; hence g is infs-preserving by Th13; end; :: Corollary 3.5 (ii) theorem Th18: for S,T being non empty Poset, d being map of T,S st T is complete holds d is sups-preserving iff d is monotone & d has_an_upper_adjoint proof let S,T be non empty Poset, d be map of T,S; assume A1: T is complete; hereby assume d is sups-preserving; then ex g being map of S,T st [g,d] is Galois & for s being Element of S holds g.s is_maximum_of d"(downarrow s) by A1,Th16; hence d is monotone & d has_an_upper_adjoint by Def12,Th12; end; assume d is monotone; assume ex g being map of S,T st [g,d] is Galois; then d is lower_adjoint by Def12; hence d is sups-preserving by Th14; end; :: Theorem 3.6 (1) iff (2) theorem Th19: for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds d*g <= id S & id T <= g*d proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume A1: [g,d] is Galois; for s being Element of S holds (d*g).s <= (id S).s proof let s be Element of S; d.(g.s) <= s by A1,Th9; then (d*g).s <= s by FUNCT_2:21; hence thesis by TMAP_1:91; end; hence d*g <= id S by YELLOW_2:10; for t being Element of T holds (id T).t <= (g*d).t proof let t be Element of T; t <= g.(d.t) by A1,Th9; then t <= (g*d).t by FUNCT_2:21; hence thesis by TMAP_1:91; end; hence id T <= g*d by YELLOW_2:10; end; :: Theorem 3.6 (2) implies (1) theorem Th20: for S,T being non empty Poset,g being map of S,T, d being map of T,S st g is monotone & d is monotone & d*g <= id S & id T <= g*d holds [g,d] is Galois proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume that A1: g is monotone and A2: d is monotone and A3: d*g <= id S and A4: id T <= g*d; for t being Element of T, s being Element of S holds t <= g.s iff d.t <= s proof let t be Element of T, s be Element of S; hereby assume t <= g.s; then A5: d.t <= d.(g.s) by A2,Def2; (d*g).s <= (id S).s by A3,YELLOW_2:10; then d.(g.s) <= (id S).s by FUNCT_2:21; then d.(g.s) <= s by TMAP_1:91; hence d.t <= s by A5,ORDERS_1:26; end; assume d.t <= s; then A6: g.(d.t) <= g.s by A1,Def2; (id T).t <= (g*d).t by A4,YELLOW_2:10; then (id T).t <= g.(d.t) by FUNCT_2:21; then t <= g.(d.t) by TMAP_1:91; hence t <= g.s by A6,ORDERS_1:26; end; hence [g,d] is Galois by A1,A2,Th9; end; :: Theorem 3.6 (2) implies (3) theorem Th21: for S,T being non empty Poset,g being map of S,T, d being map of T,S st g is monotone & d is monotone & d*g <= id S & id T <= g*d holds d = d*g*d & g = g*d*g proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume that A1: g is monotone and A2: d is monotone and A3: d*g <= id S and A4: id T <= g*d; for t being Element of T holds d.t = (d*g*d).t proof let t be Element of T; (id T).t <= (g*d).t by A4,YELLOW_2:10; then t <= (g*d).t by TMAP_1:91; then d.t <= d.((g*d).t) by A2,Def2; then d.t <= (d*(g*d)).t by FUNCT_2:21; then A5: d.t <= (d*g*d).t by RELAT_1:55; (d*g).(d.t) <= (id S).(d.t) by A3,YELLOW_2:10; then (d*g).(d.t) <= d.t by TMAP_1:91; then d.t >= (d*g*d).t by FUNCT_2:21; hence thesis by A5,ORDERS_1:25; end; hence d = d*g*d by YELLOW_2:9; for s being Element of S holds g.s = (g*d*g).s proof let s be Element of S; (id T).(g.s) <= (g*d).(g.s) by A4,YELLOW_2:10; then (g.s) <= (g*d).(g.s) by TMAP_1:91; then A6: g.s <= (g*d*g).s by FUNCT_2:21; (d*g).s <= (id S).s by A3,YELLOW_2:10; then (d*g).s <= s by TMAP_1:91; then g.((d*g).s) <= g.s by A1,Def2; then (g*(d*g)).s <= g.s by FUNCT_2:21; then g.s >= (g*d*g).s by RELAT_1:55; hence thesis by A6,ORDERS_1:25; end; hence g = g*d*g by YELLOW_2:9; end; :: Theorem 3.6 (3) implies (4) theorem Th22: for S,T being non empty RelStr, g being map of S,T, d being map of T,S st d = d*g*d & g = g*d*g holds g*d is idempotent & d*g is idempotent proof let S,T be non empty RelStr, g be map of S,T, d be map of T,S; assume A1: d = d*g*d; assume g = g*d*g; hence (g*d)*(g*d) = g*d by RELAT_1:55; thus (d*g)*(d*g) = d*g by A1,RELAT_1:55; end; :: Proposition 3.7 (1) implies (2) theorem Th23: for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois & g is onto for t being Element of T holds d.t is_minimum_of g"{t} proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume that A1: [g,d] is Galois and A2: g is onto; let t be Element of T; A3: d.t is_minimum_of g"(uparrow t) by A1,Th11; then A4: d.t = inf (g"(uparrow t)) by Def6; A5: rng g = the carrier of T by A2,FUNCT_2:def 3; then A6: g.:(g"(uparrow t)) = uparrow t by FUNCT_1:147; consider s being set such that A7: s in the carrier of S and A8: g.s = t by A5,FUNCT_2:17; reconsider s as Element of S by A7; ex_inf_of g"(uparrow t),S by A3,Def6; then A9: d.t is_<=_than g"(uparrow t) by A4,YELLOW_0:31; A10: g is monotone by A1,Th9; {t} c= uparrow {t} by WAYBEL_0:16; then A11: {t} c= uparrow t by WAYBEL_0:def 18; then A12: g"{t} c= g"(uparrow t) by RELAT_1:178; A13: t in {t} by TARSKI:def 1; then s in g"(uparrow t) by A8,A11,FUNCT_2:46; then d.t <= s by A9,LATTICE3:def 8; then A14: g.(d.t) <= t by A8,A10,Def2; d.t in g"(uparrow t) by A3,A4,Def6; then g.(d.t) in g.:(g"(uparrow t)) by FUNCT_2:43; then t <= g.(d.t) by A6,WAYBEL_0:18; then A15: g.(d.t) = t by A14,ORDERS_1:25; A16: ex_inf_of g"(uparrow t),S by A3,Def6; A17: d.t in g"{t} by A13,A15,FUNCT_2:46; thus A18: ex_inf_of g"{t},S proof take d.t; thus A19: g"{t} is_>=_than d.t by A9,A12,YELLOW_0:9; thus for b be Element of S st g"{t} is_>=_than b holds b <= d.t by A17,LATTICE3:def 8; let c be Element of S; assume g"{t} is_>=_than c; then A20: c <= d.t by A17,LATTICE3:def 8; assume for b being Element of S st g"{t} is_>=_than b holds b <= c; then d.t <= c by A19; hence c = d.t by A20,ORDERS_1:25; end; then A21: inf (g"{t}) >= d.t by A4,A12,A16,YELLOW_0:35; inf (g"{t}) is_<=_than g"{t} by A18,YELLOW_0:31; then inf (g"{t}) <= d.t by A17,LATTICE3:def 8; hence d.t = inf(g"{t}) by A21,ORDERS_1:25; hence inf(g"{t}) in g"{t} by A13,A15,FUNCT_2:46; end; :: Proposition 3.7 (2) implies (3) theorem Th24: for S,T being non empty Poset,g being map of S,T, d being map of T,S st for t being Element of T holds d.t is_minimum_of g"{t} holds g*d = id T proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume A1: for t being Element of T holds d.t is_minimum_of g"{t}; for t being Element of T holds (g*d).t = t proof let t be Element of T; d.t is_minimum_of g"{t} by A1; then d.t = inf(g"{t}) & inf(g"{t}) in g"{t} by Def6; then g.(d.t) in {t} by FUNCT_2:46; then g.(d.t) = t by TARSKI:def 1; hence (g*d).t = t by FUNCT_2:21; end; hence g*d = id T by Th1; end; :: Proposition 3.7 (3) implies (4) theorem Th25: for L1,L2 being non empty 1-sorted, g1 being map of L1,L2, g2 being map of L2,L1 st g2*g1 = id L1 holds g1 is one-to-one & g2 is onto proof let L1,L2 be non empty 1-sorted; let g1 be map of L1,L2, g2 be map of L2,L1; assume g2*g1 = id L1; then A1: g2*g1 = id the carrier of L1 by GRCAT_1:def 11; hence g1 is one-to-one by FUNCT_2:29; rng g2 = the carrier of L1 by A1,FUNCT_2:29; hence g2 is onto by FUNCT_2:def 3; end; :: Proposition 3.7 (4) iff (1) theorem for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds g is onto iff d is one-to-one proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume A1: [g,d] is Galois; hereby assume g is onto; then for t being Element of T holds d.t is_minimum_of g"{t} by A1,Th23; then g*d = id T by Th24; hence d is one-to-one by Th25; end; assume A2: d is one-to-one; A3: the carrier of T = dom d & the carrier of T = dom (g*d) & rng (g*d) c= the carrier of T by FUNCT_2:def 1; A4: g is monotone & d is monotone by A1,Th9; d*g <= id S & id T <= g*d by A1,Th19; then d = d*g*d by A4,Th21 .= d*(g*d) by RELAT_1:55; then g*d = id (the carrier of T) by A2,A3,FUNCT_1:50 .= id T by GRCAT_1:def 11; hence g is onto by Th25; end; :: Proposition 3.7 (1*) implies (2*) theorem Th27: for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois & d is onto for s being Element of S holds g.s is_maximum_of d"{s} proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume that A1: [g,d] is Galois and A2: d is onto; let s be Element of S; A3: g.s is_maximum_of (d"(downarrow s)) by A1,Th12; then A4: g.s = sup (d"(downarrow s)) by Def7; A5: rng d = the carrier of S by A2,FUNCT_2:def 3; then A6: d.:(d"(downarrow s)) = downarrow s by FUNCT_1:147; consider t being set such that A7: t in the carrier of T and A8: d.t = s by A5,FUNCT_2:17; reconsider t as Element of T by A7; ex_sup_of d"(downarrow s),T by A3,Def7; then A9: g.s is_>=_than d"(downarrow s) by A4,YELLOW_0:30; A10: d is monotone by A1,Th9; {s} c= downarrow {s} by WAYBEL_0:16; then A11: {s} c= downarrow s by WAYBEL_0:def 17; then A12: d"{s} c= d"(downarrow s) by RELAT_1:178; A13: s in {s} by TARSKI:def 1; then t in d"(downarrow s) by A8,A11,FUNCT_2:46; then g.s >= t by A9,LATTICE3:def 9; then A14: d.(g.s) >= s by A8,A10,Def2; g.s in d"(downarrow s) by A3,A4,Def7; then d.(g.s) in d.:(d"(downarrow s)) by FUNCT_2:43; then s >= d.(g.s) by A6,WAYBEL_0:17; then A15: d.(g.s) = s by A14,ORDERS_1:25; A16: ex_sup_of d"(downarrow s),T by A3,Def7; A17: g.s in d"{s} by A13,A15,FUNCT_2:46; thus A18: ex_sup_of d"{s},T proof take g.s; thus A19: d"{s} is_<=_than g.s by A9,A12,YELLOW_0:9; thus for b be Element of T st d"{s} is_<=_than b holds b >= g.s by A17,LATTICE3:def 9; let c be Element of T; assume d"{s} is_<=_than c; then A20: c >= g.s by A17,LATTICE3:def 9; assume for b being Element of T st d"{s} is_<=_than b holds b >= c; then g.s >= c by A19; hence c = g.s by A20,ORDERS_1:25; end; then A21: sup (d"{s}) <= g.s by A4,A12,A16,YELLOW_0:34; sup (d"{s}) is_>=_than d"{s} by A18,YELLOW_0:30; then sup (d"{s}) >= g.s by A17,LATTICE3:def 9; hence g.s = sup(d"{s}) by A21,ORDERS_1:25; hence sup(d"{s}) in d"{s} by A13,A15,FUNCT_2:46; end; :: Proposition 3.7 (2*) implies (3*) theorem Th28: for S,T being non empty Poset,g being map of S,T, d being map of T,S st for s being Element of S holds g.s is_maximum_of d"{s} holds d*g = id S proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume A1: for s being Element of S holds g.s is_maximum_of d"{s}; for s being Element of S holds (d*g).s = s proof let s be Element of S; g.s is_maximum_of d"{s} by A1; then g.s = sup(d"{s}) & sup(d"{s}) in d"{s} by Def7; then d.(g.s) in {s} by FUNCT_2:46; then d.(g.s) = s by TARSKI:def 1; hence (d*g).s = s by FUNCT_2:21; end; hence d*g = id S by Th1; end; :: Proposition 3.7 (1*) iff (4*) theorem for S,T being non empty Poset,g being map of S,T, d being map of T,S st [g,d] is Galois holds g is one-to-one iff d is onto proof let S,T be non empty Poset,g be map of S,T, d be map of T,S; assume A1: [g,d] is Galois; hereby assume A2: g is one-to-one; A3: the carrier of S = dom g & the carrier of S = dom (d*g) & rng (d*g) c= the carrier of S by FUNCT_2:def 1; A4: g is monotone & d is monotone by A1,Th9; d*g <= id S & id T <= g*d by A1,Th19; then g = g*d*g by A4,Th21 .= g*(d*g) by RELAT_1:55; then d*g = id (the carrier of S) by A2,A3,FUNCT_1:50 .= id S by GRCAT_1:def 11; hence d is onto by Th25; end; assume d is onto; then for s being Element of S holds g.s is_maximum_of d"{s} by A1,Th27; then d*g = id S by Th28; hence g is one-to-one by Th25; end; :: Definition 3.8 (i) definition let L be non empty RelStr, p be map of L,L; attr p is projection means :Def13: p is idempotent monotone; synonym p is_a_projection_operator; end; definition let L be non empty RelStr; cluster id L -> projection; coherence proof thus id L is idempotent by YELLOW_2:23; thus id L is monotone; end; end; definition let L be non empty RelStr; cluster projection map of L,L; existence proof take id L; thus thesis; end; end; :: Definition 3.8 (ii) definition let L be non empty RelStr, c be map of L,L; attr c is closure means :Def14: c is projection & id(L) <= c; synonym c is_a_closure_operator; end; definition let L be non empty RelStr; cluster closure -> projection map of L,L; coherence by Def14; end; Lm1: for L1,L2 being non empty RelStr, f being map of L1,L2 st L2 is reflexive holds f <= f proof let L1,L2 be non empty RelStr, f be map of L1,L2; assume L2 is reflexive; then for x be Element of L1 holds f.x <= f.x by ORDERS_1:24; hence thesis by YELLOW_2:10; end; definition let L be non empty reflexive RelStr; cluster closure map of L,L; existence proof take id L; thus id L is projection; thus thesis by Lm1; end; end; definition let L be non empty reflexive RelStr; cluster id L -> closure; coherence proof thus id L is projection; thus thesis by Lm1; end; end; :: Definition 3.8 (iii) definition let L be non empty RelStr, k be map of L,L; attr k is kernel means :Def15: k is projection & k <= id(L); synonym k is_a_kernel_operator; end; definition let L be non empty RelStr; cluster kernel -> projection map of L,L; coherence by Def15; end; definition let L be non empty reflexive RelStr; cluster kernel map of L,L; existence proof take id L; thus id L is projection; thus thesis by Lm1; end; end; definition let L be non empty reflexive RelStr; cluster id L -> kernel; coherence proof thus id L is projection; thus thesis by Lm1; end; end; Lm2: for L being non empty 1-sorted, p being map of L,L st p is idempotent for x being set st x in rng p holds p.x = x proof let L be non empty 1-sorted, p be map of L,L such that A1: p is idempotent; let x be set; assume x in rng p; then consider a being set such that A2: a in dom p and A3: x = p.a by FUNCT_1:def 5; a in the carrier of L by A2,FUNCT_2:def 1; then a is Element of L; hence p.x = x by A1,A3,YELLOW_2:20; end; theorem Th30: for L being non empty Poset, c being map of L,L, X being Subset of L st c is_a_closure_operator & ex_inf_of X,L & X c= rng c holds inf X = c.(inf X) proof let L be non empty Poset, c be map of L,L, X be Subset of L such that A1: c is_a_projection_operator and A2: id(L) <= c and A3: ex_inf_of X,L and A4: X c= rng c; A5: c is idempotent by A1,Def13; A6: c is monotone by A1,Def13; id(L).(inf X) <= c.(inf X) by A2,YELLOW_2:10; then A7: inf X <= c.(inf X) by TMAP_1:91; c.(inf X) is_<=_than X proof let x be Element of L; assume A8: x in X; inf X is_<=_than X by A3,YELLOW_0:31; then inf X <= x by A8,LATTICE3:def 8; then c.(inf X) <= c.x by A6,Def2; hence thesis by A4,A5,A8,Lm2; end; then c.(inf X) <= inf X by A3,YELLOW_0:31; hence thesis by A7,ORDERS_1:25; end; theorem Th31: for L being non empty Poset, k being map of L,L, X being Subset of L st k is_a_kernel_operator & ex_sup_of X,L & X c= rng k holds sup X = k.(sup X) proof let L be non empty Poset, k be map of L,L, X be Subset of L such that A1: k is_a_projection_operator and A2: k <= id(L) and A3: ex_sup_of X,L and A4: X c= rng k; A5: k is idempotent by A1,Def13; A6: k is monotone by A1,Def13; id(L).(sup X) >= k.(sup X) by A2,YELLOW_2:10; then A7: sup X >= k.(sup X) by TMAP_1:91; k.(sup X) is_>=_than X proof let x be Element of L; assume A8: x in X; sup X is_>=_than X by A3,YELLOW_0:30; then sup X >= x by A8,LATTICE3:def 9; then k.(sup X) >= k.x by A6,Def2; hence thesis by A4,A5,A8,Lm2; end; then k.(sup X) >= sup X by A3,YELLOW_0:30; hence thesis by A7,ORDERS_1:25; end; definition let L1, L2 be non empty RelStr, g be map of L1,L2; func corestr(g) -> map of L1,Image g equals :Def16: (the carrier of Image g)|g; coherence proof A1: the carrier of Image g = rng g by YELLOW_2:11; then (the carrier of Image g)|g = g & the carrier of L1 = dom g by FUNCT_2:def 1,RELAT_1:125; then (the carrier of Image g)|g is Function of the carrier of L1, the carrier of Image g by A1,FUNCT_2:3; hence thesis; end; end; theorem Th32: for L1, L2 being non empty RelStr,g being map of L1,L2 holds corestr g = g proof let L1, L2 be non empty RelStr, g be map of L1,L2; the carrier of Image g = rng g by YELLOW_2:11; then (the carrier of Image g)|g = g by RELAT_1:125; hence thesis by Def16; end; Lm3: for L1, L2 being non empty RelStr, g being map of L1,L2 holds corestr g is onto proof let L1, L2 be non empty RelStr, g be map of L1,L2; the carrier of Image g = rng g by YELLOW_2:11 .= rng corestr g by Th32; hence thesis by FUNCT_2:def 3; end; definition let L1, L2 be non empty RelStr, g be map of L1,L2; cluster corestr g -> onto; coherence by Lm3; end; theorem Th33: for L1, L2 being non empty RelStr, g being map of L1,L2 st g is monotone holds corestr g is monotone proof let L1, L2 be non empty RelStr, g be map of L1,L2 such that A1: g is monotone; let s1,s2 be Element of L1; reconsider s1' = g.s1, s2' = g.s2 as Element of L2; A2: s1' = (corestr g).s1 & s2' = (corestr g).s2 by Th32; assume s1 <= s2; then g.s1 <= g.s2 by A1,Def2; hence thesis by A2,YELLOW_0:61; end; definition let L1, L2 be non empty RelStr, g be map of L1,L2; func inclusion(g) -> map of Image g,L2 equals :Def17: id Image g; coherence proof A1: dom id Image g = dom id the carrier of Image g by GRCAT_1:def 11 .= the carrier of Image g by RELAT_1:71; rng id Image g = rng id the carrier of Image g by GRCAT_1:def 11 .= the carrier of Image g by RELAT_1:71 .= rng g by YELLOW_2:11; then id Image g is Function of the carrier of Image g, the carrier of L2 by A1,FUNCT_2:def 1,RELSET_1:11; hence thesis; end; end; theorem Th34: for L1, L2 being non empty RelStr, g being map of L1,L2, s being Element of Image g holds (inclusion g).s = s proof let L1, L2 be non empty RelStr, g be map of L1,L2, s be Element of Image g; thus s = (id Image g).s by TMAP_1:91 .= (inclusion g).s by Def17; end; Lm4: for L1, L2 being non empty RelStr,g being map of L1,L2 holds inclusion g is one-to-one proof let L1, L2 be non empty RelStr,g be map of L1,L2; inclusion g = id Image g by Def17 .= id the carrier of Image g by GRCAT_1:def 11; hence thesis; end; Lm5: for L1, L2 being non empty RelStr,g being map of L1,L2 holds inclusion g is monotone proof let L1, L2 be non empty RelStr,g be map of L1,L2; let s1,s2 be Element of Image g; reconsider s1'=(id Image g).s1, s2' = (id Image g).s2 as Element of L2 by YELLOW_0:59; A1: s1' = (inclusion g).s1 & s2' = (inclusion g).s2 by Def17; assume s1 <= s2; then (id Image g).s1 <= s2 by TMAP_1:91; then (id Image g).s1 <= (id Image g).s2 by TMAP_1:91; hence (inclusion g).s1 <= (inclusion g).s2 by A1,YELLOW_0:60; end; definition let L1, L2 be non empty RelStr, g be map of L1,L2; cluster inclusion g -> one-to-one monotone; coherence by Lm4,Lm5; end; theorem Th35: for L being non empty RelStr, f being map of L,L holds (inclusion f)*(corestr f) = f proof let L be non empty RelStr, f be map of L,L; thus (inclusion f)*(corestr f) = (inclusion f)*f by Th32 .= (id Image f)*f by Def17 .= (id the carrier of Image f)*f by GRCAT_1:def 11 .= (id rng f)*f by YELLOW_2:11 .= f by FUNCT_1:42; end; ::Theorem 3.10 (1) implies (2) theorem Th36: for L being non empty Poset, f being map of L,L st f is idempotent holds (corestr f)*(inclusion f) = id(Image f) proof let L be non empty Poset, f be map of L,L; assume A1: f is idempotent; for s being Element of Image f holds ((corestr f)*(inclusion f)).s = s proof let s be Element of Image f; the carrier of Image f = rng corestr f by FUNCT_2:def 3; then consider l being set such that A2: l in the carrier of L and A3: (corestr f).l = s by FUNCT_2:17; reconsider l as Element of L by A2; A4: (corestr f).l = f.l by Th32; thus ((corestr f)*(inclusion f)).s = (corestr f).((inclusion f).s) by FUNCT_2:21 .= (corestr f).s by Th34 .= f.(f.l) by A3,A4,Th32 .= s by A1,A3,A4,YELLOW_2:20; end; hence (corestr f)*(inclusion f) = id(Image f) by Th1; end; ::Theorem 3.10 (1) implies (3) theorem for L being non empty Poset, f being map of L,L st f is_a_projection_operator ex T being non empty Poset, q being map of L,T, i being map of T,L st q is monotone & q is onto & i is monotone & i is one-to-one & f = i*q & id(T) = q*i proof let L be non empty Poset, f be map of L,L; assume f is_a_projection_operator; then A1: f is monotone idempotent by Def13; reconsider T = Image f as non empty Poset; reconsider q = corestr f as map of L,T; reconsider i = inclusion f as map of T,L; take T,q,i; thus q is monotone by A1,Th33; thus q is onto; thus i is monotone one-to-one; thus f = i*q by Th35; thus id(T) = q*i by A1,Th36; end; ::Theorem 3.10 (3) implies (1) theorem for L being non empty Poset, f being map of L,L st (ex T being non empty Poset, q being map of L,T, i being map of T,L st q is monotone & i is monotone & f = i*q & id(T) = q*i) holds f is_a_projection_operator proof let L be non empty Poset, f be map of L,L; given T being non empty Poset, q being map of L,T, i being map of T,L such that A1: q is monotone and A2: i is monotone and A3: f = i*q and A4: id(T) = q*i; A5: i*q*i = i*id(T) by A4,RELAT_1:55 .= i*(id the carrier of T) by GRCAT_1:def 11 .= i by FUNCT_2:23; q*i*q = (id the carrier of T)*q by A4,GRCAT_1:def 11 .= q by FUNCT_2:23; hence f is idempotent by A3,A5,Th22; thus f is monotone by A1,A2,A3,YELLOW_2:14; end; ::Theorem 3.10 (1_1) implies (2_1) theorem Th39: for L being non empty Poset, f being map of L,L st f is_a_closure_operator holds [inclusion f,corestr f] is Galois proof let L be non empty Poset, f be map of L,L; assume that A1: f is idempotent monotone and A2: id L <= f; set g = (corestr f), d = inclusion f; A3: g is monotone by A1,Th33; g*d = id(Image f) by A1,Th36; then A4: g*d <= id(Image f) by Lm1; id L <= d*g by A2,Th35; hence thesis by A3,A4,Th20; end; ::Theorem 3.10 (2_1) implies (3_1) theorem for L being non empty Poset, f being map of L,L st f is_a_closure_operator ex S being non empty Poset, g being map of S,L, d being map of L,S st [g,d] is Galois & f = g*d proof let L be non empty Poset, f be map of L,L; assume A1: f is_a_closure_operator; reconsider S = Image f as non empty Poset; reconsider g = inclusion f as map of S,L; reconsider d = corestr f as map of L,S; take S,g,d; thus [g,d] is Galois by A1,Th39; thus f = g*d by Th35; end; ::Theorem 3.10 (3_1) implies (1_1) theorem Th41: for L being non empty Poset, f being map of L,L st f is monotone & ex S being non empty Poset, g being map of S,L, d being map of L,S st [g,d] is Galois & f = g*d holds f is_a_closure_operator proof let L be non empty Poset, f be map of L,L such that A1: f is monotone; given S being non empty Poset, g being map of S,L, d being map of L,S such that A2: [g,d] is Galois and A3: f = g*d; A4: d*g <= id S & id L <= g*d by A2,Th19; d is monotone & g is monotone by A2,Th9; then d = d*g*d & g = g*d*g by A4,Th21; hence f is idempotent monotone by A1,A3,Th22; thus id(L) <= f by A2,A3,Th19; end; ::Theorem 3.10 (1_2) implies (2_2) theorem Th42: for L being non empty Poset, f being map of L,L st f is_a_kernel_operator holds [corestr f,inclusion f] is Galois proof let L be non empty Poset, f be map of L,L; assume that A1: f is idempotent monotone and A2: f <= id(L); set g = (corestr f), d = inclusion f; A3: g is monotone by A1,Th33; g*d = id(Image f) by A1,Th36; then A4: id(Image f) <= g*d by Lm1; d*g <= id L by A2,Th35; hence thesis by A3,A4,Th20; end; ::Theorem 3.10 (2_2) implies (3_2) theorem for L being non empty Poset, f being map of L,L st f is_a_kernel_operator ex T being non empty Poset, g being map of L,T, d being map of T,L st [g,d] is Galois & f = d*g proof let L be non empty Poset, f be map of L,L; assume A1: f is_a_kernel_operator; reconsider T = Image f as non empty Poset; reconsider g = corestr f as map of L,T; reconsider d = inclusion f as map of T,L; take T,g,d; thus [g,d] is Galois by A1,Th42; thus f = d*g by Th35; end; ::Theorem 3.10 (3_2) implies (1_2) theorem for L being non empty Poset, f being map of L,L st f is monotone & ex T being non empty Poset, g being map of L,T, d being map of T,L st [g,d] is Galois & f = d*g holds f is_a_kernel_operator proof let L be non empty Poset, f be map of L,L; assume A1: f is monotone; given T being non empty Poset, g being map of L,T, d being map of T,L such that A2: [g,d] is Galois and A3: f = d*g; A4: d*g <= id L & id T <= g*d by A2,Th19; d is monotone & g is monotone by A2,Th9; then d = d*g*d & g = g*d*g by A4,Th21; hence f is idempotent monotone by A1,A3,Th22; thus f <= id L by A2,A3,Th19; end; :: Lemma 3.11 (i) (part I) theorem Th45: for L being non empty Poset, p being map of L,L st p is_a_projection_operator holds rng p = {c where c is Element of L: c <= p.c} /\ {k where k is Element of L: p.k <= k} proof let L be non empty Poset, p be map of L,L such that A1: p is idempotent and p is monotone; set Lc = {c where c is Element of L: c <= p.c}; set Lk = {k where k is Element of L: p.k <= k}; A2: dom p = the carrier of L by FUNCT_2:def 1; thus rng p c= Lc /\ Lk proof let x be set; assume A3: x in rng p; then reconsider x'=x as Element of L; consider l being set such that A4: l in dom p and A5: p.l = x by A3,FUNCT_1:def 5; l is Element of L by A2,A4; then x' <= p.x' & p.x' <= x' by A1,A5,YELLOW_2:20; then x in Lc & x in Lk; hence x in Lc /\ Lk by XBOOLE_0:def 3; end; let x be set; assume x in Lc /\ Lk; then A6: x in Lc & x in Lk by XBOOLE_0:def 3; then consider lc being Element of L such that A7: x = lc & lc <= p.lc; consider lk being Element of L such that A8: x = lk & p.lk <= lk by A6; x = p.x by A7,A8,ORDERS_1:25; hence x in rng p by A2,A7,FUNCT_1:def 5; end; theorem Th46: for L being non empty Poset, p being map of L,L st p is_a_projection_operator holds {c where c is Element of L: c <= p.c} is non empty Subset of L & {k where k is Element of L: p.k <= k} is non empty Subset of L proof let L be non empty Poset, p be map of L,L such that A1: p is_a_projection_operator; defpred P[Element of L] means $1 <= p.$1; defpred Q[Element of L] means p.$1 <= $1; set Lc = {c where c is Element of L: P[c]}; set Lk = {k where k is Element of L: Q[k]}; A2: rng p = Lc /\ Lk by A1,Th45; Lc is Subset of L from RelStrSubset; hence Lc is non empty Subset of L by A2; Lk is Subset of L from RelStrSubset; hence Lk is non empty Subset of L by A2; end; :: Lemma 3.11 (i) (part II) theorem Th47: for L being non empty Poset, p being map of L,L st p is_a_projection_operator holds rng(p|{c where c is Element of L: c <= p.c}) = rng p & rng(p|{k where k is Element of L: p.k <= k}) = rng p proof let L be non empty Poset, p be map of L,L such that A1: p is_a_projection_operator; set Lc = {c where c is Element of L: c <= p.c}; set Lk = {k where k is Element of L: p.k <= k}; A2: rng p = Lc /\ Lk by A1,Th45; A3: dom p = the carrier of L by FUNCT_2:def 1; thus rng(p|Lc) = rng p proof thus rng(p|Lc) c= rng p by RELAT_1:99; let y be set; assume y in rng p; then A4: y in Lc & y in Lk by A2,XBOOLE_0:def 3; then consider lc being Element of L such that A5: y = lc & lc <= p.lc; consider lk being Element of L such that A6: y = lk & p.lk <= lk by A4; y = p.y by A5,A6,ORDERS_1:25; hence y in rng(p|Lc) by A3,A4,A5,FUNCT_1:73; end; thus rng(p|Lk) c= rng p by RELAT_1:99; let y be set; assume y in rng p; then A7: y in Lc & y in Lk by A2,XBOOLE_0:def 3; then consider lc being Element of L such that A8: y = lc & lc <= p.lc; consider lk being Element of L such that A9: y = lk & p.lk <= lk by A7; y = p.y by A8,A9,ORDERS_1:25; hence y in rng(p|Lk) by A3,A7,A8,FUNCT_1:73; end; theorem Th48: for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lc being non empty Subset of L, Lk being non empty Subset of L st Lc = {c where c is Element of L: c <= p.c} holds p|Lc is map of subrelstr Lc,subrelstr Lc proof let L be non empty Poset, p be map of L,L such that A1: p is_a_projection_operator; let Lc be non empty Subset of L, Lk be non empty Subset of L such that A2: Lc = {c where c is Element of L: c <= p.c}; set Lk = {k where k is Element of L: p.k <= k}; rng p = Lc /\ Lk by A1,A2,Th45; then rng(p|Lc) = Lc /\ Lk by A1,A2,Th47; then A3: rng(p|Lc) c= Lc by XBOOLE_1:17; A4: Lc = the carrier of subrelstr Lc by YELLOW_0:def 15; p|Lc is Function of Lc,the carrier of L by FUNCT_2:38; then p|Lc is Function of Lc,Lc by A3,FUNCT_2:8; hence p|Lc is map of subrelstr Lc,subrelstr Lc by A4; end; theorem for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lk being non empty Subset of L st Lk = {k where k is Element of L: p.k <= k} holds p|Lk is map of subrelstr Lk,subrelstr Lk proof let L be non empty Poset, p be map of L,L such that A1: p is_a_projection_operator; let Lk be non empty Subset of L such that A2: Lk = {k where k is Element of L: p.k <= k}; set Lc = {c where c is Element of L: c <= p.c}; rng p = Lc /\ Lk by A1,A2,Th45; then rng(p|Lk) = Lc /\ Lk by A1,A2,Th47; then A3: rng(p|Lk) c= Lk by XBOOLE_1:17; A4: Lk = the carrier of subrelstr Lk by YELLOW_0:def 15; p|Lk is Function of Lk,the carrier of L by FUNCT_2:38; then p|Lk is Function of Lk,Lk by A3,FUNCT_2:8; hence p|Lk is map of subrelstr Lk,subrelstr Lk by A4; end; :: Lemma 3.11 (i) (part IIIa) theorem Th50: for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lc being non empty Subset of L st Lc = {c where c is Element of L: c <= p.c} for pc being map of subrelstr Lc,subrelstr Lc st pc = p|Lc holds pc is_a_closure_operator proof let L be non empty Poset, p be map of L,L such that A1: p is idempotent and A2: p is monotone; let Lc be non empty Subset of L such that A3: Lc = {c where c is Element of L: c <= p.c}; let pc be map of subrelstr Lc,subrelstr Lc such that A4: pc = p|Lc; A5: dom pc = the carrier of subrelstr Lc by FUNCT_2:def 1; hereby now let x be Element of subrelstr Lc; A6: pc.x = p.x by A4,A5,FUNCT_1:70; A7: x is Element of L by YELLOW_0:59; p.(p.x) = pc.(pc.x) by A4,A5,A6,FUNCT_1:70 .= (pc*pc).x by A5,FUNCT_1:23; hence (pc*pc).x = pc.x by A1,A6,A7,YELLOW_2:20; end; hence pc*pc = pc by FUNCT_2:113; thus pc is monotone proof let x1,x2 be Element of subrelstr Lc; reconsider x1' = x1, x2' = x2 as Element of L by YELLOW_0:59; A8: pc.x1 = p.x1' & pc.x2 = p.x2' by A4,A5,FUNCT_1:70; assume x1 <= x2; then x1' <= x2' by YELLOW_0:60; then p.x1' <= p.x2' by A2,Def2; hence thesis by A8,YELLOW_0:61; end; end; now let x be Element of subrelstr Lc; reconsider x'=x as Element of L by YELLOW_0:59; A9: pc.x = p.x' by A4,A5,FUNCT_1:70; x in the carrier of subrelstr Lc; then x in Lc by YELLOW_0:def 15; then ex c being Element of L st x = c & c <= p.c by A3; then x <= pc.x by A9,YELLOW_0:61; hence (id subrelstr Lc).x <= pc.x by TMAP_1:91; end; hence id(subrelstr Lc) <= pc by YELLOW_2:10; end; :: Lemma 3.11 (i) (part IIIb) theorem for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lk being non empty Subset of L st Lk = {k where k is Element of L: p.k <= k} for pk being map of subrelstr Lk,subrelstr Lk st pk = p|Lk holds pk is_a_kernel_operator proof let L be non empty Poset, p be map of L,L such that A1: p is idempotent and A2: p is monotone; let Lk be non empty Subset of L such that A3: Lk = {k where k is Element of L: p.k <= k}; let pk be map of subrelstr Lk,subrelstr Lk such that A4: pk = p|Lk; A5: dom pk = the carrier of subrelstr Lk by FUNCT_2:def 1; hereby now let x be Element of subrelstr Lk; A6: pk.x = p.x by A4,A5,FUNCT_1:70; A7: x is Element of L by YELLOW_0:59; p.(p.x) = pk.(pk.x) by A4,A5,A6,FUNCT_1:70 .= (pk*pk).x by A5,FUNCT_1:23; hence (pk*pk).x = pk.x by A1,A6,A7,YELLOW_2:20; end; hence pk*pk = pk by FUNCT_2:113; thus pk is monotone proof let x1,x2 be Element of subrelstr Lk; reconsider x1' = x1, x2' = x2 as Element of L by YELLOW_0:59; A8: pk.x1 = p.x1' & pk.x2 = p.x2' by A4,A5,FUNCT_1:70; assume x1 <= x2; then x1' <= x2' by YELLOW_0:60; then p.x1' <= p.x2' by A2,Def2; hence thesis by A8,YELLOW_0:61; end; end; now let x be Element of subrelstr Lk; reconsider x'=x as Element of L by YELLOW_0:59; A9: pk.x = p.x' by A4,A5,FUNCT_1:70; x in the carrier of subrelstr Lk; then x in Lk by YELLOW_0:def 15; then ex c being Element of L st x = c & p.c <= c by A3; then pk.x <= x by A9,YELLOW_0:61; hence pk.x <= (id subrelstr Lk).x by TMAP_1:91; end; hence pk <= id(subrelstr Lk) by YELLOW_2:10; end; :: Lemma 3.11 (ii) (part I) theorem Th52: for L being non empty Poset, p being map of L,L st p is monotone for Lc being Subset of L st Lc = {c where c is Element of L: c <= p.c} holds subrelstr Lc is sups-inheriting proof let L be non empty Poset, p be map of L,L such that A1: p is monotone; let Lc be Subset of L such that A2: Lc = {c where c is Element of L: c <= p.c}; let X be Subset of subrelstr Lc; assume A3: ex_sup_of X,L; p.("\/"(X,L)) is_>=_than X proof let x be Element of L; assume A4: x in X; then x in the carrier of subrelstr Lc; then x in Lc by YELLOW_0:def 15; then consider l being Element of L such that A5: x = l & l <= p.l by A2; ("\/"(X,L)) is_>=_than X by A3,YELLOW_0:30; then x <= "\/"(X,L) by A4,LATTICE3:def 9; then p.x <= p.("\/"(X,L)) by A1,Def2; hence x <= p.("\/"(X,L)) by A5,ORDERS_1:26; end; then "\/"(X,L) <= p.("\/"(X,L)) by A3,YELLOW_0:30; then "\/"(X,L) in Lc by A2; hence "\/"(X,L) in the carrier of subrelstr Lc by YELLOW_0:def 15; end; :: Lemma 3.11 (ii) (part II) theorem Th53: for L being non empty Poset, p being map of L,L st p is monotone for Lk being Subset of L st Lk = {k where k is Element of L: p.k <= k} holds subrelstr Lk is infs-inheriting proof let L be non empty Poset, p be map of L,L such that A1: p is monotone; let Lk be Subset of L such that A2: Lk = {k where k is Element of L: p.k <= k}; let X be Subset of subrelstr Lk; assume A3: ex_inf_of X,L; p.("/\"(X,L)) is_<=_than X proof let x be Element of L; assume A4: x in X; then x in the carrier of subrelstr Lk; then x in Lk by YELLOW_0:def 15; then consider l being Element of L such that A5: x = l & l >= p.l by A2; ("/\"(X,L)) is_<=_than X by A3,YELLOW_0:31; then x >= "/\"(X,L) by A4,LATTICE3:def 8; then p.x >= p.("/\"(X,L)) by A1,Def2; hence x >= p.("/\"(X,L)) by A5,ORDERS_1:26; end; then "/\"(X,L) >= p.("/\"(X,L)) by A3,YELLOW_0:31; then "/\"(X,L) in Lk by A2; hence "/\"(X,L) in the carrier of subrelstr Lk by YELLOW_0:def 15; end; :: Lemma 3.11 (iii) (part I) theorem for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lc being non empty Subset of L st Lc = {c where c is Element of L: c <= p.c} holds (p is infs-preserving implies subrelstr Lc is infs-inheriting & Image p is infs-inheriting) & (p is filtered-infs-preserving implies subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting) proof let L be non empty Poset, p be map of L,L; assume A1: p is_a_projection_operator; then A2: p is monotone by Def13; let Lc be non empty Subset of L such that A3: Lc = {c where c is Element of L: c <= p.c}; reconsider Lk = {k where k is Element of L: p.k <= k} as non empty Subset of L by A1,Th46; A4: the carrier of Image p = rng p by YELLOW_2:11 .= Lc /\ Lk by A1,A3,Th45; then A5: the carrier of Image p c= Lc & the carrier of Image p c= Lk by XBOOLE_1:17 ; A6: Lc = the carrier of subrelstr Lc & Lk = the carrier of subrelstr Lk by YELLOW_0:def 15; A7: the carrier of Image p c= the carrier of subrelstr Lc by A5,YELLOW_0:def 15; hereby assume A8: p is infs-preserving; thus A9: subrelstr Lc is infs-inheriting proof let X be Subset of subrelstr Lc; the carrier of subrelstr Lc is Subset of L by YELLOW_0:def 15; then X is Subset of L by XBOOLE_1:1; then reconsider X' = X as Subset of L; assume A10: ex_inf_of X,L; p preserves_inf_of X' by A8,WAYBEL_0:def 32; then A11: ex_inf_of p.:X,L & inf (p.:X') = p.(inf X') by A10,WAYBEL_0:def 30 ; inf X' is_<=_than p.:X' proof let y be Element of L; assume y in p.:X'; then consider x being Element of L such that A12: x in X' and A13: y = p.x by FUNCT_2:116; reconsider x as Element of L; x in Lc by A6,A12; then A14: ex x' being Element of L st x' = x & x' <= p.x' by A3; inf X' is_<=_than X' by A10,YELLOW_0:31; then inf X' <= x by A12,LATTICE3:def 8; hence inf X' <= y by A13,A14,ORDERS_1:26; end; then inf X' <= p.(inf X') by A11,YELLOW_0:31; hence "/\"(X,L) in the carrier of subrelstr Lc by A3,A6; end; thus Image p is infs-inheriting proof let X be Subset of Image p such that A15: ex_inf_of X,L; X c= Lc by A5,XBOOLE_1:1; then X is Subset of subrelstr Lc by A6; then A16: "/\"(X,L) in the carrier of subrelstr Lc by A9,A15,YELLOW_0:def 18; A17: subrelstr Lk is infs-inheriting by A2,Th53; X c= the carrier of subrelstr Lk by A5,A6,XBOOLE_1:1; then X is Subset of subrelstr Lk; then "/\"(X,L) in the carrier of subrelstr Lk by A15,A17,YELLOW_0:def 18; hence "/\"(X,L) in the carrier of Image p by A4,A6,A16,XBOOLE_0:def 3; end; end; assume A18: p is filtered-infs-preserving; thus A19: subrelstr Lc is filtered-infs-inheriting proof let X be filtered Subset of subrelstr Lc; assume X <> {}; then reconsider X' = X as non empty filtered Subset of L by YELLOW_2:7; assume A20: ex_inf_of X,L; p preserves_inf_of X' by A18,WAYBEL_0:def 36; then A21: ex_inf_of p.:X,L & inf (p.:X') = p.(inf X') by A20,WAYBEL_0:def 30 ; inf X' is_<=_than p.:X' proof let y be Element of L; assume y in p.:X'; then consider x being Element of L such that A22: x in X' and A23: y = p.x by FUNCT_2:116; reconsider x as Element of L; x in Lc by A6,A22; then A24: ex x' being Element of L st x' = x & x' <= p.x' by A3; inf X' is_<=_than X' by A20,YELLOW_0:31; then inf X' <= x by A22,LATTICE3:def 8; hence inf X' <= y by A23,A24,ORDERS_1:26; end; then inf X' <= p.(inf X') by A21,YELLOW_0:31; hence "/\"(X,L) in the carrier of subrelstr Lc by A3,A6; end; let X be filtered Subset of Image p such that A25: X <> {} and A26: ex_inf_of X,L; X is filtered Subset of subrelstr Lc by A7,YELLOW_2:8; then A27: "/\"(X,L) in the carrier of subrelstr Lc by A19,A25,A26,WAYBEL_0 :def 3; A28: subrelstr Lk is infs-inheriting by A2,Th53; X c= the carrier of subrelstr Lk by A5,A6,XBOOLE_1:1; then X is Subset of subrelstr Lk; then "/\"(X,L) in the carrier of subrelstr Lk by A26,A28,YELLOW_0:def 18; hence "/\"(X,L) in the carrier of Image p by A4,A6,A27,XBOOLE_0:def 3; end; :: Lemma 3.11 (iii) (part II) theorem for L being non empty Poset, p being map of L,L st p is_a_projection_operator for Lk being non empty Subset of L st Lk = {k where k is Element of L: p.k <= k} holds (p is sups-preserving implies subrelstr Lk is sups-inheriting & Image p is sups-inheriting) & (p is directed-sups-preserving implies subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting) proof let L be non empty Poset, p be map of L,L; assume A1: p is_a_projection_operator; then A2: p is monotone by Def13; let Lk be non empty Subset of L such that A3: Lk = {k where k is Element of L: p.k <= k}; reconsider Lc = {c where c is Element of L: c <= p.c} as non empty Subset of L by A1,Th46; A4: the carrier of Image p = rng p by YELLOW_2:11 .= Lc /\ Lk by A1,A3,Th45; then A5: the carrier of Image p c= Lc & the carrier of Image p c= Lk by XBOOLE_1:17 ; A6: Lc = the carrier of subrelstr Lc & Lk = the carrier of subrelstr Lk by YELLOW_0:def 15; A7: the carrier of Image p c= the carrier of subrelstr Lk by A5,YELLOW_0:def 15; hereby assume A8: p is sups-preserving; thus A9: subrelstr Lk is sups-inheriting proof let X be Subset of subrelstr Lk; the carrier of subrelstr Lk is Subset of L by YELLOW_0:def 15; then X is Subset of L by XBOOLE_1:1; then reconsider X' = X as Subset of L; assume A10: ex_sup_of X,L; p preserves_sup_of X' by A8,WAYBEL_0:def 33; then A11: ex_sup_of p.:X,L & sup (p.:X') = p.(sup X') by A10,WAYBEL_0:def 31 ; sup X' is_>=_than p.:X' proof let y be Element of L; assume y in p.:X'; then consider x being Element of L such that A12: x in X' and A13: y = p.x by FUNCT_2:116; reconsider x as Element of L; x in Lk by A6,A12; then A14: ex x' being Element of L st x' = x & x' >= p.x' by A3; sup X' is_>=_than X' by A10,YELLOW_0:30; then sup X' >= x by A12,LATTICE3:def 9; hence sup X' >= y by A13,A14,ORDERS_1:26; end; then sup X' >= p.(sup X') by A11,YELLOW_0:30; hence "\/"(X,L) in the carrier of subrelstr Lk by A3,A6; end; thus Image p is sups-inheriting proof let X be Subset of Image p such that A15: ex_sup_of X,L; X c= Lk by A5,XBOOLE_1:1; then X is Subset of subrelstr Lk by A6; then A16: "\/"(X,L) in the carrier of subrelstr Lk by A9,A15,YELLOW_0:def 19; A17: subrelstr Lc is sups-inheriting by A2,Th52; X c= the carrier of subrelstr Lc by A5,A6,XBOOLE_1:1; then X is Subset of subrelstr Lc; then "\/"(X,L) in the carrier of subrelstr Lc by A15,A17,YELLOW_0:def 19; hence "\/"(X,L) in the carrier of Image p by A4,A6,A16,XBOOLE_0:def 3; end; end; assume A18: p is directed-sups-preserving; thus A19: subrelstr Lk is directed-sups-inheriting proof let X be directed Subset of subrelstr Lk; assume X <> {}; then reconsider X' = X as non empty directed Subset of L by YELLOW_2:7; assume A20: ex_sup_of X,L; p preserves_sup_of X' by A18,WAYBEL_0:def 37; then A21: ex_sup_of p.:X,L & sup (p.:X') = p.(sup X') by A20,WAYBEL_0:def 31 ; sup X' is_>=_than p.:X' proof let y be Element of L; assume y in p.:X'; then consider x being Element of L such that A22: x in X' and A23: y = p.x by FUNCT_2:116; reconsider x as Element of L; x in Lk by A6,A22; then A24: ex x' being Element of L st x' = x & x' >= p.x' by A3; sup X' is_>=_than X' by A20,YELLOW_0:30; then sup X' >= x by A22,LATTICE3:def 9; hence sup X' >= y by A23,A24,ORDERS_1:26; end; then sup X' >= p.(sup X') by A21,YELLOW_0:30; hence "\/"(X,L) in the carrier of subrelstr Lk by A3,A6; end; let X be directed Subset of Image p such that A25: X <> {} and A26: ex_sup_of X,L; X is directed Subset of subrelstr Lk by A7,YELLOW_2:8; then A27: "\/"(X,L) in the carrier of subrelstr Lk by A19,A25,A26,WAYBEL_0: def 4; A28: subrelstr Lc is sups-inheriting by A2,Th52; X c= the carrier of subrelstr Lc by A5,A6,XBOOLE_1:1; then X is Subset of subrelstr Lc; then "\/"(X,L) in the carrier of subrelstr Lc by A26,A28,YELLOW_0:def 19; hence "\/"(X,L) in the carrier of Image p by A4,A6,A27,XBOOLE_0:def 3; end; :: Proposition 3.12 (i) theorem Th56: for L being non empty Poset, p being map of L,L holds (p is_a_closure_operator implies Image p is infs-inheriting) & (p is_a_kernel_operator implies Image p is sups-inheriting) proof let L be non empty Poset, p be map of L,L; hereby assume A1: p is_a_closure_operator; thus Image p is infs-inheriting proof let X be Subset of Image p; assume A2: ex_inf_of X,L; A3: the carrier of Image p = rng p by YELLOW_2:11; then X c= the carrier of L by XBOOLE_1:1; then reconsider X'=X as Subset of L; p.("/\"(X',L)) = "/\"(X',L) by A1,A2,A3,Th30; hence "/\"(X,L) in the carrier of Image p by A3,FUNCT_2:6; end; end; assume A4: p is_a_kernel_operator; let X be Subset of Image p; assume A5: ex_sup_of X,L; A6: the carrier of Image p = rng p by YELLOW_2:11; then X c= the carrier of L by XBOOLE_1:1; then reconsider X'=X as Subset of L; p.("\/"(X',L)) = "\/"(X',L) by A4,A5,A6,Th31; hence "\/"(X,L) in the carrier of Image p by A6,FUNCT_2:6; end; :: Proposition 3.12 (ii) theorem for L being complete (non empty Poset), p being map of L,L st p is_a_projection_operator holds Image p is complete proof let L be complete (non empty Poset), p be map of L,L; assume A1: p is_a_projection_operator; then reconsider Lc = {c where c is Element of L: c <= p.c}, Lk = {k where k is Element of L: p.k <= k} as non empty Subset of L by Th46; A2: p is monotone by A1,Def13; reconsider pc = p|Lc as map of subrelstr Lc,subrelstr Lc by A1,Th48; subrelstr Lc is sups-inheriting by A2,Th52; then A3: subrelstr Lc is complete LATTICE by YELLOW_2:33; pc is_a_closure_operator by A1,Th50; then Image pc is infs-inheriting by Th56; then subrelstr(rng pc)is infs-inheriting by YELLOW_2:def 2; then A4: subrelstr(rng pc) is complete by A3,YELLOW_2:32; A5: the carrier of Image p = the carrier of subrelstr(rng p) by YELLOW_2:def 2 .= rng p by YELLOW_0:def 15; A6: the carrier of subrelstr Lc = Lc by YELLOW_0:def 15; rng p = Lc /\ Lk by A1,Th45; then A7: the carrier of Image p c= the carrier of subrelstr Lc by A5,A6, XBOOLE_1:17 ; A8: the carrier of Image pc = the carrier of subrelstr(rng pc) by YELLOW_2:def 2 .= rng(pc) by YELLOW_0:def 15 .= the carrier of Image p by A1,A5,Th47; then the InternalRel of Image pc = (the InternalRel of subrelstr Lc)|_2 the carrier of Image p by YELLOW_0:def 14 .= ((the InternalRel of L)|_2 the carrier of subrelstr Lc) |_2 the carrier of Image p by YELLOW_0:def 14 .= (the InternalRel of L)|_2 the carrier of Image p by A7,WELLORD1:29 .= the InternalRel of Image p by YELLOW_0:def 14; hence Image p is complete by A4,A8,YELLOW_2:def 2; end; :: Proposition 3.12 (iii) theorem for L being non empty Poset, c being map of L,L st c is_a_closure_operator holds corestr c is sups-preserving & for X being Subset of L st X c= the carrier of Image c & ex_sup_of X,L holds ex_sup_of X,Image c & "\/"(X,Image c) = c.("\/"(X,L)) proof let L be non empty Poset, c be map of L,L; assume A1: c is_a_closure_operator; then [inclusion c,corestr c] is Galois by Th39; then corestr c is lower_adjoint by Def12; hence A2: corestr c is sups-preserving by Th14; let X be Subset of L such that A3: X c= the carrier of Image c and A4: ex_sup_of X,L; A5: corestr c preserves_sup_of X by A2,WAYBEL_0:def 33; A6: (corestr c) = c by Th32; A7: X c= rng c by A3,YELLOW_2:11; c is projection by A1,Def14; then c is idempotent by Def13; then c.:X = X by A7,YELLOW_2:22; hence thesis by A4,A5,A6,WAYBEL_0:def 31; end; :: Proposition 3.12 (iv) theorem for L being non empty Poset, k being map of L,L st k is_a_kernel_operator holds (corestr k) is infs-preserving & for X being Subset of L st X c= the carrier of Image k & ex_inf_of X,L holds ex_inf_of X,Image k & "/\"(X,Image k) = k.("/\"(X,L)) proof let L be non empty Poset, k be map of L,L; assume A1: k is_a_kernel_operator; then [corestr k,inclusion k] is Galois by Th42; then corestr k is upper_adjoint by Def11; hence A2: (corestr k) is infs-preserving by Th13; let X be Subset of L such that A3: X c= the carrier of Image k and A4: ex_inf_of X,L; A5: corestr k preserves_inf_of X by A2,WAYBEL_0:def 32; A6: (corestr k) = k by Th32; A7: X c= rng k by A3,YELLOW_2:11; k is projection by A1,Def15; then k is idempotent by Def13; then k.:X = X by A7,YELLOW_2:22; hence thesis by A4,A5,A6,WAYBEL_0:def 30; end; begin :: Heyting algebras :: Proposition 3.15 (i) theorem Th60: for L being complete (non empty Poset) holds [IdsMap L,SupMap L] is Galois & SupMap L is sups-preserving proof let L be complete (non empty Poset); set g = IdsMap L, d = SupMap L; now let I be Element of InclPoset(Ids L), x be Element of L; reconsider I' = I as Ideal of L by YELLOW_2:43; hereby assume I <= g.x; then I c= g.x by YELLOW_1:3; then I' c= downarrow x by YELLOW_2:def 4; then x is_>=_than I' by YELLOW_2:1; then sup I' <= x by YELLOW_0:32; hence d.I <= x by YELLOW_2:def 3; end; assume d.I <= x; then A1: sup I' <= x by YELLOW_2:def 3; sup I' is_>=_than I' by YELLOW_0:32; then x is_>=_than I' by A1,YELLOW_0:4; then I' c= downarrow x by YELLOW_2:1; then I c= g.x by YELLOW_2:def 4; hence I <= g.x by YELLOW_1:3; end; hence [IdsMap L,SupMap L] is Galois by Th9; then SupMap L is lower_adjoint by Th10; hence SupMap L is sups-preserving by Th14; end; :: Proposition 3.15 (ii) theorem for L being complete (non empty Poset) holds (IdsMap L)*(SupMap L) is_a_closure_operator & Image ((IdsMap L)*(SupMap L)),L are_isomorphic proof let L be complete (non empty Poset); set i = (IdsMap L)*(SupMap L); A1: i is monotone by YELLOW_2:14; [IdsMap L,SupMap L] is Galois by Th60; hence i is_a_closure_operator by A1,Th41; take f = (SupMap L)*(inclusion i); A2: now let I be Ideal of L; I is Element of InclPoset(Ids L) by YELLOW_2:43; hence i.I = (IdsMap L).((SupMap L).I) by FUNCT_2:21 .= (IdsMap L).(sup I) by YELLOW_2:def 3 .= downarrow (sup I) by YELLOW_2:def 4; end; A3: now let x be Element of Image i; let I be Ideal of L; assume A4: x = I; hence f.I = (SupMap L).((inclusion i).I) by FUNCT_2:21 .= (SupMap L).I by A4,Th34 .= sup I by YELLOW_2:def 3; end; A5: f is one-to-one proof let x,y be Element of Image i; assume A6: f.x = f.y; consider Ix being Element of InclPoset(Ids L) such that A7: i.Ix = x by YELLOW_2:12; consider Iy being Element of InclPoset(Ids L) such that A8: i.Iy = y by YELLOW_2:12; reconsider Ix,Iy as Ideal of L by YELLOW_2:43; A9: i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A2; x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L) by YELLOW_0:59; then reconsider x,y as Ideal of L by YELLOW_2:43; A10: f.x = sup x & f.y = sup y by A3; sup downarrow (sup Ix) = sup Ix & sup downarrow (sup Iy) = sup Iy by WAYBEL_0:34; hence thesis by A6,A7,A8,A9,A10; end; A11: f is monotone by YELLOW_2:14; A12: rng f = the carrier of L proof thus rng f c= the carrier of L; let x be set; assume x in the carrier of L; then reconsider x as Element of L; A13: (SupMap L).(downarrow x) = sup downarrow x by YELLOW_2:def 3 .= x by WAYBEL_0:34; A14: downarrow x is Element of InclPoset(Ids L) by YELLOW_2:43; then i.(downarrow x) = (IdsMap L).((SupMap L).(downarrow x)) by FUNCT_2:21 .= downarrow x by A13,YELLOW_2:def 4; then downarrow x in rng i by A14,FUNCT_2:6; then A15: downarrow x in the carrier of Image i by YELLOW_2:11; then A16: downarrow x is Element of Image i; f.(downarrow x) = (SupMap L).((inclusion i).(downarrow x)) by A15,FUNCT_2: 21 .= (SupMap L).(downarrow x) by A16,Th34; hence thesis by A13,A15,FUNCT_2:6; end; now let x,y be Element of Image i; thus x <= y implies f.x <= f.y by A11,Def2; assume A17: f.x <= f.y; consider Ix being Element of InclPoset(Ids L) such that A18: i.Ix = x by YELLOW_2:12; consider Iy being Element of InclPoset(Ids L) such that A19: i.Iy = y by YELLOW_2:12; reconsider Ix,Iy as Ideal of L by YELLOW_2:43; A20: i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A2; x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L) by YELLOW_0:59; then reconsider x'=x, y'=y as Ideal of L by YELLOW_2:43; reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy) as Element of InclPoset(Ids L) by YELLOW_2:43; A21: f.x' = sup x' & f.y' = sup y' by A3; sup downarrow (sup Ix) = sup Ix & sup downarrow (sup Iy) = sup Iy by WAYBEL_0:34; then downarrow (sup Ix) c= downarrow (sup Iy) by A17,A18,A19,A20,A21, WAYBEL_0:21; then i1 <= i2 by YELLOW_1:3; hence x <= y by A18,A19,A20,YELLOW_0:61; end; hence f is isomorphic by A5,A12,WAYBEL_0:66; end; definition let S be non empty RelStr; let x be Element of S; func x "/\" -> map of S,S means :Def18: for s being Element of S holds it.s = x"/\"s; existence proof deffunc F(Element of S) = x"/\"$1; thus ex f being map of S,S st for x being Element of S holds f.x = F(x) from LambdaMD; end; uniqueness proof let f1,f2 be map of S,S such that A1: for s being Element of S holds f1.s = x"/\"s and A2: for s being Element of S holds f2.s = x"/\"s; now let s be Element of S; thus f1.s = x"/\"s by A1 .= f2.s by A2; end; hence thesis by YELLOW_2:9; end; end; theorem Th62: for S being non empty RelStr, x,t being Element of S holds {s where s is Element of S: x"/\"s <= t} = (x "/\")"(downarrow t) proof let S be non empty RelStr, x,t be Element of S; hereby let a be set; assume a in {s where s is Element of S: x"/\"s <= t}; then consider s being Element of S such that A1: a = s and A2: x"/\"s <= t; (x "/\").s <= t by A2,Def18; then (x"/\").s in downarrow t by WAYBEL_0:17; hence a in (x "/\")"(downarrow t) by A1,FUNCT_2:46; end; let s be set; assume A3: s in (x "/\")"(downarrow t); then reconsider s as Element of S; (x "/\").s in downarrow t by A3,FUNCT_2:46; then x"/\"s in downarrow t by Def18; then x"/\"s <= t by WAYBEL_0:17; hence thesis; end; theorem Th63: for S being Semilattice, x be Element of S holds x "/\" is monotone proof let S be Semilattice, x be Element of S; let s1,s2 be Element of S; assume A1: s1 <= s2; A2: ex_inf_of {x,s2},S by YELLOW_0:21; A3: ex_inf_of {x,s1},S by YELLOW_0:21; then x"/\"s1 <= s1 by YELLOW_0:19; then x"/\"s1 <= s2 & x"/\"s1 <= x by A1,A3,ORDERS_1:26,YELLOW_0:19; then x"/\"s1 <= x"/\"s2 by A2,YELLOW_0:19; then (x "/\").s1 <= x"/\"s2 by Def18; hence (x "/\").s1 <= (x "/\").s2 by Def18; end; definition let S be Semilattice, x be Element of S; cluster x "/\" -> monotone; coherence by Th63; end; theorem Th64: for S being non empty RelStr, x being Element of S, X being Subset of S holds (x "/\").:X = {x"/\"y where y is Element of S: y in X} proof let S be non empty RelStr, x be Element of S, X be Subset of S; set Y = {x"/\"y where y is Element of S: y in X}; hereby let y be set; assume y in (x "/\").:X; then consider z being set such that A1: z in the carrier of S and A2: z in X and A3: y = (x "/\").z by FUNCT_2:115; reconsider z as Element of S by A1; y = x "/\" z by A3,Def18; hence y in Y by A2; end; let y be set; assume y in Y; then consider z being Element of S such that A4: y = x "/\" z and A5: z in X; y = (x "/\").z by A4,Def18; hence y in (x "/\").:X by A5,FUNCT_2:43; end; :: Lemma 3.16 (1) iff (2) theorem Th65: for S being Semilattice holds (for x being Element of S holds x "/\" has_an_upper_adjoint) iff (for x,t being Element of S holds ex_max_of {s where s is Element of S: x"/\"s <= t},S) proof let S be Semilattice; hereby assume A1: for x being Element of S holds x "/\" has_an_upper_adjoint; let x,t be Element of S; set X = {s where s is Element of S: x"/\"s <= t}; (x "/\") has_an_upper_adjoint by A1; then consider g being map of S,S such that A2: [g, x "/\"] is Galois by Def12; A3: X = (x "/\")"(downarrow t) by Th62; g.t is_maximum_of (x "/\")"(downarrow t) by A2,Th12; then ex_sup_of X,S & "\/"(X,S)in X by A3,Def7; hence ex_max_of X,S by Def5; end; assume A4: for x,t being Element of S holds ex_max_of {s where s is Element of S: x"/\"s <= t},S; let x be Element of S; deffunc F(Element of S) = "\/"((x "/\")"(downarrow $1),S); consider g being map of S,S such that A5: for s being Element of S holds g.s = F(s) from LambdaMD; now let t be Element of S; set X = {s where s is Element of S: x"/\"s <= t}; ex_max_of X,S by A4; then A6: ex_sup_of X,S & "\/"(X,S) in X by Def5; A7: X = (x "/\")"(downarrow t) by Th62; g.t = "\/"((x "/\")"(downarrow t),S) by A5; hence g.t is_maximum_of (x "/\")"(downarrow t) by A6,A7,Def7; end; then [g, x "/\"] is Galois by Th12; hence x "/\" has_an_upper_adjoint by Def12; end; :: Lemma 3.16 (1) implies (3) theorem Th66: for S being Semilattice st for x being Element of S holds x "/\" has_an_upper_adjoint for X being Subset of S st ex_sup_of X,S for x being Element of S holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S) proof let S be Semilattice such that A1: for x being Element of S holds x "/\" has_an_upper_adjoint; let X be Subset of S such that A2: ex_sup_of X,S; let x be Element of S; x "/\" has_an_upper_adjoint by A1; then x "/\" is sups-preserving by Th14; then x "/\" preserves_sup_of X by WAYBEL_0:def 33; then ex_sup_of (x "/\").:X,S & sup ((x "/\").:X) = (x "/\").(sup X) by A2,WAYBEL_0:def 31; hence x "/\" "\/"(X,S) = sup ((x "/\").:X) by Def18 .= "\/"({x"/\" y where y is Element of S: y in X},S) by Th64; end; :: Lemma 3.16 (1) iff (3) theorem for S being complete (non empty Poset) holds (for x being Element of S holds x "/\" has_an_upper_adjoint) iff for X being Subset of S, x being Element of S holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S) proof let S be complete (non empty Poset); hereby assume A1: for x being Element of S holds x "/\" has_an_upper_adjoint; let X be Subset of S, x be Element of S; ex_sup_of X,S by YELLOW_0:17; hence x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S) by A1,Th66; end; assume A2: for X being Subset of S, x being Element of S holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S); let x be Element of S; x "/\" is sups-preserving proof let X be Subset of S; assume ex_sup_of X,S; thus ex_sup_of (x "/\").:X,S by YELLOW_0:17; thus (x "/\").(sup X) = x "/\" "\/"(X,S) by Def18 .= "\/"({x"/\" y where y is Element of S: y in X},S) by A2 .= sup ((x "/\").:X) by Th64; end; hence x "/\" has_an_upper_adjoint by Th18; end; :: Lemma 3.16 (3) implies (D) theorem Th68: for S being LATTICE st for X being Subset of S st ex_sup_of X,S for x being Element of S holds x"/\"("\/"(X,S)) = "\/"({x"/\" y where y is Element of S: y in X},S) holds S is distributive proof let S be LATTICE such that A1: for X being Subset of S st ex_sup_of X,S for x being Element of S holds x"/\"("\/"(X,S)) = "\/"({x"/\"y where y is Element of S: y in X},S); let x,y,z be Element of S; set Y = {x"/\"s where s is Element of S: s in {y,z}}; now let t be set; hereby assume t in Y; then consider s being Element of S such that A2: t = x"/\"s and A3: s in {y,z}; thus t = x"/\"y or t = x"/\"z by A2,A3,TARSKI:def 2; end; assume A4: t = x"/\"y or t = x"/\"z; per cases by A4; suppose A5: t = x"/\"y; y in {y,z} by TARSKI:def 2; hence t in Y by A5; suppose A6: t = x"/\"z; z in {y,z} by TARSKI:def 2; hence t in Y by A6; end; then A7: Y = {x"/\"y,x"/\"z} by TARSKI:def 2; A8: ex_sup_of {y,z},S by YELLOW_0:20; thus x "/\" (y "\/" z) = x "/\" (sup {y,z}) by YELLOW_0:41 .= "\/"({x"/\"y,x"/\"z},S) by A1,A7,A8 .= (x "/\" y) "\/" (x "/\" z) by YELLOW_0:41; end; definition let H be non empty RelStr; attr H is Heyting means :Def19: H is LATTICE & for x being Element of H holds x "/\" has_an_upper_adjoint; synonym H is_a_Heyting_algebra; end; definition cluster Heyting -> with_infima with_suprema reflexive transitive antisymmetric (non empty RelStr); coherence by Def19; end; definition let H be non empty RelStr, a be Element of H; assume A1: H is Heyting; func a => -> map of H,H means :Def20: [it,a "/\"] is Galois; existence proof a "/\" has_an_upper_adjoint by A1,Def19; hence ex g being map of H,H st [g, a "/\"] is Galois by Def12; end; uniqueness proof let g1,g2 be map of H,H such that A2: [g1,a "/\"] is Galois and A3: [g2,a "/\"] is Galois; now let x be Element of H; H is LATTICE by A1,Def19; then g1.x is_maximum_of (a "/\")"(downarrow x) & g2.x is_maximum_of (a "/\")"(downarrow x) by A2,A3,Th12; then g1.x = "\/"((a "/\")"(downarrow x),H) & g2.x = "\/"((a "/\" )"(downarrow x),H) by Def7; hence g1.x = g2.x; end; hence g1 = g2 by YELLOW_2:9; end; end; theorem Th69: for H being non empty RelStr st H is_a_Heyting_algebra holds H is distributive proof let H be non empty RelStr; assume A1: H is LATTICE & for x being Element of H holds x "/\" has_an_upper_adjoint; then for X being Subset of H st ex_sup_of X,H for x being Element of H holds x "/\" "\/"(X,H) = "\/"({x"/\"y where y is Element of H: y in X},H) by Th66; hence H is distributive by A1,Th68; end; definition cluster Heyting -> distributive (non empty RelStr); coherence by Th69; end; definition let H be non empty RelStr, a,y be Element of H; func a => y -> Element of H equals :Def21: (a=>).y; correctness; end; theorem Th70: for H being non empty RelStr st H is_a_Heyting_algebra for x,a,y being Element of H holds x >= a "/\" y iff a => x >= y proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let x,a,y be Element of H; [a =>, a "/\"] is Galois by A1,Def20; then x >= (a "/\").y iff (a =>).x >= y by A2,Th9; hence thesis by Def18,Def21; end; theorem Th71: for H being non empty RelStr st H is_a_Heyting_algebra holds H is upper-bounded proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; consider a being Element of H; take x = a => a; let y be Element of H; assume y in the carrier of H; a >= a "/\" y by A2,YELLOW_0:23; hence x >= y by A1,Th70; end; definition cluster Heyting -> upper-bounded (non empty RelStr); coherence by Th71; end; theorem Th72: for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H holds Top H = a => b iff a <= b proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; A3: H is upper-bounded by A1,Th71; let a,b be Element of H; A4: a "/\" Top H = Top H "/\" a by A2,LATTICE3:15 .= a by A2,A3,Th5; hereby assume Top H = a => b; then a => b >= Top H by A2,ORDERS_1:24; hence a <= b by A1,A4,Th70; end; assume a <= b; then A5: a => b >= Top H by A1,A4,Th70; a => b <= Top H by A2,A3,YELLOW_0:45; hence Top H = a => b by A2,A5,ORDERS_1:25; end; theorem for H being non empty RelStr st H is_a_Heyting_algebra for a being Element of H holds Top H = a => a proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a be Element of H; a >= a "/\" Top H by A2,YELLOW_0:23; then A3: Top H <= a => a by A1,Th70; H is upper-bounded by A1,Th71; then Top H >= a => a by A2,YELLOW_0:45; hence Top H = a => a by A2,A3,ORDERS_1:25; end; theorem for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H st Top H = a => b & Top H = b => a holds a = b proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a,b be Element of H; assume Top H = a => b; then A3: a <= b by A1,Th72; assume Top H = b => a; then b <= a by A1,Th72; hence thesis by A2,A3,ORDERS_1:25; end; theorem Th75: for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H holds b <= (a => b) proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a,b be Element of H; a"/\"b <= b by A2,YELLOW_0:23; hence b <= (a => b) by A1,Th70; end; theorem for H being non empty RelStr st H is_a_Heyting_algebra for a being Element of H holds Top H = a => Top H proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a be Element of H; H is upper-bounded by A1,Th71; then a <= Top H by A2,YELLOW_0:45; hence thesis by A1,Th72; end; theorem for H being non empty RelStr st H is_a_Heyting_algebra for b being Element of H holds b = (Top H) => b proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; A3: H is upper-bounded by A1,Th71; let b be Element of H; (Top H) => b <= (Top H) => b by A2,ORDERS_1:24; then Top H "/\" ((Top H) => b) <= b by A1,Th70; then A4: (Top H) => b <= b by A2,A3,Th5; (Top H) => b >= b by A1,Th75; hence thesis by A2,A4,ORDERS_1:25; end; Lm6: for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H holds a"/\"(a => b) <= b proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a,b be Element of H; (a => b) <= (a => b) by A2,ORDERS_1:24; hence a"/\"(a => b) <= b by A1,Th70; end; theorem Th78: for H being non empty RelStr st H is_a_Heyting_algebra for a,b,c being Element of H st a <= b holds (b => c) <= (a => c) proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a,b,c be Element of H; assume a <= b; then A3: a"/\"(b => c) <= b"/\"(b => c) by A2,Th2; b"/\"(b => c) <= c by A1,Lm6; then a"/\"(b => c) <= c by A2,A3,ORDERS_1:26; hence (b => c) <= (a => c) by A1,Th70; end; theorem for H being non empty RelStr st H is_a_Heyting_algebra for a,b,c being Element of H st b <= c holds (a => b) <= (a => c) proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a,b,c be Element of H; assume A3: b <= c; a"/\"(a => b) <= b by A1,Lm6; then a"/\"(a => b) <= c by A2,A3,ORDERS_1:26; hence thesis by A1,Th70; end; theorem Th80: for H being non empty RelStr st H is_a_Heyting_algebra for a,b being Element of H holds a"/\"(a => b) = a"/\"b proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a,b be Element of H; a"/\"(a => b) <= b by A1,Lm6; then (a"/\"(a => b))"/\"a <= b"/\"a by A2,Th2; then a"/\"(a"/\"(a => b)) <= b"/\"a by A2,LATTICE3:15; then a"/\"(a"/\"(a => b)) <= a"/\"b by A2,LATTICE3:15; then (a"/\"a)"/\"(a => b) <= a"/\"b by A2,LATTICE3:16; then A3: a"/\"(a => b) <= a"/\"b by A2,YELLOW_0:25; b <= (a => b) by A1,Th75; then b"/\"a <= (a => b)"/\"a by A2,Th2; then a"/\"b <= (a => b)"/\"a by A2,LATTICE3:15; then a"/\"b <= a"/\"(a => b) by A2,LATTICE3:15; hence thesis by A2,A3,ORDERS_1:25; end; theorem Th81: for H being non empty RelStr st H is_a_Heyting_algebra for a,b,c being Element of H holds (a"\/"b)=> c = (a => c) "/\" (b => c) proof let H be non empty RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; A3: H is distributive by A1,Th69; let a,b,c be Element of H; a <= a"\/"b & b <= a"\/"b by A2,YELLOW_0:22; then (a"\/"b)=> c <= (a => c) & (a"\/"b)=> c <= (b => c) by A1,Th78; then A4: (a"\/"b)=> c <= (a => c) "/\" (b => c) by A2,YELLOW_0:23; set d = (a => c) "/\" (b => c); A5: (a"\/"b)"/\"d = d"/\"(a"\/"b) by A2,LATTICE3:15 .= (d"/\"a)"\/"(d"/\"b) by A3,Def3 .= (a"/\"d)"\/"(d"/\"b) by A2,LATTICE3:15 .= (a"/\"d)"\/"(b"/\"d) by A2,LATTICE3:15 .= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"d) by A2,LATTICE3:16 .= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"((b=>c)"/\"(a=>c))) by A2,LATTICE3:15 .= ((a"/\"(a=>c))"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A2,LATTICE3:16 .= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A1,Th80 .= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"c)"/\"(a=>c)) by A1,Th80; ((a"/\"c)"/\"(b=>c)) <= a"/\"c & a"/\"c <= c by A2,YELLOW_0:23; then A6: ((a"/\"c)"/\"(b=>c)) <= c by A2,ORDERS_1:26; ((b"/\"c)"/\"(a=>c)) <= b"/\"c & b"/\"c <= c by A2,YELLOW_0:23; then ((b"/\"c)"/\"(a=>c)) <= c by A2,ORDERS_1:26; then (a"\/"b)"/\"d <= c by A2,A5,A6,YELLOW_0:22; then (a"\/"b)=> c >= d by A1,Th70; hence (a"\/"b)=> c = d by A2,A4,ORDERS_1:25; end; definition let H be non empty RelStr, a be Element of H; func 'not' a -> Element of H equals :Def22: a => Bottom H; correctness; end; theorem for H being non empty RelStr st H is_a_Heyting_algebra & H is lower-bounded for a being Element of H holds 'not' a is_maximum_of {x where x is Element of H: a"/\"x = Bottom H} proof let H be non empty RelStr such that A1: H is_a_Heyting_algebra and A2: H is lower-bounded; let a be Element of H; A3: H is LATTICE by A1,Def19; set X = {x where x is Element of H: a"/\"x = Bottom H}, Y = {x where x is Element of H: a"/\"x <= Bottom H}; A4: X = Y proof hereby let y be set; assume y in X; then consider x being Element of H such that A5: y = x and A6: a"/\"x = Bottom H; a"/\"x <= Bottom H by A3,A6,ORDERS_1:24; hence y in Y by A5; end; let y be set; assume y in Y; then consider x being Element of H such that A7: y = x and A8: a"/\"x <= Bottom H; Bottom H <= a"/\"x by A2,A3,YELLOW_0:44; then Bottom H = a"/\"x by A3,A8,ORDERS_1:25; hence y in X by A7; end; for x being Element of H holds x "/\" has_an_upper_adjoint by A1,Def19; then A9: ex_max_of X,H by A3,A4,Th65; hence ex_sup_of X,H by Def5; A10: 'not' a is_>=_than X proof let b be Element of H; assume b in X; then consider x being Element of H such that A11: x = b and A12: a"/\"x <= Bottom H by A4; a => Bottom H >= x by A1,A12,Th70; hence 'not' a >= b by A11,Def22; end; now let b be Element of H such that A13: b is_>=_than X; a => (Bottom H) <= a => (Bottom H) by A3,ORDERS_1:24; then 'not' a <= a => (Bottom H) by Def22; then a"/\"'not' a <= Bottom H by A1,Th70; then 'not' a in X by A4; hence 'not' a <= b by A13,LATTICE3:def 9; end; hence 'not' a = "\/"(X,H) by A3,A10,YELLOW_0:30; thus "\/"(X,H) in X by A9,Def5; end; theorem Th83: for H being non empty RelStr st H is_a_Heyting_algebra & H is lower-bounded holds 'not' Bottom H = Top H & 'not' Top H = Bottom H proof let H be non empty RelStr such that A1: H is_a_Heyting_algebra and A2: H is lower-bounded; A3: H is LATTICE by A1,Def19; then Bottom H >= Bottom H "/\" Top H by YELLOW_0:23; then Top H <= (Bottom H) => (Bottom H) by A1,Th70; then A4: 'not' Bottom H >= Top H by Def22; A5: H is upper-bounded by A1,Th71; then 'not' Bottom H <= Top H by A3,YELLOW_0:45; hence Top H = 'not' Bottom H by A3,A4,ORDERS_1:25; (Top H) => (Bottom H) <= (Top H) => (Bottom H) by A3,ORDERS_1:24; then 'not' Top H <= (Top H) => (Bottom H) by Def22; then Bottom H >= Top H "/\" 'not' Top H & Bottom H <= Top H "/\" 'not' Top H by A1,A2,A3,Th70,YELLOW_0:44; then A6: Bottom H = Top H "/\" 'not' Top H by A3,ORDERS_1:25; 'not' Top H <= Top H by A3,A5,YELLOW_0:45; hence 'not' Top H = 'not' Top H"/\"Top H by A3,YELLOW_0:25 .= Bottom H by A3,A6,LATTICE3:15; end; :: Exercise 3.18 (i) theorem for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' a >= b iff 'not' b >= a proof let H be non empty lower-bounded RelStr such that A1: H is_a_Heyting_algebra; let a,b be Element of H; A2: H is LATTICE by A1,Def19; (Bottom H >= b "/\" a iff b => Bottom H >= a) & (Bottom H >= a "/\" b iff a => Bottom H >= b) by A1,Th70; hence 'not' a >= b iff 'not' b >= a by A2,Def22,LATTICE3:15; end; :: Exercise 3.18 (ii) theorem Th85: for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' a >= b iff a "/\" b = Bottom H proof let H be non empty lower-bounded RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is LATTICE by Def19; let a,b be Element of H; A3: a =>Bottom H = 'not' a by Def22; hereby A4: a "/\" b >= Bottom H by A2,YELLOW_0:44; assume 'not' a >= b; then a "/\" b <= Bottom H by A1,A3,Th70; hence a "/\" b = Bottom H by A2,A4,ORDERS_1:25; end; assume a "/\" b = Bottom H; then a "/\" b <= Bottom H by A2,ORDERS_1:24; hence 'not' a >= b by A1,A3,Th70; end; theorem for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H st a <= b holds 'not' b <= 'not' a proof let H be non empty lower-bounded RelStr such that A1: H is_a_Heyting_algebra; let a,b be Element of H; A2: H is LATTICE by A1,Def19; then A3: 'not' b >= 'not' b by ORDERS_1:24; assume a <= b; then a "/\" 'not' b = (a"/\"b)"/\"'not' b by A2,YELLOW_0:25 .= a"/\"(b"/\"'not' b) by A2,LATTICE3:16 .= a"/\"Bottom H by A1,A3,Th85 .= Bottom H"/\"a by A2,LATTICE3:15 .= Bottom H by A2,Th4; hence thesis by A1,Th85; end; theorem Th87: for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b proof let H be non empty lower-bounded RelStr; assume A1: H is_a_Heyting_algebra; let a,b be Element of H; thus 'not' (a"\/"b) = (a"\/"b)=> Bottom H by Def22 .= (a => Bottom H) "/\" (b => Bottom H) by A1,Th81 .= 'not' a "/\" (b => Bottom H) by Def22 .= 'not' a"/\"'not' b by Def22; end; theorem for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra for a,b being Element of H holds 'not' (a"/\"b) >= 'not' a"\/"'not' b proof let H be non empty lower-bounded RelStr; assume A1: H is_a_Heyting_algebra; then A2: H is distributive by Th69; let a,b be Element of H; A3: H is LATTICE by A1,Def19; then A4: 'not' a <= 'not' a by ORDERS_1:24; A5: 'not' b <= 'not' b by A3,ORDERS_1:24; A6: Bottom H<=Bottom H by A3,ORDERS_1:24; (a"/\"b)"/\"('not' a"\/"'not' b) = ((a"/\"b)"/\"'not' a)"\/"((a"/\"b)"/\" 'not' b) by A2,Def3 .= ((b"/\"a)"/\"'not' a)"\/"((a"/\"b)"/\" 'not' b) by A3,LATTICE3:15 .= (b"/\"(a"/\"'not' a))"\/"((a"/\"b)"/\" 'not' b) by A3,LATTICE3:16 .= (b"/\"(a"/\"'not' a))"\/"(a"/\"(b"/\" 'not' b)) by A3,LATTICE3:16 .= (b"/\"Bottom H)"\/"(a"/\"(b"/\"'not' b)) by A1,A4,Th85 .= (b"/\"Bottom H)"\/"(a"/\"Bottom H) by A1,A5,Th85 .= (Bottom H"/\"b)"\/"(a"/\"Bottom H) by A3,LATTICE3:15 .= (Bottom H"/\"b)"\/"(Bottom H"/\"a) by A3,LATTICE3:15 .= Bottom H"\/"(Bottom H"/\"a) by A3,Th4 .= Bottom H"\/"Bottom H by A3,Th4 .= Bottom H by A3,A6,YELLOW_0:24; hence thesis by A1,Th85; end; definition let L be non empty RelStr, x,y be Element of L; pred y is_a_complement_of x means :Def23: x "\/" y = Top L & x "/\" y = Bottom L; end; definition let L be non empty RelStr; attr L is complemented means :Def24: for x being Element of L ex y being Element of L st y is_a_complement_of x; end; definition let X be set; cluster BoolePoset X -> complemented; coherence proof let x be Element of BoolePoset X; A1: the carrier of BoolePoset X = the carrier of LattPOSet BooleLatt X by YELLOW_1:def 2 .= the carrier of RelStr (#the carrier of BooleLatt X, LattRel BooleLatt X#) by LATTICE3:def 2 .= bool X by LATTICE3:def 1; X\x c= X by XBOOLE_1:109; then reconsider y = X\x as Element of BoolePoset X by A1; take y; thus x "\/" y = x \/ y by YELLOW_1:17 .= X \/ x by XBOOLE_1:39 .= X by A1,XBOOLE_1:12 .= Top (BoolePoset X) by YELLOW_1:19; A2:x misses y by XBOOLE_1:79; thus x "/\" y = x /\ y by YELLOW_1:17 .= {} by A2,XBOOLE_0:def 7 .= Bottom (BoolePoset X) by YELLOW_1:18; end; end; :: Exercise 3.19 (1) implies (3) Lm7: for L being bounded LATTICE st L is distributive complemented for x being Element of L ex x' being Element of L st for y being Element of L holds (y "\/" x') "/\" x <= y & y <= (y "/\" x) "\/" x' proof let L be bounded LATTICE such that A1: L is distributive and A2: L is complemented; let x be Element of L; consider x' being Element of L such that A3: x' is_a_complement_of x by A2,Def24; take x'; let y be Element of L; (y "\/" x') "/\" x = (x "/\" y) "\/" (x "/\" x') by A1,Def3 .= Bottom L "\/" (x "/\" y) by A3,Def23 .= x "/\" y by Th4; hence (y "\/" x') "/\" x <= y by YELLOW_0:23; (y "/\" x) "\/" x' = (x' "\/" y) "/\" (x' "\/" x) by A1,Th6 .= (x' "\/" y) "/\" Top L by A3,Def23 .= x' "\/" y by Th5; hence y <= (y "/\" x) "\/" x' by YELLOW_0:22; end; :: Exercise 3.19 (3) implies (2) Lm8: for L being bounded LATTICE st for x being Element of L ex x' being Element of L st for y being Element of L holds (y "\/" x') "/\" x <= y & y <= (y "/\" x) "\/" x' holds L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not' x = x proof let L be bounded LATTICE; defpred P[Element of L, Element of L] means for y being Element of L holds (y "\/" $2) "/\" $1 <= y & y <= (y "/\" $1) "\/" $2; assume A1: for x being Element of L ex x' being Element of L st P[x,x']; consider g' being map of L,L such that A2: for x being Element of L holds P[x,g'.x] from NonUniqExMD(A1); A3: now let y be Element of L; let g be map of L,L such that A4: for z being Element of L holds g.z = g'.y "\/" z; A5: g is monotone proof let z1,z2 be Element of L; assume z1 <= z2; then g'.y "\/" z1 <= z2 "\/" g'.y by Th3; then g.z1 <= g'.y "\/" z2 by A4; hence thesis by A4; end; now let x be Element of L, z be Element of L; hereby assume x <= g.z; then x <= g'.y "\/" z by A4; then A6: x "/\" y <= (g'.y "\/" z) "/\" y by Th2; (g'.y "\/" z) "/\" y <= z by A2; then x "/\" y <= z by A6,ORDERS_1:26; hence (y "/\").x <= z by Def18; end; assume (y "/\").x <= z; then y "/\" x <= z by Def18; then A7: (x "/\" y) "\/" g'.y <= z "\/" g'.y by Th3; x <= (x "/\" y) "\/" g'.y by A2; then x <= z "\/" g'.y by A7,ORDERS_1:26; hence x <= g.z by A4; end; hence [g,y "/\"] is Galois by A5,Th9; end; thus A8: L is_a_Heyting_algebra proof thus L is LATTICE; let y be Element of L; deffunc F(Element of L) = g'.y "\/" $1; consider g being map of L,L such that A9: for z being Element of L holds g.z = F(z) from LambdaMD; [g,y "/\"] is Galois by A3,A9; hence y "/\" has_an_upper_adjoint by Def12; end; then A10: L is distributive by Th69; A11: now let x be Element of L; deffunc F(Element of L) = g'.x "\/" $1; consider g being map of L,L such that A12: for z being Element of L holds g.z = F(z) from LambdaMD; [g,x "/\"] is Galois by A3,A12; then A13: g = x => by A8,Def20; thus 'not' x = x => Bottom L by Def22 .= g.Bottom L by A13,Def21 .= Bottom L "\/" g'.x by A12 .= g'.x by Th4; end; A14: now let x be Element of L; Top L <= (Top L "/\" x) "\/" g'.x by A2; then A15: Top L <= x "\/" g'.x by Th5; x "\/" g'.x <= Top L by YELLOW_0:45; hence Top L = x "\/" g'.x by A15,ORDERS_1:25 .= x "\/" 'not' x by A11; end; A16: now let x be Element of L; (Bottom L "\/" g'.x) "/\" x <= Bottom L by A2; then (x "/\" Bottom L) "\/" (x "/\" g'.x) <= Bottom L by A10,Def3; then Bottom L "\/" (x "/\" g'.x) <= Bottom L by Th4; then A17: x "/\" g'.x <= Bottom L by Th4; Bottom L <= x "/\" g'.x by YELLOW_0:44; hence Bottom L = x "/\" g'.x by A17,ORDERS_1:25 .= x "/\" 'not' x by A11; end; let x be Element of L; ('not' x "\/" 'not' 'not' x) "/\" x = Top L "/\" x by A14; then x = x "/\" ('not' x "\/" 'not' 'not' x) by Th5 .= (x "/\" 'not' x) "\/" (x "/\" 'not' 'not' x) by A10,Def3 .= Bottom L "\/" (x "/\" 'not' 'not' x) by A16 .= x "/\" 'not' 'not' x by Th4; then A18: x <= 'not' 'not' x by YELLOW_0:25; Bottom L "\/" x = ('not' x "/\" 'not' 'not' x) "\/" x by A16; then x = x "\/" ('not' x "/\" 'not' 'not' x) by Th4 .= (x "\/" 'not' x) "/\" (x "\/" 'not' 'not' x) by A10,Th6 .= Top L "/\" (x "\/" 'not' 'not' x) by A14 .= x "\/" 'not' 'not' x by Th5; hence thesis by A18,YELLOW_0:24; end; :: Exercise 3.19 theorem Th89: for L being bounded LATTICE st L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not' x = x for x being Element of L holds 'not' x is_a_complement_of x proof let L be bounded LATTICE such that A1: L is_a_Heyting_algebra and A2: for x being Element of L holds 'not' 'not' x = x; let x be Element of L; A3: 'not' x >= 'not' x by ORDERS_1:24; then A4: x "/\" 'not' x = Bottom L by A1,Th85; 'not' (x "\/" 'not' x) = 'not' x "/\" 'not' 'not' x by A1,Th87 .= x "/\" 'not' x by A2; hence x "\/" 'not' x = 'not' (Bottom L) by A2,A4 .= Top L by A1,Th83; thus thesis by A1,A3,Th85; end; :: Exercise 3.19 (1) iff (2) theorem Th90: for L being bounded LATTICE holds L is distributive complemented iff L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not' x = x proof let L be bounded LATTICE; hereby assume L is distributive complemented; then for x being Element of L ex x' being Element of L st for y being Element of L holds (y "\/" x') "/\" x <= y & y <= (y "/\" x) "\/" x' by Lm7; hence L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not' x = x by Lm8; end; assume that A1: L is_a_Heyting_algebra and A2: for x being Element of L holds 'not' 'not' x = x; thus L is distributive by A1,Th69; let x be Element of L; take 'not' x; thus 'not' x is_a_complement_of x by A1,A2,Th89; end; :: Definition 3.20 definition let B be non empty RelStr; attr B is Boolean means :Def25: B is LATTICE & B is bounded distributive complemented; synonym B is_a_Boolean_algebra; synonym B is_a_Boolean_lattice; end; definition cluster Boolean -> reflexive transitive antisymmetric with_infima with_suprema bounded distributive complemented (non empty RelStr); coherence by Def25; end; definition cluster reflexive transitive antisymmetric with_infima with_suprema bounded distributive complemented -> Boolean (non empty RelStr); coherence by Def25; end; definition cluster Boolean -> Heyting (non empty RelStr); coherence proof let B be non empty RelStr; assume B is LATTICE & B is bounded distributive complemented; hence thesis by Th90; end; end; definition cluster strict Boolean non empty LATTICE; existence proof consider X being set; take BoolePoset X; thus thesis; end; end; definition cluster strict Heyting non empty LATTICE; existence proof consider L being strict Boolean non empty LATTICE; take L; thus thesis; end; end;