:: Galois Connections
:: by Czes\law Byli\'nski
::
:: Received September 25, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, STRUCT_0, FUNCT_1, SUBSET_1, ORDERS_2, SEQM_3,
XXREAL_0, RELAT_2, LATTICE3, LATTICES, EQREL_1, WAYBEL_0, YELLOW_1,
YELLOW_0, RELAT_1, CAT_1, WELLORD1, ORDINAL2, TARSKI, REWRITE1, CARD_FIL,
BINOP_1, FUNCT_2, GROUP_6, YELLOW_2, LATTICE2, XBOOLEAN, ZFMISC_1,
XXREAL_2, WAYBEL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
DOMAIN_1, STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, QUANTAL1, ORDERS_3,
YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2;
constructors DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, RELSET_1;
registrations RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_2, RELSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3, QUANTAL1, YELLOW_0, WAYBEL_0, XBOOLE_0;
equalities TARSKI, LATTICE3, WAYBEL_0, XBOOLE_0, YELLOW_2, STRUCT_0;
expansions TARSKI, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0, XBOOLE_0, STRUCT_0;
theorems ORDERS_2, FUNCT_1, FUNCT_2, LATTICE3, RELAT_1, TARSKI, WELLORD1,
YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, RELSET_1, XBOOLE_0, XBOOLE_1,
XTUPLE_0;
schemes FUNCT_2, DOMAIN_1;
begin :: Preliminaries
definition
let L1,L2 be non empty 1-sorted, f be Function of L1,L2;
redefine attr f is one-to-one means :: redefines one-to-one (FUNCT_1, definition)
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:19;
assume for x,y being Element of L1 st f.x = f.y holds x=y;
then for x,y be object st x in the carrier of L1 & y in the carrier of L1
holds f.x = f.y implies x=y;
hence thesis by FUNCT_2:19;
end;
end;
definition
let L1,L2 be non empty RelStr, f be Function of L1,L2;
redefine attr f is monotone means :: redefines monotone (ORDERS_3, definition)
for x,y being Element of L1 st x <= y holds f.x <= f.y;
compatibility;
end;
theorem Th1:
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;
A1: x"/\"z <= x by YELLOW_0:23;
A2: x"/\"z <= z by YELLOW_0:23;
assume x <= y;
then x"/\"z <= y by A1,ORDERS_2:3;
hence thesis by A2,YELLOW_0:23;
end;
theorem Th2:
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;
A1: y <= y"\/"z by YELLOW_0:22;
A2: z <= y"\/"z by YELLOW_0:22;
assume x <= y;
then x <= y"\/"z by A1,ORDERS_2:3;
hence thesis by A2,YELLOW_0:22;
end;
theorem Th3:
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 thesis by ORDERS_2:2;
end;
assume
A1: L is with_suprema;
then
A2: x <= Bottom L "\/" x by YELLOW_0:22;
assume L is reflexive transitive;
then
A3: x <= x;
Bottom L <= x by YELLOW_0:44;
then Bottom L "\/" x <= x by A1,A3,YELLOW_0:22;
hence thesis by A2,ORDERS_2:2;
end;
theorem Th4:
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;
then x "/\" x <= Top L "/\" x by Th1,YELLOW_0:45;
then
A2: x <= Top L "/\" x by A1,YELLOW_0:25;
Top L "/\" x <= x by A1,YELLOW_0:23;
hence thesis by A2,ORDERS_2:2;
end;
assume L is with_suprema;
then Top L "\/" x <= Top L & Top L <= Top L "\/" x by YELLOW_0:22,45;
hence thesis by ORDERS_2:2;
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 Th5:
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
.= ((x"\/"y)"/\"x)"\/"((x"\/"y)"/\"z) by LATTICE3:18
.= (x"\/"y)"/\"(x"\/"z) by A1;
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;
registration
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;
pred ex_max_of X,S means
ex_sup_of X,S & "\/"(X,S) in X;
end;
notation
let S be non empty RelStr, X be set;
synonym X has_the_min_in S for ex_min_of X,S;
synonym X has_the_max_in S for ex_max_of X,S;
end;
definition
let S be non empty RelStr, s be Element of S, X be set;
pred s is_minimum_of X means
ex_inf_of X,S & s = "/\"(X,S) & "/\"(X,S ) in X;
pred s is_maximum_of X means
ex_sup_of X,S & s = "\/"(X,S) & "\/"(X,S )in X;
end;
registration
let L be RelStr;
cluster id L -> isomorphic;
coherence
proof
per cases;
suppose
A1: L is non empty;
A2: id L = (id L)" by FUNCT_1:45;
id L is monotone;
hence thesis by A1,A2,WAYBEL_0:def 38;
end;
suppose
L is empty;
hence thesis by WAYBEL_0:def 38;
end;
end;
end;
definition
let L1,L2 be RelStr;
pred L1,L2 are_isomorphic means
ex f being Function 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 Function of L1,L2 such that
A1: f is isomorphic;
consider g being Function of L2,L1 such that
A2: g = (f qua Function)" and
A3: g is monotone by A1,WAYBEL_0:def 38;
f = (g qua Function)" by A1,A2,FUNCT_1:43;
then g is isomorphic by A1,A2,A3,WAYBEL_0:def 38;
hence thesis;
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 Function of L1,L2 such that
A1: f1 is isomorphic;
given f2 being Function of L2,L3 such that
A2: f2 is isomorphic;
A3: L1 is empty implies f2*f1 is Function of L1,L3 by FUNCT_2:13;
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 Function of L1,L2;
reconsider f2 as Function of L2,L3;
consider g1 being Function of L2,L1 such that
A4: g1 = (f1 qua Function)" & g1 is monotone by A1,WAYBEL_0:def 38;
consider g2 being Function of L3,L2 such that
A5: g2 = (f2 qua Function)" & g2 is monotone by A2,WAYBEL_0:def 38;
A6: f2*f1 is monotone by A1,A2,YELLOW_2:12;
g1*g2 is monotone & g1*g2 = ((f2*f1) qua Function)" by A1,A2,A4,A5,
FUNCT_1:44,YELLOW_2:12;
then f2*f1 is isomorphic by A1,A2,A6,WAYBEL_0:def 38;
hence thesis;
end;
suppose
A7: L1 is empty;
then reconsider f = f2*f1 as Function of L1,L3 by A3;
L2 is empty by A1,A7,WAYBEL_0:def 38;
then L3 is empty by A2,WAYBEL_0:def 38;
then f is isomorphic by A7,WAYBEL_0:def 38;
hence thesis;
end;
suppose
A8: L2 is empty;
then reconsider f = f2*f1 as Function of L1,L3 by A1,A3,WAYBEL_0:def 38;
L1 is empty & L3 is empty by A1,A2,A8,WAYBEL_0:def 38;
then f is isomorphic by WAYBEL_0:def 38;
hence thesis;
end;
suppose
A9: L3 is empty;
then
A10: L2 is empty by A2,WAYBEL_0:def 38;
then reconsider f = f2*f1 as Function of L1,L3 by A1,A3,WAYBEL_0:def 38;
L1 is empty by A1,A10,WAYBEL_0:def 38;
then f is isomorphic by A9,WAYBEL_0:def 38;
hence thesis;
end;
end;
begin :: Galois Connections
definition
let S,T be RelStr;
mode Connection of S,T -> set means
:Def9:
ex g being Function of S,T, d being Function of T,S st it = [g,d];
existence
proof
set g = the Function of S,T,d = the Function of T,S;
take [g,d];
thus thesis;
end;
end;
definition
let S,T be RelStr, g be Function of S,T, d be Function of T,S;
redefine func [g,d] -> Connection of S,T; :: redefines [ (TARSKI, definition)
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
ex g being Function of S,T, d being Function
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 Th8:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
hereby
assume [g,d] is Galois;
then consider g9 being Function of S,T, d9 being Function of T,S such that
A1: [g,d] = [g9,d9] and
A2: g9 is monotone & d9 is monotone & for t being Element of T, s
being Element of S holds t <= g9.s iff d9.t <= s;
g = g9 & d = d9 by A1,XTUPLE_0:1;
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;
end;
:: Definition 3.1
definition
let S,T be non empty RelStr, g be Function of S,T;
attr g is upper_adjoint means
ex d being Function of T,S st [g,d] is Galois;
end;
:: Definition 3.1
definition
let S,T be non empty RelStr, d be Function of T,S;
attr d is lower_adjoint means
:Def12:
ex g being Function of S,T st [g,d] is Galois;
end;
theorem
for S,T being non empty Poset,g being Function of S,T, d being
Function of T,S st [g,d] is Galois holds g is upper_adjoint & d is
lower_adjoint;
:: Theorem 3.2 (1) iff (2)
theorem Th10:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
hereby
assume
A1: [g,d] is Galois;
hence g is monotone by Th8;
let t be Element of T;
thus d.t is_minimum_of g"(uparrow t)
proof
set X = g"(uparrow t);
t <= g.(d.t) by A1,Th8;
then g.(d.t) in uparrow t by WAYBEL_0:18;
then
A2: d.t in X by FUNCT_2:38;
then
A3: for s being Element of S st s is_<=_than X holds d.t >= s;
A4: 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 7;
then t <= g.s by WAYBEL_0:18;
hence d.t <= s by A1,Th8;
end;
hence ex_inf_of X,S & d.t = inf X by A3,YELLOW_0:31;
thus thesis by A4,A2,A3,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: 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);
hereby
assume t <= g.s;
then g.s in uparrow t by WAYBEL_0:18;
then
A8: s in X by FUNCT_2:38;
A9: d.t is_minimum_of g"(uparrow t) by A6;
then ex_inf_of X,S;
then X is_>=_than inf X by YELLOW_0:def 10;
then s >= inf X by A8;
hence d.t <= s by A9;
end;
A10: d.t is_minimum_of X by A6;
then inf X in X;
then g.(inf X) in uparrow t by FUNCT_1:def 7;
then g.(inf X) >= t by WAYBEL_0:18;
then
A11: g.(d.t) >= t by A10;
assume d.t <= s;
then g.(d.t) <= g.s by A5;
hence thesis by A11,ORDERS_2:3;
end;
d is monotone
proof
let t1,t2 be Element of T;
assume t1 <= t2;
then
A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22;
A13: d.t2 is_minimum_of g"(uparrow t2) by A6;
then
A14: ex_inf_of g"(uparrow t2),S;
A15: d.t1 is_minimum_of g"(uparrow t1) by A6;
then ex_inf_of g"(uparrow t1),S;
then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A14,A12,RELAT_1:143
,YELLOW_0:35;
then d.t1 <= inf (g"(uparrow t2)) by A15;
hence d.t1 <= d.t2 by A13;
end;
hence thesis by A5,A7;
end;
:: Theorem 3.2 (1) iff (3)
theorem Th11:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
hereby
assume
A1: [g,d] is Galois;
hence d is monotone by Th8;
let s be Element of S;
thus g.s is_maximum_of d"(downarrow s)
proof
set X = d"(downarrow s);
s >= d.(g.s) by A1,Th8;
then d.(g.s) in downarrow s by WAYBEL_0:17;
then
A2: g.s in X by FUNCT_2:38;
then
A3: for t being Element of T st t is_>=_than X holds g.s <= t;
A4: 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 7;
then s >= d.t by WAYBEL_0:17;
hence thesis by A1,Th8;
end;
hence ex_sup_of X,T & g.s = sup X by A3,YELLOW_0:30;
thus thesis by A4,A2,A3,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: 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);
A8: g.s is_maximum_of X by A6;
then sup X in X;
then d.(sup X) in downarrow s by FUNCT_1:def 7;
then d.(sup X) <= s by WAYBEL_0:17;
then
A9: d.(g.s) <= s by A8;
hereby
assume s >= d.t;
then d.t in downarrow s by WAYBEL_0:17;
then
A10: t in X by FUNCT_2:38;
ex_sup_of X,T by A8;
then X is_<=_than sup X by YELLOW_0:def 9;
then t <= sup X by A10;
hence g.s >= t by A8;
end;
assume g.s >= t;
then d.(g.s) >= d.t by A5;
hence thesis by A9,ORDERS_2:3;
end;
g is monotone
proof
let s1,s2 be Element of S;
assume s1 <= s2;
then
A11: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
A12: g.s2 is_maximum_of d"(downarrow s2) by A6;
then
A13: ex_sup_of d"(downarrow s2),T;
A14: g.s1 is_maximum_of d"(downarrow s1) by A6;
then ex_sup_of d"(downarrow s1),T;
then sup (d"(downarrow s1)) <= sup (d"(downarrow s2)) by A13,A11,
RELAT_1:143,YELLOW_0:34;
then g.s1 <= sup (d"(downarrow s2)) by A14;
hence g.s1 <= g.s2 by A12;
end;
hence thesis by A5,A7;
end;
:: Theorem 3.3 (first part)
theorem Th12:
for S,T being non empty Poset,g being Function of S,T st g is
upper_adjoint holds g is infs-preserving
proof
let S,T be non empty Poset,g be Function of S,T;
given d being Function of T,S such that
A1: [g,d] is Galois;
let X be Subset of S;
set s = inf X;
assume
A2: ex_inf_of X,S;
A3: for t being Element of T st t is_<=_than g.:X holds g.s >= t
proof
let t be Element of T;
assume
A4: 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:35;
then t <= g.si by A4;
hence d.t <= si by A1,Th8;
end;
then d.t <= s by A2,YELLOW_0:31;
hence thesis by A1,Th8;
end;
g.s is_<=_than g.:X
proof
let t be Element of T;
assume t in g.:X;
then consider si being Element of S such that
A5: si in X and
A6: t = g.si by FUNCT_2:65;
A7: g is monotone by A1,Th8;
reconsider si as Element of S;
s is_<=_than X by A2,YELLOW_0:31;
then s <= si by A5;
hence g.s <= t by A7,A6;
end;
hence thesis by A3,YELLOW_0:31;
end;
registration
let S,T be non empty Poset;
cluster upper_adjoint -> infs-preserving for Function of S,T;
coherence by Th12;
end;
:: Theorem 3.3 (second part)
theorem Th13:
for S,T being non empty Poset, d being Function of T,S st d is
lower_adjoint holds d is sups-preserving
proof
let S,T be non empty Poset, d be Function of T,S;
given g being Function of S,T such that
A1: [g,d] is Galois;
let X be Subset of T;
set t = sup X;
assume
A2: ex_sup_of X,T;
A3: for s being Element of S st s is_>=_than d.:X holds d.t <= s
proof
let s be Element of S;
assume
A4: 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:35;
then s >= d.ti by A4;
hence thesis by A1,Th8;
end;
then g.s >= t by A2,YELLOW_0:30;
hence thesis by A1,Th8;
end;
d.t is_>=_than d.:X
proof
let s be Element of S;
assume s in d.:X;
then consider ti being Element of T such that
A5: ti in X and
A6: s = d.ti by FUNCT_2:65;
A7: d is monotone by A1,Th8;
reconsider ti as Element of T;
t is_>=_than X by A2,YELLOW_0:30;
then t >= ti by A5;
hence thesis by A7,A6;
end;
hence thesis by A3,YELLOW_0:30;
end;
registration
let S,T be non empty Poset;
cluster lower_adjoint -> sups-preserving for Function of S,T;
coherence by Th13;
end;
:: Theorem 3.4
theorem Th14:
for S,T being non empty Poset,g being Function of S,T st S is
complete & g is infs-preserving ex d being Function 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 Function of S,T;
assume that
A1: S is complete and
A2: g is infs-preserving;
defpred P[object,object] means
ex t being Element of T st t = $1 & $2 = inf (g"(
uparrow t));
A3: for e being object st e in the carrier of T
ex u being object st u in the carrier of S & P[e,u]
proof
let e be object;
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 object st e in the carrier of T holds P[e,d.e] from FUNCT_2
:sch 1(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 Function of T,S;
for X being Filter of S holds g preserves_inf_of X by A2;
then
A6: g is monotone by WAYBEL_0:69;
A7: 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;
A8: ex_inf_of uparrow t,T by WAYBEL_0:39;
A9: 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
A10: 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:38;
hence d.t <= s by A10;
end;
g preserves_inf_of (g"(uparrow t)) by A2;
then
ex_inf_of g.:(g"(uparrow t)),T & g.(inf (g"(uparrow t))) = inf (g.:(g
"( uparrow t))) by A9;
then g.(inf (g"(uparrow t))) >= inf(uparrow t) by A8,FUNCT_1:75,YELLOW_0:35
;
then
A11: g.(inf (g"(uparrow t))) >= t by WAYBEL_0:39;
assume d.t <= s;
then g.(d.t) <= g.s by A6;
then g.(inf (g"(uparrow t))) <= g.s by A5;
hence thesis by A11,ORDERS_2:3;
end;
take d;
d is monotone
proof
let t1,t2 be Element of T;
assume t1 <= t2;
then
A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22;
ex_inf_of g"(uparrow t1),S & ex_inf_of g"(uparrow t2),S by A1,YELLOW_0:17;
then inf (g"(uparrow t1)) <= inf (g"(uparrow t2)) by A12,RELAT_1:143
,YELLOW_0:35;
then d.t1 <= inf (g"(uparrow t2)) by A5;
hence d.t1 <= d.t2 by A5;
end;
hence [g,d] is Galois by A6,A7;
let t be Element of T;
thus
A13: ex_inf_of g"(uparrow t),S by A1,YELLOW_0:17;
thus
A14: d.t = inf (g"(uparrow t)) by A5;
A15: ex_inf_of uparrow t,T by WAYBEL_0:39;
g preserves_inf_of (g"(uparrow t)) by A2;
then
ex_inf_of g.:(g"(uparrow t)),T & g.(inf (g"(uparrow t))) = inf (g.:(g"(
uparrow t))) by A13;
then g.(inf (g"(uparrow t))) >= inf(uparrow t) by A15,FUNCT_1:75,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 thesis by A14,FUNCT_2:38;
end;
:: Theorem 3.4 (dual)
theorem Th15:
for S,T being non empty Poset, d being Function of T,S st T is
complete & d is sups-preserving ex g being Function 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 Function of T,S;
assume that
A1: T is complete and
A2: d is sups-preserving;
defpred P[object,object] means
ex s being Element of S st s = $1 & $2 = sup (d"(
downarrow s));
A3: for e being object st e in the carrier of S
ex u being object st u in the carrier of T & P[e,u]
proof
let e be object;
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 object st e in the carrier of S holds P[e,g.e] from FUNCT_2
:sch 1(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 Function of S,T;
for X being Ideal of T holds d preserves_sup_of X by A2;
then
A6: d is monotone by WAYBEL_0:72;
A7: 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;
A8: ex_sup_of downarrow s,S by WAYBEL_0:34;
A9: 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
A10: 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:38;
hence g.s >= t by A10;
end;
d preserves_sup_of (d"(downarrow s)) by A2;
then
ex_sup_of d.:(d"(downarrow s)),S & d.(sup (d"(downarrow s))) = sup (d
.:(d"( downarrow s))) by A9;
then d.(sup (d"(downarrow s))) <= sup(downarrow s) by A8,FUNCT_1:75
,YELLOW_0:34;
then
A11: d.(sup (d"(downarrow s))) <= s by WAYBEL_0:34;
assume g.s >= t;
then d.(g.s) >= d.t by A6;
then d.(sup (d"(downarrow s))) >= d.t by A5;
hence thesis by A11,ORDERS_2:3;
end;
take g;
g is monotone
proof
let s1,s2 be Element of S;
assume s1 <= s2;
then
A12: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
ex_sup_of d"(downarrow s1),T & ex_sup_of d"(downarrow s2),T by A1,
YELLOW_0:17;
then sup (d"(downarrow s1)) <= sup (d"(downarrow s2)) by A12,RELAT_1:143
,YELLOW_0:34;
then g.s1 <= sup (d"(downarrow s2)) by A5;
hence g.s1 <= g.s2 by A5;
end;
hence [g,d] is Galois by A6,A7;
let s be Element of S;
thus
A13: ex_sup_of d"(downarrow s),T by A1,YELLOW_0:17;
thus
A14: g.s = sup (d"(downarrow s)) by A5;
A15: ex_sup_of downarrow s,S by WAYBEL_0:34;
d preserves_sup_of (d"(downarrow s)) by A2;
then
ex_sup_of d.:(d"(downarrow s)),S & d.(sup (d"(downarrow s))) = sup (d.:
(d"( downarrow s))) by A13;
then d.(sup (d"(downarrow s))) <= sup(downarrow s) by A15,FUNCT_1:75
,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 thesis by A14,FUNCT_2:38;
end;
:: Corollary 3.5 (i)
theorem
for S,T being non empty Poset, g being Function of S,T st S is
complete holds (g is infs-preserving iff g is monotone & g is upper_adjoint)
proof
let S,T be non empty Poset,g be Function of S,T;
assume
A1: S is complete;
hereby
assume g is infs-preserving;
then
ex d being Function 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,Th14;
hence g is monotone & g is upper_adjoint by Th10;
end;
assume g is monotone;
assume ex d being Function of T,S st [g,d] is Galois;
then g is upper_adjoint;
hence thesis;
end;
:: Corollary 3.5 (ii)
theorem Th17:
for S,T being non empty Poset, d being Function of T,S st T is
complete holds d is sups-preserving iff d is monotone & d is lower_adjoint
proof
let S,T be non empty Poset, d be Function of T,S;
assume
A1: T is complete;
hereby
assume d is sups-preserving;
then
ex g being Function 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,Th15;
hence d is monotone & d is lower_adjoint by Th11;
end;
assume d is monotone;
assume ex g being Function of S,T st [g,d] is Galois;
then d is lower_adjoint;
hence thesis;
end;
:: Theorem 3.6 (1) iff (2)
theorem Th18:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function 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,Th8;
then (d*g).s <= s by FUNCT_2:15;
hence thesis;
end;
hence d*g <= id S by YELLOW_2:9;
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,Th8;
then t <= (g*d).t by FUNCT_2:15;
hence thesis;
end;
hence thesis by YELLOW_2:9;
end;
:: Theorem 3.6 (2) implies (1)
theorem Th19:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function 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
(d*g).s <= (id S).s by A3,YELLOW_2:9;
then d.(g.s) <= (id S).s by FUNCT_2:15;
then
A5: d.(g.s) <= s;
assume t <= g.s;
then d.t <= d.(g.s) by A2;
hence d.t <= s by A5,ORDERS_2:3;
end;
(id T).t <= (g*d).t by A4,YELLOW_2:9;
then (id T).t <= g.(d.t) by FUNCT_2:15;
then
A6: t <= g.(d.t);
assume d.t <= s;
then g.(d.t) <= g.s by A1;
hence thesis by A6,ORDERS_2:3;
end;
hence thesis by A1,A2;
end;
:: Theorem 3.6 (2) implies (3)
theorem Th20:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function 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:9;
then t <= (g*d).t;
then d.t <= d.((g*d).t) by A2;
then d.t <= (d*(g*d)).t by FUNCT_2:15;
then
A5: d.t <= (d*g*d).t by RELAT_1:36;
(d*g).(d.t) <= (id S).(d.t) by A3,YELLOW_2:9;
then (d*g).(d.t) <= d.t;
then d.t >= (d*g*d).t by FUNCT_2:15;
hence thesis by A5,ORDERS_2:2;
end;
hence d = d*g*d by FUNCT_2:63;
for s being Element of S holds g.s = (g*d*g).s
proof
let s be Element of S;
(d*g).s <= (id S).s by A3,YELLOW_2:9;
then (d*g).s <= s;
then g.((d*g).s) <= g.s by A1;
then (g*(d*g)).s <= g.s by FUNCT_2:15;
then
A6: g.s >= (g*d*g).s by RELAT_1:36;
(id T).(g.s) <= (g*d).(g.s) by A4,YELLOW_2:9;
then (g.s) <= (g*d).(g.s);
then g.s <= (g*d*g).s by FUNCT_2:15;
hence thesis by A6,ORDERS_2:2;
end;
hence thesis by FUNCT_2:63;
end;
:: Theorem 3.6 (3) implies (4)
theorem Th21:
for S,T being non empty RelStr, g being Function of S,T, d being
Function of T,S st g = g*d*g holds g*d is idempotent
proof
let S,T be non empty RelStr, g be Function of S,T, d be Function of T,S;
assume g = g*d*g;
hence (g*d)*(g*d) = g*d by RELAT_1:36;
end;
:: Proposition 3.7 (1) implies (2)
theorem Th22:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
assume that
A1: [g,d] is Galois and
A2: g is onto;
A3: g is monotone by A1,Th8;
let t be Element of T;
A4: rng g = the carrier of T by A2,FUNCT_2:def 3;
then
A5: g.:(g"(uparrow t)) = uparrow t by FUNCT_1:77;
A6: d.t is_minimum_of g"(uparrow t) by A1,Th10;
then
A7: d.t = inf (g"(uparrow t));
d.t in g"(uparrow t) by A6;
then g.(d.t) in g.:(g"(uparrow t)) by FUNCT_2:35;
then
A8: t <= g.(d.t) by A5,WAYBEL_0:18;
ex_inf_of g"(uparrow t),S by A6;
then
A9: d.t is_<=_than g"(uparrow t) by A7,YELLOW_0:31;
consider s being object such that
A10: s in the carrier of S and
A11: g.s = t by A4,FUNCT_2:11;
reconsider s as Element of S by A10;
A12: t in {t} by TARSKI:def 1;
A13: {t} c= uparrow {t} by WAYBEL_0:16;
then s in g"(uparrow t) by A11,A12,FUNCT_2:38;
then d.t <= s by A9;
then g.(d.t) <= t by A11,A3;
then
A14: g.(d.t) = t by A8,ORDERS_2:2;
then
A15: d.t in g"{t} by A12,FUNCT_2:38;
A16: g"{t} c= g"(uparrow t) by RELAT_1:143,WAYBEL_0:16;
thus
A17: ex_inf_of g"{t},S
proof
take d.t;
thus g"{t} is_>=_than d.t by A9,A16;
thus for b be Element of S st g"{t} is_>=_than b holds b <= d.t by A15;
let c be Element of S;
assume g"{t} is_>=_than c;
then
A18: c <= d.t by A15;
assume for b being Element of S st g"{t} is_>=_than b holds b <= c;
then d.t <= c by A9,A16,YELLOW_0:9;
hence thesis by A18,ORDERS_2:2;
end;
then inf (g"{t}) is_<=_than g"{t} by YELLOW_0:31;
then
A19: inf (g"{t}) <= d.t by A15;
ex_inf_of g"(uparrow t),S by A6;
then inf (g"{t}) >= d.t by A7,A13,A17,RELAT_1:143,YELLOW_0:35;
hence d.t = inf(g"{t}) by A19,ORDERS_2:2;
hence thesis by A12,A14,FUNCT_2:38;
end;
:: Proposition 3.7 (2) implies (3)
theorem Th23:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function 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};
then g.(d.t) in {t} by FUNCT_2:38;
then g.(d.t) = t by TARSKI:def 1;
hence thesis by FUNCT_2:15;
end;
hence thesis by FUNCT_2:124;
end;
:: Proposition 3.7 (4) iff (1)
theorem
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
A1: the carrier of T = dom d & the carrier of T = dom (g*d) by FUNCT_2:def 1;
assume
A2: [g,d] is Galois;
then
A3: d*g <= id S & id T <= g*d by Th18;
hereby
assume g is onto;
then for t being Element of T holds d.t is_minimum_of g"{t} by A2,Th22;
then g*d = id T by Th23;
hence d is one-to-one by FUNCT_2:23;
end;
A4: rng (g*d) c= the carrier of T;
g is monotone & d is monotone by A2,Th8;
then
A5: d = d*g*d by A3,Th20
.= d*(g*d) by RELAT_1:36;
assume d is one-to-one;
then g*d = id T by A1,A4,A5,FUNCT_1:28;
hence thesis by FUNCT_2:23;
end;
:: Proposition 3.7 (1*) implies (2*)
theorem Th25:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
assume that
A1: [g,d] is Galois and
A2: d is onto;
A3: d is monotone by A1,Th8;
let s be Element of S;
A4: rng d = the carrier of S by A2,FUNCT_2:def 3;
then
A5: d.:(d"(downarrow s)) = downarrow s by FUNCT_1:77;
A6: g.s is_maximum_of (d"(downarrow s)) by A1,Th11;
then
A7: g.s = sup (d"(downarrow s));
g.s in d"(downarrow s) by A6;
then d.(g.s) in d.:(d"(downarrow s)) by FUNCT_2:35;
then
A8: s >= d.(g.s) by A5,WAYBEL_0:17;
ex_sup_of d"(downarrow s),T by A6;
then
A9: g.s is_>=_than d"(downarrow s) by A7,YELLOW_0:30;
consider t being object such that
A10: t in the carrier of T and
A11: d.t = s by A4,FUNCT_2:11;
reconsider t as Element of T by A10;
A12: s in {s} by TARSKI:def 1;
A13: {s} c= downarrow {s} by WAYBEL_0:16;
then t in d"(downarrow s) by A11,A12,FUNCT_2:38;
then g.s >= t by A9;
then d.(g.s) >= s by A11,A3;
then
A14: d.(g.s) = s by A8,ORDERS_2:2;
then
A15: g.s in d"{s} by A12,FUNCT_2:38;
A16: d"{s} c= d"(downarrow s) by RELAT_1:143,WAYBEL_0:16;
thus
A17: ex_sup_of d"{s},T
proof
take g.s;
thus d"{s} is_<=_than g.s by A9,A16;
thus for b be Element of T st d"{s} is_<=_than b holds b >= g.s by A15;
let c be Element of T;
assume d"{s} is_<=_than c;
then
A18: c >= g.s by A15;
assume for b being Element of T st d"{s} is_<=_than b holds b >= c;
then g.s >= c by A9,A16,YELLOW_0:9;
hence thesis by A18,ORDERS_2:2;
end;
then sup (d"{s}) is_>=_than d"{s} by YELLOW_0:30;
then
A19: sup (d"{s}) >= g.s by A15;
ex_sup_of d"(downarrow s),T by A6;
then sup (d"{s}) <= g.s by A7,A13,A17,RELAT_1:143,YELLOW_0:34;
hence g.s = sup(d"{s}) by A19,ORDERS_2:2;
hence thesis by A12,A14,FUNCT_2:38;
end;
:: Proposition 3.7 (2*) implies (3*)
theorem Th26:
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function 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};
then d.(g.s) in {s} by FUNCT_2:38;
then d.(g.s) = s by TARSKI:def 1;
hence thesis by FUNCT_2:15;
end;
hence thesis by FUNCT_2:124;
end;
:: Proposition 3.7 (1*) iff (4*)
theorem
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T, d be Function of T,S;
assume
A1: [g,d] is Galois;
hereby
A2: d*g <= id S & id T <= g*d by A1,Th18;
g is monotone & d is monotone by A1,Th8;
then
A3: g = g*d*g by A2,Th20
.= g*(d*g) by RELAT_1:36;
A4: the carrier of S = dom g & the carrier of S = dom (d*g) by FUNCT_2:def 1;
A5: rng (d*g) c= the carrier of S;
assume g is one-to-one;
then d*g = id S by A4,A5,A3,FUNCT_1:28;
hence d is onto by FUNCT_2:23;
end;
assume d is onto;
then for s being Element of S holds g.s is_maximum_of d"{s} by A1,Th25;
then d*g = id S by Th26;
hence thesis by FUNCT_2:23;
end;
:: Definition 3.8 (i)
definition
let L be non empty RelStr, p be Function of L,L;
attr p is projection means
:Def13:
p is idempotent monotone;
end;
registration
let L be non empty RelStr;
cluster id L -> projection;
coherence
by YELLOW_2:21;
end;
registration
let L be non empty RelStr;
cluster projection for Function 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 Function of L,L;
attr c is closure means
c is projection & id(L) <= c;
end;
registration
let L be non empty RelStr;
cluster closure -> projection for Function of L,L;
coherence;
end;
Lm1: for L1,L2 being non empty RelStr, f being Function of L1,L2 st L2 is
reflexive holds f <= f
proof
let L1,L2 be non empty RelStr, f be Function of L1,L2;
assume L2 is reflexive;
then for x be Element of L1 holds f.x <= f.x;
hence thesis by YELLOW_2:9;
end;
registration
let L be non empty reflexive RelStr;
cluster closure for Function of L,L;
existence
proof
take id L;
thus id L is projection;
thus thesis by Lm1;
end;
end;
registration
let L be non empty reflexive RelStr;
cluster id L -> closure;
coherence
by Lm1;
end;
:: Definition 3.8 (iii)
definition
let L be non empty RelStr, k be Function of L,L;
attr k is kernel means
k is projection & k <= id(L);
end;
registration
let L be non empty RelStr;
cluster kernel -> projection for Function of L,L;
coherence;
end;
registration
let L be non empty reflexive RelStr;
cluster kernel for Function of L,L;
existence
proof
take id L;
thus id L is projection;
thus thesis by Lm1;
end;
end;
registration
let L be non empty reflexive RelStr;
cluster id L -> kernel;
coherence
by Lm1;
end;
Lm2: for L being non empty 1-sorted, p being Function 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 Function of L,L such that
A1: p is idempotent;
let x be set;
assume x in rng p;
then ex a being object st a in dom p & x = p.a by FUNCT_1:def 3;
hence thesis by A1,YELLOW_2:18;
end;
theorem Th28:
for L being non empty Poset, c being Function of L,L, X being
Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds inf X = c.(inf X
)
proof
let L be non empty Poset, c be Function of L,L, X be Subset of L such that
A1: c is projection and
A2: id(L) <= c and
A3: ex_inf_of X,L and
A4: X c= rng c;
A5: c is monotone by A1;
A6: c is idempotent by A1;
c.(inf X) is_<=_than X
proof
let x be Element of L;
assume
A7: x in X;
inf X is_<=_than X by A3,YELLOW_0:31;
then inf X <= x by A7;
then c.(inf X) <= c.x by A5;
hence thesis by A4,A6,A7,Lm2;
end;
then
A8: c.(inf X) <= inf X by A3,YELLOW_0:31;
id(L).(inf X) <= c.(inf X) by A2,YELLOW_2:9;
then inf X <= c.(inf X);
hence thesis by A8,ORDERS_2:2;
end;
theorem Th29:
for L being non empty Poset, k being Function of L,L, X being
Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds sup X = k.(sup X)
proof
let L be non empty Poset, k be Function of L,L, X be Subset of L such that
A1: k is projection and
A2: k <= id(L) and
A3: ex_sup_of X,L and
A4: X c= rng k;
A5: k is monotone by A1;
A6: k is idempotent by A1;
k.(sup X) is_>=_than X
proof
let x be Element of L;
assume
A7: x in X;
sup X is_>=_than X by A3,YELLOW_0:30;
then sup X >= x by A7;
then k.(sup X) >= k.x by A5;
hence thesis by A4,A6,A7,Lm2;
end;
then
A8: k.(sup X) >= sup X by A3,YELLOW_0:30;
id(L).(sup X) >= k.(sup X) by A2,YELLOW_2:9;
then sup X >= k.(sup X);
hence thesis by A8,ORDERS_2:2;
end;
definition
let L1, L2 be non empty RelStr, g be Function of L1,L2;
func corestr(g) -> Function of L1,Image g equals
(the carrier of Image g)|`g;
coherence
proof
A1: the carrier of L1 = dom g by FUNCT_2:def 1;
A2: the carrier of Image g = rng g by YELLOW_0:def 15;
thus thesis by A2,A1,FUNCT_2:1;
end;
end;
theorem Th30:
for L1, L2 being non empty RelStr,g being Function of L1,L2
holds corestr g = g
proof
let L1, L2 be non empty RelStr, g be Function of L1,L2;
the carrier of Image g = rng g by YELLOW_0:def 15;
hence thesis;
end;
Lm3: for L1, L2 being non empty RelStr, g being Function of L1,L2 holds
corestr g is onto
proof
let L1, L2 be non empty RelStr, g be Function of L1,L2;
the carrier of Image g = rng g by YELLOW_0:def 15
.= rng corestr g by Th30;
hence thesis by FUNCT_2:def 3;
end;
registration
let L1, L2 be non empty RelStr, g be Function of L1,L2;
cluster corestr g -> onto;
coherence by Lm3;
end;
theorem Th31:
for L1, L2 being non empty RelStr, g being Function of L1,L2 st
g is monotone holds corestr g is monotone
proof
let L1, L2 be non empty RelStr, g be Function of L1,L2 such that
A1: g is monotone;
let s1,s2 be Element of L1;
assume s1 <= s2;
then
A2: g.s1 <= g.s2 by A1;
reconsider s19 = g.s1, s29 = g.s2 as Element of L2;
s19 = (corestr g).s1 & s29 = (corestr g).s2 by Th30;
hence thesis by A2,YELLOW_0:60;
end;
definition
let L1, L2 be non empty RelStr, g be Function of L1,L2;
func inclusion(g) -> Function of Image g,L2 equals
id Image g;
coherence
proof
A1: rng id Image g = the carrier of Image g
.= rng g by YELLOW_0:def 15;
dom id Image g = the carrier of Image g;
hence thesis by A1,RELSET_1:4;
end;
end;
Lm4: for L1, L2 being non empty RelStr,g being Function of L1,L2 holds
inclusion g is monotone
by YELLOW_0:59;
registration
let L1, L2 be non empty RelStr, g be Function of L1,L2;
cluster inclusion g -> one-to-one monotone;
coherence by Lm4;
end;
theorem Th32:
for L being non empty RelStr, f being Function of L,L holds (
inclusion f)*(corestr f) = f
proof
let L be non empty RelStr, f be Function of L,L;
thus (inclusion f)*(corestr f) = (id the carrier of Image f)*f by Th30
.= (id rng f)*f by YELLOW_0:def 15
.= f by RELAT_1:54;
end;
::Theorem 3.10 (1) implies (2)
theorem Th33:
for L being non empty Poset, f being Function of L,L st f is
idempotent holds (corestr f)*(inclusion f) = id(Image f)
proof
let L be non empty Poset, f be Function 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 object such that
A2: l in the carrier of L and
A3: (corestr f).l = s by FUNCT_2:11;
reconsider l as Element of L by A2;
A4: (corestr f).l = f.l by Th30;
thus ((corestr f)*(inclusion f)).s = (corestr f).((inclusion f).s) by
FUNCT_2:15
.= (corestr f).s
.= f.(f.l) by A3,A4,Th30
.= s by A1,A3,A4,YELLOW_2:18;
end;
hence thesis by FUNCT_2:124;
end;
::Theorem 3.10 (1) implies (3)
theorem
for L being non empty Poset, f being Function of L,L st f is
projection ex T being non empty Poset, q being Function of L,T, i being
Function 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 Function of L,L;
reconsider T = Image f as non empty Poset;
reconsider q = corestr f as Function of L,T;
reconsider i = inclusion f as Function of T,L;
assume f is projection;
then
A1: f is monotone idempotent;
take T,q,i;
thus q is monotone by A1,Th31;
thus q is onto;
thus i is monotone one-to-one;
thus f = i*q by Th32;
thus thesis by A1,Th33;
end;
::Theorem 3.10 (3) implies (1)
theorem
for L being non empty Poset, f being Function of L,L st (ex T being
non empty Poset, q being Function of L,T, i being Function of T,L st q is
monotone & i is monotone & f = i*q & id(T) = q*i) holds f is projection
proof
let L be non empty Poset, f be Function of L,L;
given T being non empty Poset, q being Function of L,T, i being Function of
T,L such that
A1: q is monotone & i is monotone and
A2: f = i*q and
A3: id(T) = q*i;
i*q*i = i*(id the carrier of T) by A3,RELAT_1:36
.= i by FUNCT_2:17;
hence f is idempotent by A2,Th21;
thus thesis by A1,A2,YELLOW_2:12;
end;
::Theorem 3.10 (1_1) implies (2_1)
theorem Th36:
for L being non empty Poset, f being Function of L,L st f is
closure holds [inclusion f,corestr f] is Galois
proof
let L be non empty Poset, f be Function of L,L;
assume that
A1: f is idempotent monotone and
A2: id L <= f;
set g = (corestr f), d = inclusion f;
g*d = id(Image f) by A1,Th33;
then
A3: g*d <= id(Image f) by Lm1;
g is monotone & id L <= d*g by A1,A2,Th31,Th32;
hence thesis by A3,Th19;
end;
::Theorem 3.10 (2_1) implies (3_1)
theorem
for L being non empty Poset, f being Function of L,L st f is closure
ex S being non empty Poset, g being Function of S,L, d being Function of L,S st
[g,d] is Galois & f = g*d
proof
let L be non empty Poset, f be Function of L,L;
assume
A1: f is closure;
reconsider S = Image f as non empty Poset;
reconsider g = inclusion f as Function of S,L;
reconsider d = corestr f as Function of L,S;
take S,g,d;
thus [g,d] is Galois by A1,Th36;
thus thesis by Th32;
end;
::Theorem 3.10 (3_1) implies (1_1)
theorem Th38:
for L being non empty Poset, f being Function of L,L st f is
monotone & ex S being non empty Poset, g being Function of S,L, d being
Function of L,S st [g,d] is Galois & f = g*d holds f is closure
proof
let L be non empty Poset, f be Function of L,L such that
A1: f is monotone;
given S being non empty Poset, g being Function of S,L, d being Function of
L,S such that
A2: [g,d] is Galois and
A3: f = g*d;
A4: d is monotone & g is monotone by A2,Th8;
d*g <= id S & id L <= g*d by A2,Th18;
then g = g*d*g by A4,Th20;
hence f is idempotent monotone by A1,A3,Th21;
thus thesis by A2,A3,Th18;
end;
::Theorem 3.10 (1_2) implies (2_2)
theorem Th39:
for L being non empty Poset, f being Function of L,L st f is
kernel holds [corestr f,inclusion f] is Galois
proof
let L be non empty Poset, f be Function of L,L;
assume that
A1: f is idempotent monotone and
A2: f <= id(L);
set g = (corestr f), d = inclusion f;
g*d = id(Image f) by A1,Th33;
then
A3: id(Image f) <= g*d by Lm1;
g is monotone & d*g <= id L by A1,A2,Th31,Th32;
hence thesis by A3,Th19;
end;
::Theorem 3.10 (2_2) implies (3_2)
theorem
for L being non empty Poset, f being Function of L,L st f is kernel ex
T being non empty Poset, g being Function of L,T, d being Function of T,L st [g
,d] is Galois & f = d*g
proof
let L be non empty Poset, f be Function of L,L;
assume
A1: f is kernel;
reconsider T = Image f as non empty Poset;
reconsider g = corestr f as Function of L,T;
reconsider d = inclusion f as Function of T,L;
take T,g,d;
thus [g,d] is Galois by A1,Th39;
thus thesis by Th32;
end;
::Theorem 3.10 (3_2) implies (1_2)
theorem
for L being non empty Poset, f being Function of L,L st f is monotone
& ex T being non empty Poset, g being Function of L,T, d being Function of T,L
st [g,d] is Galois & f = d*g holds f is kernel
proof
let L be non empty Poset, f be Function of L,L;
assume
A1: f is monotone;
given T being non empty Poset, g being Function of L,T, d being Function of
T,L such that
A2: [g,d] is Galois and
A3: f = d*g;
A4: d is monotone & g is monotone by A2,Th8;
d*g <= id L & id T <= g*d by A2,Th18;
then d = d*g*d by A4,Th20;
hence f is idempotent monotone by A1,A3,Th21;
thus thesis by A2,A3,Th18;
end;
:: Lemma 3.11 (i) (part I)
theorem Th42:
for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L such that
A1: p is idempotent and
p is monotone;
set Lk = {k where k is Element of L: p.k <= k};
set Lc = {c where c is Element of L: c <= p.c};
thus rng p c= Lc /\ Lk
proof
let x be object;
assume
A2: x in rng p;
then reconsider x9=x as Element of L;
A3: ex l being object st l in dom p & p.l = x by A2,FUNCT_1:def 3;
then p.x9 <= x9 by A1,YELLOW_2:18;
then
A4: x in Lk;
x9 <= p.x9 by A1,A3,YELLOW_2:18;
then x in Lc;
hence thesis by A4,XBOOLE_0:def 4;
end;
let x be object;
assume
A5: x in Lc /\ Lk;
then x in Lc by XBOOLE_0:def 4;
then
A6: ex lc being Element of L st x = lc & lc <= p.lc;
x in Lk by A5,XBOOLE_0:def 4;
then ex lk being Element of L st x = lk & p.lk <= lk;
then dom p = the carrier of L & x = p.x by A6,FUNCT_2:def 1,ORDERS_2:2;
hence thesis by A6,FUNCT_1:def 3;
end;
theorem Th43:
for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L such that
A1: p is projection;
defpred Q[Element of L] means p.$1 <= $1;
defpred P[Element of L] means $1 <= p.$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,Th42;
Lc is Subset of L from DOMAIN_1:sch 7;
hence Lc is non empty Subset of L by A2;
Lk is Subset of L from DOMAIN_1:sch 7;
hence thesis by A2;
end;
:: Lemma 3.11 (i) (part II)
theorem Th44:
for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L such that
A1: p is projection;
set Lk = {k where k is Element of L: p.k <= k};
set Lc = {c where c is Element of L: c <= p.c};
A2: rng p = Lc /\ Lk by A1,Th42;
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:70;
let y be object;
assume
A4: y in rng p;
then
A5: y in Lc by A2,XBOOLE_0:def 4;
then
A6: ex lc being Element of L st y = lc & lc <= p.lc;
y in Lk by A2,A4,XBOOLE_0:def 4;
then ex lk being Element of L st y = lk & p.lk <= lk;
then y = p.y by A6,ORDERS_2:2;
hence thesis by A3,A5,A6,FUNCT_1:50;
end;
thus rng(p|Lk) c= rng p by RELAT_1:70;
let y be object;
assume
A7: y in rng p;
then y in Lc by A2,XBOOLE_0:def 4;
then
A8: ex lc being Element of L st y = lc & lc <= p.lc;
A9: y in Lk by A2,A7,XBOOLE_0:def 4;
then ex lk being Element of L st y = lk & p.lk <= lk;
then y = p.y by A8,ORDERS_2:2;
hence thesis by A3,A9,A8,FUNCT_1:50;
end;
theorem Th45:
for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of
subrelstr Lc,subrelstr Lc
proof
let L be non empty Poset, p be Function of L,L such that
A1: p is projection;
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,Th42;
then rng(p|Lc) = Lc /\ Lk by A1,A2,Th44;
then
A3: rng(p|Lc) c= Lc by XBOOLE_1:17;
Lc = the carrier of subrelstr Lc & p|Lc is Function of Lc,the carrier of
L by FUNCT_2:32,YELLOW_0:def 15;
hence thesis by A3,FUNCT_2:6;
end;
theorem
for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} holds p|Lk is Function of subrelstr Lk,subrelstr Lk
proof
let L be non empty Poset, p be Function of L,L such that
A1: p is projection;
set Lc = {c where c is Element of L: c <= p.c};
let Lk be non empty Subset of L such that
A2: Lk = {k where k is Element of L: p.k <= k};
rng p = Lc /\ Lk by A1,A2,Th42;
then rng(p|Lk) = Lc /\ Lk by A1,A2,Th44;
then
A3: rng(p|Lk) c= Lk by XBOOLE_1:17;
Lk = the carrier of subrelstr Lk & p|Lk is Function of Lk,the carrier of
L by FUNCT_2:32,YELLOW_0:def 15;
hence thesis by A3,FUNCT_2:6;
end;
:: Lemma 3.11 (i) (part IIIa)
theorem Th47:
for L being non empty Poset, p being Function of L,L st p is
projection for Lc being non empty Subset of L st Lc = {c where c is Element of
L: c <= p.c} for pc being Function of subrelstr Lc,subrelstr Lc st pc = p|Lc
holds pc is closure
proof
let L be non empty Poset, p be Function 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 Function 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: x is Element of L by YELLOW_0:58;
A7: pc.x = p.x by A4,A5,FUNCT_1:47;
then p.(p.x) = pc.(pc.x) by A4,A5,FUNCT_1:47
.= (pc*pc).x by A5,FUNCT_1:13;
hence (pc*pc).x = pc.x by A1,A7,A6,YELLOW_2:18;
end;
hence pc*pc = pc by FUNCT_2:63;
thus pc is monotone
proof
let x1,x2 be Element of subrelstr Lc;
reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
assume x1 <= x2;
then x19 <= x29 by YELLOW_0:59;
then
A8: p.x19 <= p.x29 by A2;
pc.x1 = p.x19 & pc.x2 = p.x29 by A4,A5,FUNCT_1:47;
hence thesis by A8,YELLOW_0:60;
end;
end;
now
let x be Element of subrelstr Lc;
reconsider x9=x as Element of L by YELLOW_0:58;
x in the carrier of subrelstr Lc;
then x in Lc by YELLOW_0:def 15;
then
A9: ex c being Element of L st x = c & c <= p.c by A3;
pc.x = p.x9 by A4,A5,FUNCT_1:47;
then x <= pc.x by A9,YELLOW_0:60;
hence (id subrelstr Lc).x <= pc.x;
end;
hence thesis by YELLOW_2:9;
end;
:: Lemma 3.11 (i) (part IIIb)
theorem
for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} for pk being Function of subrelstr Lk,subrelstr Lk st pk = p|Lk
holds pk is kernel
proof
let L be non empty Poset, p be Function 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 Function 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: x is Element of L by YELLOW_0:58;
A7: pk.x = p.x by A4,A5,FUNCT_1:47;
then p.(p.x) = pk.(pk.x) by A4,A5,FUNCT_1:47
.= (pk*pk).x by A5,FUNCT_1:13;
hence (pk*pk).x = pk.x by A1,A7,A6,YELLOW_2:18;
end;
hence pk*pk = pk by FUNCT_2:63;
thus pk is monotone
proof
let x1,x2 be Element of subrelstr Lk;
reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
assume x1 <= x2;
then x19 <= x29 by YELLOW_0:59;
then
A8: p.x19 <= p.x29 by A2;
pk.x1 = p.x19 & pk.x2 = p.x29 by A4,A5,FUNCT_1:47;
hence thesis by A8,YELLOW_0:60;
end;
end;
now
let x be Element of subrelstr Lk;
reconsider x9=x as Element of L by YELLOW_0:58;
x in the carrier of subrelstr Lk;
then x in Lk by YELLOW_0:def 15;
then
A9: ex c being Element of L st x = c & p.c <= c by A3;
pk.x = p.x9 by A4,A5,FUNCT_1:47;
then pk.x <= x by A9,YELLOW_0:60;
hence pk.x <= (id subrelstr Lk).x;
end;
hence thesis by YELLOW_2:9;
end;
:: Lemma 3.11 (ii) (part I)
theorem Th49:
for L being non empty Poset, p being Function 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 Function 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
A5: ex l being Element of L st x = l & l <= p.l by A2;
("\/"(X,L)) is_>=_than X by A3,YELLOW_0:30;
then x <= "\/"(X,L) by A4;
then p.x <= p.("\/"(X,L)) by A1;
hence x <= p.("\/"(X,L)) by A5,ORDERS_2:3;
end;
then "\/"(X,L) <= p.("\/"(X,L)) by A3,YELLOW_0:30;
then "\/"(X,L) in Lc by A2;
hence thesis by YELLOW_0:def 15;
end;
:: Lemma 3.11 (ii) (part II)
theorem Th50:
for L being non empty Poset, p being Function 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 Function 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
A5: ex l being Element of L st x = l & l >= p.l by A2;
("/\"(X,L)) is_<=_than X by A3,YELLOW_0:31;
then x >= "/\"(X,L) by A4;
then p.x >= p.("/\"(X,L)) by A1;
hence thesis by A5,ORDERS_2:3;
end;
then "/\"(X,L) >= p.("/\"(X,L)) by A3,YELLOW_0:31;
then "/\"(X,L) in Lk by A2;
hence thesis by YELLOW_0:def 15;
end;
:: Lemma 3.11 (iii) (part I)
theorem
for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L;
assume
A1: p is projection;
then reconsider
Lk = {k where k is Element of L: p.k <= k} as non empty Subset of
L by Th43;
let Lc be non empty Subset of L such that
A2: Lc = {c where c is Element of L: c <= p.c};
A3: p is monotone by A1;
then
A4: subrelstr Lk is infs-inheriting by Th50;
A5: Lc = the carrier of subrelstr Lc by YELLOW_0:def 15;
A6: the carrier of Image p = rng p by YELLOW_0:def 15
.= Lc /\ Lk by A1,A2,Th42;
then
A7: the carrier of Image p c= Lk by XBOOLE_1:17;
A8: Lk = the carrier of subrelstr Lk by YELLOW_0:def 15;
A9: the carrier of Image p c= Lc by A6,XBOOLE_1:17;
hereby
assume
A10: p is infs-preserving;
thus
A11: 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 reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume
A12: ex_inf_of X,L;
A13: inf X9 is_<=_than p.:X9
proof
let y be Element of L;
assume y in p.:X9;
then consider x being Element of L such that
A14: x in X9 and
A15: y = p.x by FUNCT_2:65;
reconsider x as Element of L;
x in Lc by A5,A14;
then
A16: ex x9 being Element of L st x9 = x & x9 <= p.x9 by A2;
inf X9 is_<=_than X9 by A12,YELLOW_0:31;
then inf X9 <= x by A14;
hence inf X9 <= y by A15,A16,ORDERS_2:3;
end;
p preserves_inf_of X9 by A10;
then ex_inf_of p.:X,L & inf (p.:X9) = p.(inf X9) by A12;
then inf X9 <= p.(inf X9) by A13,YELLOW_0:31;
hence thesis by A2,A5;
end;
thus Image p is infs-inheriting
proof
let X be Subset of Image p such that
A17: ex_inf_of X,L;
X c= Lc by A9;
then
A18: "/\"(X,L) in the carrier of subrelstr Lc by A5,A11,A17;
subrelstr Lk is infs-inheriting & X c= the carrier of subrelstr Lk
by A3,A7,A8,Th50;
then "/\"(X,L) in the carrier of subrelstr Lk by A17;
hence thesis by A6,A5,A8,A18,XBOOLE_0:def 4;
end;
end;
assume
A19: p is filtered-infs-preserving;
thus
A20: subrelstr Lc is filtered-infs-inheriting
proof
let X be filtered Subset of subrelstr Lc;
assume X <> {};
then reconsider X9 = X as non empty filtered Subset of L by YELLOW_2:7;
assume
A21: ex_inf_of X,L;
A22: inf X9 is_<=_than p.:X9
proof
let y be Element of L;
assume y in p.:X9;
then consider x being Element of L such that
A23: x in X9 and
A24: y = p.x by FUNCT_2:65;
reconsider x as Element of L;
x in Lc by A5,A23;
then
A25: ex x9 being Element of L st x9 = x & x9 <= p.x9 by A2;
inf X9 is_<=_than X9 by A21,YELLOW_0:31;
then inf X9 <= x by A23;
hence inf X9 <= y by A24,A25,ORDERS_2:3;
end;
p preserves_inf_of X9 by A19;
then ex_inf_of p.:X,L & inf (p.:X9) = p.(inf X9) by A21;
then inf X9 <= p.(inf X9) by A22,YELLOW_0:31;
hence thesis by A2,A5;
end;
let X be filtered Subset of Image p such that
A26: X <> {} and
A27: ex_inf_of X,L;
the carrier of Image p c= the carrier of subrelstr Lc by A9,YELLOW_0:def 15;
then X is filtered Subset of subrelstr Lc by YELLOW_2:8;
then
A28: "/\"(X,L) in the carrier of subrelstr Lc by A20,A26,A27;
X c= the carrier of subrelstr Lk by A7,A8;
then "/\"(X,L) in the carrier of subrelstr Lk by A27,A4;
hence thesis by A6,A5,A8,A28,XBOOLE_0:def 4;
end;
:: Lemma 3.11 (iii) (part II)
theorem
for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of L,L;
assume
A1: p is projection;
then reconsider
Lc = {c where c is Element of L: c <= p.c} as non empty Subset of
L by Th43;
let Lk be non empty Subset of L such that
A2: Lk = {k where k is Element of L: p.k <= k};
A3: p is monotone by A1;
then
A4: subrelstr Lc is sups-inheriting by Th49;
A5: Lc = the carrier of subrelstr Lc by YELLOW_0:def 15;
A6: the carrier of Image p = rng p by YELLOW_0:def 15
.= Lc /\ Lk by A1,A2,Th42;
then
A7: the carrier of Image p c= Lk by XBOOLE_1:17;
A8: Lk = the carrier of subrelstr Lk by YELLOW_0:def 15;
A9: the carrier of Image p c= Lc by A6,XBOOLE_1:17;
hereby
assume
A10: p is sups-preserving;
thus
A11: 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 reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume
A12: ex_sup_of X,L;
A13: sup X9 is_>=_than p.:X9
proof
let y be Element of L;
assume y in p.:X9;
then consider x being Element of L such that
A14: x in X9 and
A15: y = p.x by FUNCT_2:65;
reconsider x as Element of L;
x in Lk by A8,A14;
then
A16: ex x9 being Element of L st x9 = x & x9 >= p.x9 by A2;
sup X9 is_>=_than X9 by A12,YELLOW_0:30;
then sup X9 >= x by A14;
hence thesis by A15,A16,ORDERS_2:3;
end;
p preserves_sup_of X9 by A10;
then ex_sup_of p.:X,L & sup (p.:X9) = p.(sup X9) by A12;
then sup X9 >= p.(sup X9) by A13,YELLOW_0:30;
hence thesis by A2,A8;
end;
thus Image p is sups-inheriting
proof
let X be Subset of Image p such that
A17: ex_sup_of X,L;
X c= Lk by A7;
then
A18: "\/"(X,L) in the carrier of subrelstr Lk by A8,A11,A17;
subrelstr Lc is sups-inheriting & X c= the carrier of subrelstr Lc
by A3,A9,A5,Th49;
then "\/"(X,L) in the carrier of subrelstr Lc by A17;
hence thesis by A6,A5,A8,A18,XBOOLE_0:def 4;
end;
end;
assume
A19: p is directed-sups-preserving;
thus
A20: subrelstr Lk is directed-sups-inheriting
proof
let X be directed Subset of subrelstr Lk;
assume X <> {};
then reconsider X9 = X as non empty directed Subset of L by YELLOW_2:7;
assume
A21: ex_sup_of X,L;
A22: sup X9 is_>=_than p.:X9
proof
let y be Element of L;
assume y in p.:X9;
then consider x being Element of L such that
A23: x in X9 and
A24: y = p.x by FUNCT_2:65;
reconsider x as Element of L;
x in Lk by A8,A23;
then
A25: ex x9 being Element of L st x9 = x & x9 >= p.x9 by A2;
sup X9 is_>=_than X9 by A21,YELLOW_0:30;
then sup X9 >= x by A23;
hence thesis by A24,A25,ORDERS_2:3;
end;
p preserves_sup_of X9 by A19;
then ex_sup_of p.:X,L & sup (p.:X9) = p.(sup X9) by A21;
then sup X9 >= p.(sup X9) by A22,YELLOW_0:30;
hence thesis by A2,A8;
end;
let X be directed Subset of Image p such that
A26: X <> {} and
A27: ex_sup_of X,L;
the carrier of Image p c= the carrier of subrelstr Lk by A7,YELLOW_0:def 15;
then X is directed Subset of subrelstr Lk by YELLOW_2:8;
then
A28: "\/"(X,L) in the carrier of subrelstr Lk by A20,A26,A27;
X c= the carrier of subrelstr Lc by A9,A5;
then "\/"(X,L) in the carrier of subrelstr Lc by A27,A4;
hence thesis by A6,A5,A8,A28,XBOOLE_0:def 4;
end;
:: Proposition 3.12 (i)
theorem Th53:
for L being non empty Poset, p being Function of L,L holds (p is
closure implies Image p is infs-inheriting) & (p is kernel implies Image p is
sups-inheriting)
proof
let L be non empty Poset, p be Function of L,L;
hereby
assume
A1: p is closure;
thus Image p is infs-inheriting
proof
let X be Subset of Image p;
A2: the carrier of Image p = rng p by YELLOW_0:def 15;
then reconsider X9=X as Subset of L by XBOOLE_1:1;
assume ex_inf_of X,L;
then p.("/\"(X9,L)) = "/\"(X9,L) by A1,A2,Th28;
hence thesis by A2,FUNCT_2:4;
end;
end;
assume
A3: p is kernel;
let X be Subset of Image p;
A4: the carrier of Image p = rng p by YELLOW_0:def 15;
then reconsider X9=X as Subset of L by XBOOLE_1:1;
assume ex_sup_of X,L;
then p.("\/"(X9,L)) = "\/"(X9,L) by A3,A4,Th29;
hence thesis by A4,FUNCT_2:4;
end;
:: Proposition 3.12 (ii)
theorem
for L being complete non empty Poset, p being Function of L,L st p
is projection holds Image p is complete
proof
let L be complete non empty Poset, p be Function of L,L;
A1: the carrier of Image p = rng p by YELLOW_0:def 15;
assume
A2: p is projection;
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 Th43;
A3: the carrier of subrelstr Lc = Lc & rng p = Lc /\ Lk by A2,Th42,
YELLOW_0:def 15;
p is monotone by A2;
then subrelstr Lc is sups-inheriting by Th49;
then
A4: subrelstr Lc is complete LATTICE by YELLOW_2:31;
reconsider pc = p|Lc as Function of subrelstr Lc,subrelstr Lc by A2,Th45;
A5: Image pc is infs-inheriting by A2,Th47,Th53;
A6: the carrier of Image pc = rng(pc) by YELLOW_0:def 15
.= the carrier of Image p by A2,A1,Th44;
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 A1,A3,WELLORD1:22
,XBOOLE_1:17
.= the InternalRel of Image p by YELLOW_0:def 14;
hence thesis by A4,A5,A6,YELLOW_2:30;
end;
:: Proposition 3.12 (iii)
theorem
for L being non empty Poset, c being Function of L,L st c is closure
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 Function of L,L;
A1: (corestr c) = c by Th30;
assume
A2: c is closure;
then
A3: c is idempotent by Def13;
[inclusion c,corestr c] is Galois by A2,Th36;
then
A4: corestr c is lower_adjoint;
hence corestr c is sups-preserving;
let X be Subset of L such that
A5: X c= the carrier of Image c and
A6: ex_sup_of X,L;
X c= rng c by A5,YELLOW_0:def 15;
then
A7: c.:X = X by A3,YELLOW_2:20;
corestr c preserves_sup_of X by A4,WAYBEL_0:def 33;
hence thesis by A6,A1,A7;
end;
:: Proposition 3.12 (iv)
theorem
for L being non empty Poset, k being Function of L,L st k is kernel
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 Function of L,L;
A1: (corestr k) = k by Th30;
assume
A2: k is kernel;
then
A3: k is idempotent by Def13;
[corestr k,inclusion k] is Galois by A2,Th39;
then
A4: corestr k is upper_adjoint;
hence (corestr k) is infs-preserving;
let X be Subset of L such that
A5: X c= the carrier of Image k and
A6: ex_inf_of X,L;
X c= rng k by A5,YELLOW_0:def 15;
then
A7: k.:X = X by A3,YELLOW_2:20;
corestr k preserves_inf_of X by A4,WAYBEL_0:def 32;
hence thesis by A6,A1,A7;
end;
begin :: Heyting algebras
:: Proposition 3.15 (i)
theorem Th57:
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 I9 = I as Ideal of L by YELLOW_2:41;
hereby
assume I <= g.x;
then I c= g.x by YELLOW_1:3;
then I9 c= downarrow x by YELLOW_2:def 4;
then x is_>=_than I9 by YELLOW_2:1;
then sup I9 <= x by YELLOW_0:32;
hence d.I <= x by YELLOW_2:def 3;
end;
assume d.I <= x;
then
A1: sup I9 <= x by YELLOW_2:def 3;
sup I9 is_>=_than I9 by YELLOW_0:32;
then x is_>=_than I9 by A1,YELLOW_0:4;
then I9 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;
then SupMap L is lower_adjoint;
hence thesis;
end;
:: Proposition 3.15 (ii)
theorem
for L being complete non empty Poset holds (IdsMap L)*(SupMap L) is
closure & Image ((IdsMap L)*(SupMap L)),L are_isomorphic
proof
let L be complete non empty Poset;
set i = (IdsMap L)*(SupMap L);
A1: now
let I be Ideal of L;
I is Element of InclPoset(Ids L) by YELLOW_2:41;
hence i.I = (IdsMap L).((SupMap L).I) by FUNCT_2:15
.= (IdsMap L).(sup I) by YELLOW_2:def 3
.= downarrow (sup I) by YELLOW_2:def 4;
end;
i is monotone & [IdsMap L,SupMap L] is Galois by Th57,YELLOW_2:12;
hence i is closure by Th38;
take f = (SupMap L)*(inclusion i);
A2: now
let x be Element of Image i;
let I be Ideal of L;
assume
A3: x = I;
hence f.I = (SupMap L).((inclusion i).I) by FUNCT_2:15
.= (SupMap L).I by A3
.= sup I by YELLOW_2:def 3;
end;
A4: f is monotone by YELLOW_2:12;
A5: now
let x,y be Element of Image i;
consider Ix being Element of InclPoset(Ids L) such that
A6: i.Ix = x by YELLOW_2:10;
thus x <= y implies f.x <= f.y by A4;
assume
A7: f.x <= f.y;
x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L)
by YELLOW_0:58;
then reconsider x9=x, y9=y as Ideal of L by YELLOW_2:41;
consider Iy being Element of InclPoset(Ids L) such that
A8: i.Iy = y by YELLOW_2:10;
reconsider Ix,Iy as Ideal of L by YELLOW_2:41;
reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy) as Element of
InclPoset(Ids L) by YELLOW_2:41;
A9: i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A1;
A10: f.x9 = sup x9 & f.y9 = sup y9 by A2;
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 A7,A6,A8,A9,A10,
WAYBEL_0:21;
then i1 <= i2 by YELLOW_1:3;
hence x <= y by A6,A8,A9,YELLOW_0:60;
end;
A11: rng f = the carrier of L
proof
thus rng f c= the carrier of L;
let x be object;
assume x in the carrier of L;
then reconsider x as Element of L;
A12: (SupMap L).(downarrow x) = sup downarrow x by YELLOW_2:def 3
.= x by WAYBEL_0:34;
A13: downarrow x is Element of InclPoset(Ids L) by YELLOW_2:41;
then i.(downarrow x) = (IdsMap L).((SupMap L).(downarrow x)) by FUNCT_2:15
.= downarrow x by A12,YELLOW_2:def 4;
then downarrow x in rng i by A13,FUNCT_2:4;
then
A14: downarrow x in the carrier of Image i by YELLOW_0:def 15;
then f.(downarrow x) = (SupMap L).((inclusion i).(downarrow x)) by
FUNCT_2:15
.= (SupMap L).(downarrow x) by A14,FUNCT_1:18;
hence thesis by A12,A14,FUNCT_2:4;
end;
f is one-to-one
proof
let x,y be Element of Image i;
assume
A15: f.x = f.y;
consider Ix being Element of InclPoset(Ids L) such that
A16: i.Ix = x by YELLOW_2:10;
consider Iy being Element of InclPoset(Ids L) such that
A17: i.Iy = y by YELLOW_2:10;
x is Element of InclPoset(Ids L) & y is Element of InclPoset(Ids L)
by YELLOW_0:58;
then reconsider x,y as Ideal of L by YELLOW_2:41;
reconsider Ix,Iy as Ideal of L by YELLOW_2:41;
A18: sup downarrow (sup Ix) = sup Ix by WAYBEL_0:34;
A19: i.Ix = downarrow (sup Ix) & i.Iy = downarrow (sup Iy) by A1;
f.x = sup x & f.y = sup y by A2;
hence thesis by A15,A16,A17,A19,A18,WAYBEL_0:34;
end;
hence thesis by A11,A5,WAYBEL_0:66;
end;
definition
let S be non empty RelStr;
let x be Element of S;
func x "/\" -> Function 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 Function of S,S st for x being Element of S holds f.x = F(
x) from FUNCT_2:sch 4;
end;
uniqueness
proof
let f1,f2 be Function 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 FUNCT_2:63;
end;
end;
theorem Th59:
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 object;
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:38;
end;
let s be object;
assume
A3: s in (x "/\")"(downarrow t);
then reconsider s as Element of S;
(x "/\").s in downarrow t by A3,FUNCT_2:38;
then x"/\"s in downarrow t by Def18;
then x"/\"s <= t by WAYBEL_0:17;
hence thesis;
end;
theorem Th60:
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,s1},S by YELLOW_0:21;
then
A3: x"/\"s1 <= x by YELLOW_0:19;
x"/\"s1 <= s1 by A2,YELLOW_0:19;
then ex_inf_of {x,s2},S & x"/\"s1 <= s2 by A1,ORDERS_2:3,YELLOW_0:21;
then x"/\"s1 <= x"/\"s2 by A3,YELLOW_0:19;
then (x "/\").s1 <= x"/\"s2 by Def18;
hence (x "/\").s1 <= (x "/\").s2 by Def18;
end;
registration
let S be Semilattice, x be Element of S;
cluster x "/\" -> monotone;
coherence by Th60;
end;
theorem Th61:
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 object;
assume y in (x "/\").:X;
then consider z being object such that
A1: z in the carrier of S and
A2: z in X and
A3: y = (x "/\").z by FUNCT_2:64;
reconsider z as Element of S by A1;
y = x "/\" z by A3,Def18;
hence y in Y by A2;
end;
let y be object;
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 thesis by A5,FUNCT_2:35;
end;
:: Lemma 3.16 (1) iff (2)
theorem Th62:
for S being Semilattice holds (for x being Element of S holds x
"/\" is lower_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 "/\" is lower_adjoint;
let x,t be Element of S;
(x "/\") is lower_adjoint by A1;
then consider g being Function of S,S such that
A2: [g, x "/\"] is Galois;
set X = {s where s is Element of S: x"/\"s <= t};
A3: X = (x "/\")"(downarrow t) by Th59;
g.t is_maximum_of (x "/\")"(downarrow t) by A2,Th11;
then ex_sup_of X,S & "\/"(X,S)in X by A3;
hence ex_max_of X,S;
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 Function of S,S such that
A5: for s being Element of S holds g.s = F(s) from FUNCT_2:sch 4;
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;
X = (x "/\")"(downarrow t) & g.t = "\/"((x "/\")"(downarrow t),S) by A5
,Th59;
hence g.t is_maximum_of (x "/\")"(downarrow t) by A6;
end;
then [g, x "/\"] is Galois by Th11;
hence thesis;
end;
:: Lemma 3.16 (1) implies (3)
theorem Th63:
for S being Semilattice st for x being Element of S holds x "/\"
is lower_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 "/\" is lower_adjoint;
let X be Subset of S such that
A2: ex_sup_of X,S;
let x be Element of S;
x "/\" is sups-preserving by A1,Th13;
then x "/\" preserves_sup_of X;
then sup ((x "/\").:X) = (x "/\").(sup X) by A2;
hence x "/\" "\/"(X,S) = sup ((x "/\").:X) by Def18
.= "\/"({x"/\" y where y is Element of S: y in X},S) by Th61;
end;
:: Lemma 3.16 (1) iff (3)
theorem
for S being complete non empty Poset holds (for x being Element of S
holds x "/\" is lower_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;
thus (for x being Element of S holds x "/\" is lower_adjoint) implies 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) by Th63,YELLOW_0:17;
assume
A1: 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 A1
.= sup ((x "/\").:X) by Th61;
end;
hence thesis by Th17;
end;
:: Lemma 3.16 (3) implies (D)
theorem Th65:
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}};
A2: ex_sup_of {y,z},S by YELLOW_0:20;
now
let t be object;
hereby
assume t in Y;
then ex s being Element of S st t = x"/\"s & s in {y,z};
hence t = x"/\"y or t = x"/\"z by TARSKI:def 2;
end;
assume
A3: t = x"/\"y or t = x"/\"z;
per cases by A3;
suppose
A4: t = x"/\"y;
y in {y,z} by TARSKI:def 2;
hence t in Y by A4;
end;
suppose
A5: t = x"/\"z;
z in {y,z} by TARSKI:def 2;
hence t in Y by A5;
end;
end;
then
A6: Y = {x"/\"y,x"/\"z} by TARSKI:def 2;
thus x "/\" (y "\/" z) = x "/\" (sup {y,z}) by YELLOW_0:41
.= "\/"({x"/\"y,x"/\"z},S) by A1,A6,A2
.= (x "/\" y) "\/" (x "/\" z) by YELLOW_0:41;
end;
definition
let H be non empty RelStr;
attr H is Heyting means
H is LATTICE & for x being Element of H holds x "/\" is lower_adjoint;
end;
registration
cluster Heyting -> with_infima with_suprema reflexive transitive
antisymmetric for non empty RelStr;
coherence;
end;
definition
let H be non empty RelStr, a be Element of H;
assume
A1: H is Heyting;
func a => -> Function of H,H means
:Def20:
[it,a "/\"] is Galois;
existence
by A1,Def12;
uniqueness
proof
let g1,g2 be Function of H,H such that
A2: [g1,a "/\"] is Galois and
A3: [g2,a "/\"] is Galois;
now
let x be Element of H;
g1.x is_maximum_of (a "/\")"(downarrow x) by A1,A2,Th11;
then
A4: g1.x = "\/"((a "/\")"(downarrow x),H);
g2.x is_maximum_of (a "/\")"(downarrow x) by A1,A3,Th11;
hence g1.x = g2.x by A4;
end;
hence g1 = g2 by FUNCT_2:63;
end;
end;
theorem Th66:
for H being non empty RelStr st H is Heyting holds H is distributive
proof
let H be non empty RelStr;
assume that
A1: H is LATTICE and
A2: for x being Element of H holds x "/\" is lower_adjoint;
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 A1,A2
,Th63;
hence thesis by A1,Th65;
end;
registration
cluster Heyting -> distributive for non empty RelStr;
coherence by Th66;
end;
definition
let H be non empty RelStr, a,y be Element of H;
func a => y -> Element of H equals
(a=>).y;
correctness;
end;
theorem Th67:
for H being non empty RelStr st H is Heyting 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 Heyting;
let x,a,y be Element of H;
[a =>, a "/\"] is Galois by A1,Def20;
then x >= (a "/\").y iff (a =>).x >= y by A1,Th8;
hence thesis by Def18;
end;
theorem Th68:
for H being non empty RelStr st H is Heyting holds H is upper-bounded
proof
let H be non empty RelStr;
assume
A1: H is Heyting;
set a = the Element of H;
take a => a;
let y be Element of H;
assume y in the carrier of H;
a >= a "/\" y by A1,YELLOW_0:23;
hence thesis by A1,Th67;
end;
registration
cluster Heyting -> upper-bounded for non empty RelStr;
coherence by Th68;
end;
theorem Th69:
for H being non empty RelStr st H is Heyting 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 Heyting;
let a,b be Element of H;
A2: a "/\" Top H = Top H "/\" a by A1,LATTICE3:15
.= a by A1,Th4;
hereby
assume Top H = a => b;
then a => b >= Top H by A1,ORDERS_2:1;
hence a <= b by A1,A2,Th67;
end;
assume a <= b;
then
A3: a => b >= Top H by A1,A2,Th67;
a => b <= Top H by A1,YELLOW_0:45;
hence thesis by A1,A3,ORDERS_2:2;
end;
theorem
for H being non empty RelStr st H is Heyting for a being Element of H
holds Top H = a => a
proof
let H be non empty RelStr;
assume
A1: H is Heyting;
let a be Element of H;
a >= a "/\" Top H by A1,YELLOW_0:23;
then
A2: Top H <= a => a by A1,Th67;
Top H >= a => a by A1,YELLOW_0:45;
hence thesis by A1,A2,ORDERS_2:2;
end;
theorem
for H being non empty RelStr st H is Heyting 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 Heyting;
let a,b be Element of H;
assume
A2: Top H = a => b;
assume Top H = b => a;
then
A3: b <= a by A1,Th69;
a <= b by A1,A2,Th69;
hence thesis by A1,A3,ORDERS_2:2;
end;
theorem Th72:
for H being non empty RelStr st H is Heyting for a,b being
Element of H holds b <= (a => b)
proof
let H be non empty RelStr;
assume
A1: H is Heyting;
let a,b be Element of H;
a"/\"b <= b by A1,YELLOW_0:23;
hence thesis by A1,Th67;
end;
theorem
for H being non empty RelStr st H is Heyting for a being Element of H
holds Top H = a => Top H
proof
let H be non empty RelStr;
assume
A1: H is Heyting;
let a be Element of H;
a <= Top H by A1,YELLOW_0:45;
hence thesis by A1,Th69;
end;
theorem
for H being non empty RelStr st H is Heyting for b being Element of H
holds b = (Top H) => b
proof
let H be non empty RelStr;
assume
A1: H is Heyting;
let b be Element of H;
(Top H) => b <= (Top H) => b by A1,ORDERS_2:1;
then Top H "/\" ((Top H) => b) <= b by A1,Th67;
then
A2: (Top H) => b <= b by A1,Th4;
(Top H) => b >= b by A1,Th72;
hence thesis by A1,A2,ORDERS_2:2;
end;
Lm5: for H being non empty RelStr st H is Heyting for a,b being Element of H
holds a"/\"(a => b) <= b
proof
let H be non empty RelStr;
assume
A1: H is Heyting;
let a,b be Element of H;
(a => b) <= (a => b) by A1,ORDERS_2:1;
hence thesis by A1,Th67;
end;
theorem Th75:
for H being non empty RelStr st H is Heyting 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 Heyting;
let a,b,c be Element of H;
assume a <= b;
then
A2: a"/\"(b => c) <= b"/\"(b => c) by A1,Th1;
b"/\"(b => c) <= c by A1,Lm5;
then a"/\"(b => c) <= c by A1,A2,ORDERS_2:3;
hence thesis by A1,Th67;
end;
theorem
for H being non empty RelStr st H is Heyting 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 Heyting;
let a,b,c be Element of H;
assume
A2: b <= c;
a"/\"(a => b) <= b by A1,Lm5;
then a"/\"(a => b) <= c by A1,A2,ORDERS_2:3;
hence thesis by A1,Th67;
end;
theorem Th77:
for H being non empty RelStr st H is Heyting for a,b being
Element of H holds a"/\"(a => b) = a"/\"b
proof
let H be non empty RelStr;
assume
A1: H is Heyting;
let a,b be Element of H;
(a"/\"(a => b))"/\"a <= b"/\"a by A1,Lm5,Th1;
then a"/\"(a"/\"(a => b)) <= b"/\"a by A1,LATTICE3:15;
then a"/\"(a"/\"(a => b)) <= a"/\"b by A1,LATTICE3:15;
then (a"/\"a)"/\"(a => b) <= a"/\"b by A1,LATTICE3:16;
then
A2: a"/\"(a => b) <= a"/\"b by A1,YELLOW_0:25;
b"/\"a <= (a => b)"/\"a by A1,Th1,Th72;
then a"/\"b <= (a => b)"/\"a by A1,LATTICE3:15;
then a"/\"b <= a"/\"(a => b) by A1,LATTICE3:15;
hence thesis by A1,A2,ORDERS_2:2;
end;
theorem Th78:
for H being non empty RelStr st H is Heyting 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 Heyting;
let a,b,c be Element of H;
((a"/\"c)"/\"(b=>c)) <= a"/\"c & a"/\"c <= c by A1,YELLOW_0:23;
then
A2: ((a"/\"c)"/\"(b=>c)) <= c by A1,ORDERS_2:3;
((b"/\"c)"/\"(a=>c)) <= b"/\"c & b"/\"c <= c by A1,YELLOW_0:23;
then
A3: ((b"/\"c)"/\"(a=>c)) <= c by A1,ORDERS_2:3;
set d = (a => c) "/\" (b => c);
(a"\/"b)"/\"d = d"/\"(a"\/"b) by A1,LATTICE3:15
.= (d"/\"a)"\/"(d"/\"b) by A1,Def3
.= (a"/\"d)"\/"(d"/\"b) by A1,LATTICE3:15
.= (a"/\"d)"\/"(b"/\"d) by A1,LATTICE3:15
.= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"d) by A1,LATTICE3:16
.= ((a"/\"(a=>c))"/\"(b=>c))"\/"(b"/\"((b=>c)"/\"(a=>c))) by A1,LATTICE3:15
.= ((a"/\"(a=>c))"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A1,LATTICE3:16
.= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"(b=>c))"/\"(a=>c)) by A1,Th77
.= ((a"/\"c)"/\"(b=>c))"\/"((b"/\"c)"/\"(a=>c)) by A1,Th77;
then (a"\/"b)"/\"d <= c by A1,A2,A3,YELLOW_0:22;
then
A4: (a"\/"b)=> c >= d by A1,Th67;
b <= a"\/"b by A1,YELLOW_0:22;
then
A5: (a"\/"b)=> c <= (b => c) by A1,Th75;
a <= a"\/"b by A1,YELLOW_0:22;
then (a"\/"b)=> c <= (a => c) by A1,Th75;
then (a"\/"b)=> c <= (a => c) "/\" (b => c) by A1,A5,YELLOW_0:23;
hence thesis by A1,A4,ORDERS_2:2;
end;
definition
let H be non empty RelStr, a be Element of H;
func 'not' a -> Element of H equals
a => Bottom H;
correctness;
end;
theorem
for H being non empty RelStr st H is Heyting & 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 Heyting and
A2: H is lower-bounded;
let a be Element of H;
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};
A3: X = Y
proof
hereby
let y be object;
assume y in X;
then consider x being Element of H such that
A4: y = x and
A5: a"/\"x = Bottom H;
a"/\"x <= Bottom H by A1,A5,ORDERS_2:1;
hence y in Y by A4;
end;
let y be object;
assume y in Y;
then consider x being Element of H such that
A6: y = x and
A7: a"/\"x <= Bottom H;
Bottom H <= a"/\"x by A1,A2,YELLOW_0:44;
then Bottom H = a"/\"x by A1,A7,ORDERS_2:2;
hence thesis by A6;
end;
A8: now
a => (Bottom H) <= a => (Bottom H) by A1,ORDERS_2:1;
then a"/\"'not' a <= Bottom H by A1,Th67;
then
A9: 'not' a in X by A3;
let b be Element of H;
assume b is_>=_than X;
hence 'not' a <= b by A9;
end;
A10: ex_max_of X,H by A1,A3,Th62;
hence ex_sup_of X,H;
'not' a is_>=_than X
proof
let b be Element of H;
assume b in X;
then ex x being Element of H st x = b & a"/\"x <= Bottom H by A3;
hence thesis by A1,Th67;
end;
hence 'not' a = "\/"(X,H) by A1,A8,YELLOW_0:30;
thus thesis by A10;
end;
theorem Th80:
for H being non empty RelStr st H is Heyting & 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 Heyting and
A2: H is lower-bounded;
(Top H) => (Bottom H) <= (Top H) => (Bottom H) by A1,ORDERS_2:1;
then
A3: Bottom H >= Top H "/\" 'not' Top H by A1,Th67;
Bottom H >= Bottom H "/\" Top H by A1,YELLOW_0:23;
then
A4: Top H <= (Bottom H) => (Bottom H) by A1,Th67;
Bottom H <= Top H "/\" 'not' Top H by A1,A2,YELLOW_0:44;
then
A5: Bottom H = Top H "/\" 'not' Top H by A1,A3,ORDERS_2:2;
'not' Bottom H <= Top H by A1,YELLOW_0:45;
hence Top H = 'not' Bottom H by A1,A4,ORDERS_2:2;
'not' Top H <= Top H by A1,YELLOW_0:45;
hence 'not' Top H = 'not' Top H"/\"Top H by A1,YELLOW_0:25
.= Bottom H by A1,A5,LATTICE3:15;
end;
:: Exercise 3.18 (i)
theorem
for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
let a,b be Element of H;
A2: Bottom H >= a "/\" b iff a => Bottom H >= b by A1,Th67;
Bottom H >= b "/\" a iff b => Bottom H >= a by A1,Th67;
hence thesis by A1,A2,LATTICE3:15;
end;
:: Exercise 3.18 (ii)
theorem Th82:
for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
let a,b be Element of H;
hereby
assume 'not' a >= b;
then
A2: a "/\" b <= Bottom H by A1,Th67;
a "/\" b >= Bottom H by A1,YELLOW_0:44;
hence a "/\" b = Bottom H by A1,A2,ORDERS_2:2;
end;
assume a "/\" b = Bottom H;
then a "/\" b <= Bottom H by A1,ORDERS_2:1;
hence thesis by A1,Th67;
end;
theorem
for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
let a,b be Element of H;
A2: 'not' b >= 'not' b by A1,ORDERS_2:1;
assume a <= b;
then a "/\" 'not' b = (a"/\"b)"/\"'not' b by A1,YELLOW_0:25
.= a"/\"(b"/\"'not' b) by A1,LATTICE3:16
.= a"/\"Bottom H by A1,A2,Th82
.= Bottom H"/\"a by A1,LATTICE3:15
.= Bottom H by A1,Th3;
hence thesis by A1,Th82;
end;
theorem
for H being non empty lower-bounded RelStr st H is Heyting for a,b
being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b by Th78;
theorem
for H being non empty lower-bounded RelStr st H is Heyting 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 Heyting;
then
A2: Bottom H<=Bottom H by ORDERS_2:1;
let a,b be Element of H;
A3: 'not' a <= 'not' a by A1,ORDERS_2:1;
A4: 'not' b <= 'not' b by A1,ORDERS_2:1;
(a"/\"b)"/\"('not' a"\/"'not' b) = ((a"/\"b)"/\"'not' a)"\/"((a"/\"b)
"/\" 'not' b) by A1,Def3
.= ((b"/\"a)"/\"'not' a)"\/"((a"/\"b)"/\" 'not' b) by A1,LATTICE3:15
.= (b"/\"(a"/\"'not' a))"\/"((a"/\"b)"/\" 'not' b) by A1,LATTICE3:16
.= (b"/\"(a"/\"'not' a))"\/"(a"/\"(b"/\" 'not' b)) by A1,LATTICE3:16
.= (b"/\"Bottom H)"\/"(a"/\"(b"/\"'not' b)) by A1,A3,Th82
.= (b"/\"Bottom H)"\/"(a"/\"Bottom H) by A1,A4,Th82
.= (Bottom H"/\"b)"\/"(a"/\"Bottom H) by A1,LATTICE3:15
.= (Bottom H"/\"b)"\/"(Bottom H"/\"a) by A1,LATTICE3:15
.= Bottom H"\/"(Bottom H"/\"a) by A1,Th3
.= Bottom H"\/"Bottom H by A1,Th3
.= Bottom H by A1,A2,YELLOW_0:24;
hence thesis by A1,Th82;
end;
definition
let L be non empty RelStr, x,y be Element of L;
pred y is_a_complement_of x means
x "\/" y = Top L & x "/\" y = Bottom L;
end;
definition
let L be non empty RelStr;
attr L is complemented means
for x being Element of L ex y being Element of L st y is_a_complement_of x;
end;
registration
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
.= bool X by LATTICE3:def 1;
then reconsider y = X\x as Element of BoolePoset X by XBOOLE_1:109;
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
.= Bottom (BoolePoset X) by YELLOW_1:18;
end;
end;
:: Exercise 3.19 (1) implies (3)
Lm6: for L being bounded LATTICE st L is distributive complemented for x being
Element of L ex x9 being Element of L st for y being Element of L holds (y "\/"
x9) "/\" x <= y & y <= (y "/\" x) "\/" x9
proof
let L be bounded LATTICE such that
A1: L is distributive and
A2: L is complemented;
let x be Element of L;
consider x9 being Element of L such that
A3: x9 is_a_complement_of x by A2;
take x9;
let y be Element of L;
(y "\/" x9) "/\" x = (x "/\" y) "\/" (x "/\" x9) by A1
.= Bottom L "\/" (x "/\" y) by A3
.= x "/\" y by Th3;
hence (y "\/" x9) "/\" x <= y by YELLOW_0:23;
(y "/\" x) "\/" x9 = (x9 "\/" y) "/\" (x9 "\/" x) by A1,Th5
.= (x9 "\/" y) "/\" Top L by A3
.= x9 "\/" y by Th4;
hence thesis by YELLOW_0:22;
end;
:: Exercise 3.19 (3) implies (2)
Lm7: for L being bounded LATTICE st for x being Element of L ex x9 being
Element of L st for y being Element of L holds (y "\/" x9) "/\" x <= y & y <= (
y "/\" x) "\/" x9 holds L is Heyting & 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 x9 being Element of L st P[x,x9];
consider g9 being Function of L,L such that
A2: for x being Element of L holds P[x,g9.x] from FUNCT_2:sch 3(A1);
A3: now
let y be Element of L;
let g be Function of L,L such that
A4: for z being Element of L holds g.z = g9.y "\/" z;
A5: now
let x be Element of L, z be Element of L;
hereby
assume x <= g.z;
then x <= g9.y "\/" z by A4;
then
A6: x "/\" y <= (g9.y "\/" z) "/\" y by Th1;
(g9.y "\/" z) "/\" y <= z by A2;
then x "/\" y <= z by A6,ORDERS_2:3;
hence (y "/\").x <= z by Def18;
end;
assume (y "/\").x <= z;
then y "/\" x <= z by Def18;
then
A7: (x "/\" y) "\/" g9.y <= z "\/" g9.y by Th2;
x <= (x "/\" y) "\/" g9.y by A2;
then x <= z "\/" g9.y by A7,ORDERS_2:3;
hence x <= g.z by A4;
end;
g is monotone
proof
let z1,z2 be Element of L;
assume z1 <= z2;
then g9.y "\/" z1 <= z2 "\/" g9.y by Th2;
then g.z1 <= g9.y "\/" z2 by A4;
hence thesis by A4;
end;
hence [g,y "/\"] is Galois by A5;
end;
thus
A8: L is Heyting
proof
thus L is LATTICE;
let y be Element of L;
deffunc F(Element of L) = g9.y "\/" $1;
consider g being Function of L,L such that
A9: for z being Element of L holds g.z = F(z) from FUNCT_2:sch 4;
[g,y "/\"] is Galois by A3,A9;
hence thesis;
end;
A10: now
let x be Element of L;
deffunc F(Element of L) = g9.x "\/" $1;
consider g being Function of L,L such that
A11: for z being Element of L holds g.z = F(z) from FUNCT_2:sch 4;
[g,x "/\"] is Galois by A3,A11;
then g = x => by A8,Def20;
hence 'not' x = Bottom L "\/" g9.x by A11
.= g9.x by Th3;
end;
A12: now
let x be Element of L;
(Bottom L "\/" g9.x) "/\" x <= Bottom L by A2;
then (x "/\" Bottom L) "\/" (x "/\" g9.x) <= Bottom L by A8,Def3;
then Bottom L "\/" (x "/\" g9.x) <= Bottom L by Th3;
then
A13: x "/\" g9.x <= Bottom L by Th3;
Bottom L <= x "/\" g9.x by YELLOW_0:44;
hence Bottom L = x "/\" g9.x by A13,ORDERS_2:2
.= x "/\" 'not' x by A10;
end;
let x be Element of L;
A14: now
let x be Element of L;
Top L <= (Top L "/\" x) "\/" g9.x by A2;
then
A15: Top L <= x "\/" g9.x by Th4;
x "\/" g9.x <= Top L by YELLOW_0:45;
hence Top L = x "\/" g9.x by A15,ORDERS_2:2
.= x "\/" 'not' x by A10;
end;
then ('not' x "\/" 'not' 'not' x) "/\" x = Top L "/\" x;
then x = x "/\" ('not' x "\/" 'not' 'not' x) by Th4
.= (x "/\" 'not' x) "\/" (x "/\" 'not' 'not' x) by A8,Def3
.= Bottom L "\/" (x "/\" 'not' 'not' x) by A12
.= x "/\" 'not' 'not' x by Th3;
then
A16: x <= 'not' 'not' x by YELLOW_0:25;
Bottom L "\/" x = ('not' x "/\" 'not' 'not' x) "\/" x by A12;
then x = x "\/" ('not' x "/\" 'not' 'not' x) by Th3
.= (x "\/" 'not' x) "/\" (x "\/" 'not' 'not' x) by A8,Th5
.= Top L "/\" (x "\/" 'not' 'not' x) by A14
.= x "\/" 'not' 'not' x by Th4;
hence thesis by A16,YELLOW_0:24;
end;
:: Exercise 3.19
theorem Th86:
for L being bounded LATTICE st L is Heyting & 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 Heyting and
A2: for x being Element of L holds 'not' 'not' x = x;
let x be Element of L;
A3: 'not' (x "\/" 'not' x) = 'not' x "/\" 'not' 'not' x by A1,Th78
.= x "/\" 'not' x by A2;
A4: 'not' x >= 'not' x by ORDERS_2:1;
then x "/\" 'not' x = Bottom L by A1,Th82;
hence x "\/" 'not' x = 'not' (Bottom L) by A2,A3
.= Top L by A1,Th80;
thus thesis by A1,A4,Th82;
end;
:: Exercise 3.19 (1) iff (2)
theorem Th87:
for L being bounded LATTICE holds L is distributive complemented
iff L is Heyting & 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 x9 being Element of L st for y being
Element of L holds (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 by Lm6;
hence L is Heyting & for x being Element of L holds 'not' 'not' x = x by
Lm7;
end;
assume that
A1: L is Heyting and
A2: for x being Element of L holds 'not' 'not' x = x;
thus L is distributive by A1;
let x be Element of L;
take 'not' x;
thus thesis by A1,A2,Th86;
end;
:: Definition 3.20
definition
let B be non empty RelStr;
attr B is Boolean means
B is LATTICE & B is bounded distributive complemented;
end;
registration
cluster Boolean -> reflexive transitive antisymmetric with_infima
with_suprema bounded distributive complemented for non empty RelStr;
coherence;
end;
registration
cluster reflexive transitive antisymmetric with_infima with_suprema bounded
distributive complemented -> Boolean for non empty RelStr;
coherence;
end;
registration
cluster Boolean -> Heyting for non empty RelStr;
coherence by Th87;
end;
registration
cluster strict Boolean non empty for LATTICE;
existence
proof
take BoolePoset {};
thus thesis;
end;
end;
registration
cluster strict Heyting non empty for LATTICE;
existence
proof
set L = the strict Boolean non empty LATTICE;
take L;
thus thesis;
end;
end;