Copyright (c) 1996 Association of Mizar Users
environ
vocabulary ORDERS_1, RELAT_1, OPPCAT_1, RELAT_2, LATTICE3, YELLOW_0, LATTICES,
BHSP_3, WAYBEL_0, FINSET_1, QUANTAL1, BOOLE, ZF_LANG, PRE_TOPC, FUNCT_1,
CAT_1, WELLORD1, SEQM_3, WAYBEL_1, PBOOLE, WAYBEL_5, FUNCT_6, FUNCOP_1,
ZF_REFLE, FINSEQ_4, YELLOW_2, ORDINAL2, CARD_3, PRALG_1, REALSET1,
YELLOW_7;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1,
FUNCT_2, FINSET_1, CARD_3, FUNCT_6, REALSET1, PRE_TOPC, PRALG_1, PBOOLE,
STRUCT_0, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL_0,
WAYBEL_5;
constructors LATTICE3, WAYBEL_1, ORDERS_3, WAYBEL_5, PRALG_2;
clusters RELSET_1, STRUCT_0, PRALG_1, MSUALG_1, LATTICE3, YELLOW_0, WAYBEL_0,
WAYBEL_1, WAYBEL_5, FINSET_1, PBOOLE, PRVECT_1, CANTOR_1, SUBSET_1,
FRAENKEL, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_2, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1,
WAYBEL_5, XBOOLE_0;
theorems RELAT_1, RELAT_2, FUNCT_1, FUNCT_2, CARD_3, STRUCT_0, ORDERS_1,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_5, PBOOLE,
FUNCT_6, FUNCOP_1, MSUALG_1, PRALG_2, YELLOW_5, PRALG_1, XBOOLE_0;
schemes ZFREFLE1, YELLOW_2;
begin
definition
let L be RelStr;
redefine func L~; synonym L opp;
end;
theorem Th1:
for L being RelStr, x,y being Element of L opp holds x <= y iff ~x >= ~y
proof let L be RelStr, x,y be Element of L opp;
~x = x & (~x)~ = ~x & ~y = y & (~y)~ = ~y by LATTICE3:def 6,def 7;
hence thesis by LATTICE3:9;
end;
theorem Th2:
for L being RelStr, x being Element of L, y being Element of L opp holds
(x <= ~y iff x~ >= y) & (x >= ~y iff x~ <= y)
proof let L be RelStr, x be Element of L, y be Element of L opp;
~(x~) = x~ & x~ = x by LATTICE3:def 6,def 7;
hence thesis by Th1;
end;
theorem
for L being RelStr holds L is empty iff L opp is empty
proof let L be RelStr;
(L is empty iff the carrier of L is empty) &
L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5,STRUCT_0:def 1;
hence thesis by STRUCT_0:def 1;
end;
theorem Th4:
for L being RelStr holds L is reflexive iff L opp is reflexive
proof let L be RelStr;
A1: L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
thus L is reflexive implies L opp is reflexive
proof assume L is reflexive;
then A2: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_1:
def 4;
let x be set; assume x in the carrier of L opp;
then [x,x] in the InternalRel of L by A1,A2,RELAT_2:def 1;
hence thesis by A1,RELAT_1:def 7;
end;
assume L opp is reflexive;
then A3: the InternalRel of L opp is_reflexive_in the carrier of L opp
by ORDERS_1:def 4;
let x be set; assume x in the carrier of L;
then [x,x] in the InternalRel of L opp by A1,A3,RELAT_2:def 1;
hence thesis by A1,RELAT_1:def 7;
end;
theorem Th5:
for L being RelStr holds L is antisymmetric iff L opp is antisymmetric
proof let L be RelStr;
thus L is antisymmetric implies L opp is antisymmetric
proof assume
A1: L is antisymmetric;
let x,y be Element of L opp;
assume x <= y & x >= y;
then ~x >= ~y & ~x <= ~y by Th1;
then ~x = ~y by A1,YELLOW_0:def 3;
hence x = ~y by LATTICE3:def 7 .= y by LATTICE3:def 7;
end;
assume
A2: L opp is antisymmetric;
let x,y be Element of L;
assume x <= y & x >= y;
then x~ >= y~ & x~ <= y~ by LATTICE3:9;
then x~ = y~ by A2,YELLOW_0:def 3;
hence x = y~ by LATTICE3:def 6 .= y by LATTICE3:def 6;
end;
theorem Th6:
for L being RelStr holds L is transitive iff L opp is transitive
proof let L be RelStr;
thus L is transitive implies L opp is transitive
proof assume
A1: L is transitive;
let x,y,z be Element of L opp;
assume x <= y & z >= y;
then ~x >= ~y & ~z <= ~y by Th1;
then ~x >= ~z by A1,YELLOW_0:def 2;
hence thesis by Th1;
end;
assume
A2: L opp is transitive;
let x,y,z be Element of L;
assume x <= y & z >= y;
then x~ >= y~ & z~ <= y~ by LATTICE3:9;
then x~ >= z~ by A2,YELLOW_0:def 2;
hence thesis by LATTICE3:9;
end;
theorem Th7:
for L being non empty RelStr holds L is connected iff L opp is connected
proof let L be non empty RelStr;
thus L is connected implies L opp is connected
proof assume
A1: for x,y being Element of L holds x <= y or x >= y;
let x,y be Element of L opp;
~x <= ~y or ~x >= ~y by A1;
hence thesis by Th1;
end;
assume
A2: for x,y being Element of L opp holds x <= y or x >= y;
let x,y be Element of L;
x~ <= y~ or x~ >= y~ by A2;
hence thesis by LATTICE3:9;
end;
definition
let L be reflexive RelStr;
cluster L opp -> reflexive;
coherence by Th4;
end;
definition
let L be transitive RelStr;
cluster L opp -> transitive;
coherence by Th6;
end;
definition
let L be antisymmetric RelStr;
cluster L opp -> antisymmetric;
coherence by Th5;
end;
definition
let L be connected (non empty RelStr);
cluster L opp -> connected;
coherence by Th7;
end;
theorem Th8:
for L being RelStr, x being Element of L, X being set holds
(x is_<=_than X iff x~ is_>=_than X) &
(x is_>=_than X iff x~ is_<=_than X)
proof
A1: now let L be RelStr, x be Element of L, X be set; assume
A2: x is_<=_than X;
thus x~ is_>=_than X
proof let a be Element of L opp; assume
A3: a in X;
A4: (~a)~ = ~a & ~a = a by LATTICE3:def 6,def 7;
then x <= ~a by A2,A3,LATTICE3:def 8;
hence thesis by A4,LATTICE3:9;
end;
end;
A5: now let L be RelStr, x be Element of L, X be set; assume
A6: x is_>=_than X;
thus x~ is_<=_than X
proof let a be Element of L opp; assume
A7: a in X;
A8: (~a)~ = ~a & ~a = a by LATTICE3:def 6,def 7;
then x >= ~a by A6,A7,LATTICE3:def 9;
hence thesis by A8,LATTICE3:9;
end;
end;
let L be RelStr, x be Element of L, X be set;
A9: x~~ = x~ & x~ = x by LATTICE3:def 6;
A10: L opp~ = the RelStr of L by LATTICE3:8;
then x~~ is_<=_than X implies x is_<=_than X by A9,YELLOW_0:2;
hence x is_<=_than X iff x~ is_>=_than X by A1,A5;
x~~ is_>=_than X implies x is_>=_than X by A9,A10,YELLOW_0:2;
hence thesis by A1,A5;
end;
theorem Th9:
for L being RelStr, x being Element of L opp, X being set holds
(x is_<=_than X iff ~x is_>=_than X) &
(x is_>=_than X iff ~x is_<=_than X)
proof let L be RelStr, x be Element of L opp, X be set;
(~x)~ = ~x & ~x = x by LATTICE3:def 6,def 7;
hence thesis by Th8;
end;
theorem Th10:
for L being RelStr, X being set holds ex_sup_of X,L iff ex_inf_of X,L opp
proof let L be RelStr, X be set;
hereby assume ex_sup_of X,L;
then consider a being Element of L such that
A1: X is_<=_than a and
A2: for b being Element of L st X is_<=_than b holds b >= a and
A3: for c being Element of L st X is_<=_than c &
for b being Element of L st X is_<=_than b holds b >= c
holds c = a by YELLOW_0:def 7;
thus ex_inf_of X,L opp
proof take a~;
thus X is_>=_than a~ by A1,Th8;
hereby let b be Element of L opp; assume
X is_>=_than b;
then X is_<=_than ~b by Th9;
then ~b >= a by A2;
hence b <= a~ by Th2;
end;
let c be Element of L opp; assume
X is_>=_than c;
then A4: X is_<=_than ~c by Th9;
assume
A5: for b being Element of L opp st X is_>=_than b holds b <= c;
now let b be Element of L; assume
X is_<=_than b;
then X is_>=_than b~ by Th8;
then b~ <= c by A5;
hence b >= ~c by Th2;
end;
then ~c = a & ~c = c by A3,A4,LATTICE3:def 7;
hence thesis by LATTICE3:def 6;
end;
end;
assume ex_inf_of X,L opp;
then consider a being Element of L opp such that
A6: X is_>=_than a and
A7: for b being Element of L opp st X is_>=_than b holds b <= a and
A8: for c being Element of L opp st X is_>=_than c &
for b being Element of L opp st X is_>=_than b holds b <= c
holds c = a by YELLOW_0:def 8;
take ~a;
thus X is_<=_than ~a by A6,Th9;
hereby let b be Element of L; assume
X is_<=_than b;
then X is_>=_than b~ by Th8;
then b~ <= a by A7;
hence b >= ~a by Th2;
end;
let c be Element of L; assume
X is_<=_than c;
then A9: X is_>=_than c~ by Th8;
assume
A10: for b being Element of L st X is_<=_than b holds b >= c;
now let b be Element of L opp; assume
X is_>=_than b;
then X is_<=_than ~b by Th9;
then ~b >= c by A10;
hence b <= c~ by Th2;
end;
then c~ = a & c~ = c by A8,A9,LATTICE3:def 6;
hence thesis by LATTICE3:def 7;
end;
theorem Th11:
for L being RelStr, X being set holds ex_sup_of X,L opp iff ex_inf_of X,L
proof let L be RelStr, X be set;
L opp~ = the RelStr of L by LATTICE3:8;
then ex_inf_of X,L iff ex_inf_of X,L opp~ by YELLOW_0:14;
hence thesis by Th10;
end;
theorem Th12:
for L being non empty RelStr, X being set
st ex_sup_of X,L or ex_inf_of X,L opp
holds "\/"(X,L) = "/\"(X,L opp)
proof let L be non empty RelStr, X be set; assume
ex_sup_of X,L or ex_inf_of X,L opp;
then A1: ex_sup_of X,L & ex_inf_of X,L opp by Th10;
then "\/"(X,L) is_>=_than X by YELLOW_0:def 9;
then A2: "\/"(X,L)~ is_<=_than X by Th8;
now let x be Element of L opp; assume x is_<=_than X;
then ~x is_>=_than X by Th9;
then ~x >= "\/"(X,L) by A1,YELLOW_0:def 9;
hence x <= "\/"(X,L)~ by Th2;
end;
then "/\"(X,L opp) = "\/"(X,L)~ by A1,A2,YELLOW_0:def 10;
hence thesis by LATTICE3:def 6;
end;
theorem Th13:
for L being non empty RelStr, X being set
st ex_inf_of X,L or ex_sup_of X,L opp
holds "/\"(X,L) = "\/"(X,L opp)
proof let L be non empty RelStr, X be set; assume
ex_inf_of X,L or ex_sup_of X,L opp;
then A1: ex_inf_of X,L & ex_sup_of X,L opp by Th11;
then "/\"(X,L) is_<=_than X by YELLOW_0:def 10;
then A2: "/\"(X,L)~ is_>=_than X by Th8;
now let x be Element of L opp; assume x is_>=_than X;
then ~x is_<=_than X by Th9;
then ~x <= "/\"(X,L) by A1,YELLOW_0:def 10;
hence x >= "/\"(X,L)~ by Th2;
end;
then "\/"(X,L opp) = "/\"(X,L)~ by A1,A2,YELLOW_0:def 9;
hence thesis by LATTICE3:def 6;
end;
theorem Th14:
for L1,L2 being RelStr
st the RelStr of L1 = the RelStr of L2 & L1 is with_infima
holds L2 is with_infima
proof let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: for x,y being Element of L1
ex z being Element of L1 st z <= x & z <= y &
for z' being Element of L1 st z' <= x & z' <= y holds z' <= z;
let a,b be Element of L2;
reconsider x = a, y = b as Element of L1 by A1;
consider z being Element of L1 such that
A3: z <= x & z <= y and
A4: for z' being Element of L1 st z' <= x & z' <= y holds z' <= z by A2;
reconsider c = z as Element of L2 by A1;
take c; thus c <= a & c <= b by A1,A3,YELLOW_0:1;
let d be Element of L2;
reconsider z' = d as Element of L1 by A1;
assume d <= a & d <= b;
then z' <= x & z' <= y by A1,YELLOW_0:1;
then z' <= z by A4;
hence thesis by A1,YELLOW_0:1;
end;
theorem
for L1,L2 being RelStr
st the RelStr of L1 = the RelStr of L2 & L1 is with_suprema
holds L2 is with_suprema
proof let L1,L2 be RelStr such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: for x,y being Element of L1
ex z being Element of L1 st z >= x & z >= y &
for z' being Element of L1 st z' >= x & z' >= y holds z' >= z;
let a,b be Element of L2;
reconsider x = a, y = b as Element of L1 by A1;
consider z being Element of L1 such that
A3: z >= x & z >= y and
A4: for z' being Element of L1 st z' >= x & z' >= y holds z' >= z by A2;
reconsider c = z as Element of L2 by A1;
take c; thus c >= a & c >= b by A1,A3,YELLOW_0:1;
let d be Element of L2;
reconsider z' = d as Element of L1 by A1;
assume d >= a & d >= b;
then z' >= x & z' >= y by A1,YELLOW_0:1;
then z' >= z by A4;
hence thesis by A1,YELLOW_0:1;
end;
theorem Th16:
for L being RelStr holds
L is with_infima iff L opp is with_suprema
proof let L be RelStr;
L opp~ = the RelStr of L by LATTICE3:8;
then L is with_infima iff L opp~ is with_infima by Th14;
hence thesis by LATTICE3:10;
end;
:: LATTICE3:10
:: for L being RelStr holds L opp is with_infima iff L is with_suprema;
theorem Th17:
for L being non empty RelStr holds
L is complete iff L opp is complete
proof
A1: now let L be non empty RelStr; assume
A2: L is complete;
thus L opp is complete
proof let X be set;
set Y = {x where x is Element of L: x is_<=_than X};
consider a being Element of L such that
A3: Y is_<=_than a & for b being Element of L st Y is_<=_than b holds a <=
b
by A2,LATTICE3:def 12;
take x = a~;
thus X is_<=_than x
proof let y be Element of L opp; assume
A4: y in X;
Y is_<=_than ~y
proof let b be Element of L; assume b in Y;
then y = ~y & ex z being Element of L st b = z & z is_<=_than X
by LATTICE3:def 7;
hence b <= ~y by A4,LATTICE3:def 8;
end;
then a <= ~y by A3;
hence thesis by Th2;
end;
let y be Element of L opp; assume X is_<=_than y;
then X is_>=_than ~y by Th9;
then ~y in Y;
then a >= ~y & ~x = x & x = a by A3,LATTICE3:def 6,def 7,def 9;
hence thesis by Th1;
end;
end;
let L be non empty RelStr;
L opp~ = the RelStr of L by LATTICE3:8;
then L opp~ is complete implies L is complete by YELLOW_0:3;
hence thesis by A1;
end;
definition
let L be with_infima RelStr;
cluster L opp -> with_suprema;
coherence by Th16;
end;
definition
let L be with_suprema RelStr;
cluster L opp -> with_infima;
coherence by LATTICE3:10;
end;
definition
let L be complete (non empty RelStr);
cluster L opp -> complete;
coherence by Th17;
end;
theorem
for L being non empty RelStr
for X being Subset of L, Y being Subset of L opp st X = Y
holds fininfs X = finsups Y & finsups X = fininfs Y
proof let L be non empty RelStr;
let X be Subset of L, Y be Subset of L opp such that
A1: X = Y;
A2: fininfs X = {"/\"(Z,L) where Z is finite Subset of X: ex_inf_of Z,L}
by WAYBEL_0:def 28;
A3: finsups Y = {"\/"
(Z,L opp) where Z is finite Subset of Y: ex_sup_of Z,L opp}
by WAYBEL_0:def 27;
thus fininfs X c= finsups Y
proof let x be set; assume x in fininfs X;
then consider Z being finite Subset of X such that
A4: x = "/\"(Z,L) & ex_inf_of Z,L by A2;
x = "\/"(Z,L opp) & ex_sup_of Z, L opp by A4,Th11,Th13;
hence thesis by A1,A3;
end;
thus finsups Y c= fininfs X
proof let x be set; assume x in finsups Y;
then consider Z being finite Subset of Y such that
A5: x = "\/"(Z,L opp) & ex_sup_of Z,L opp by A3;
x = "/\"(Z,L) & ex_inf_of Z, L by A5,Th11,Th13;
hence thesis by A1,A2;
end;
A6: fininfs Y = {"/\"
(Z,L opp) where Z is finite Subset of Y: ex_inf_of Z,L opp}
by WAYBEL_0:def 28;
A7: finsups X = {"\/"(Z,L) where Z is finite Subset of X: ex_sup_of Z,L}
by WAYBEL_0:def 27;
thus finsups X c= fininfs Y
proof let x be set; assume x in finsups X;
then consider Z being finite Subset of X such that
A8: x = "\/"(Z,L) & ex_sup_of Z,L by A7;
x = "/\"(Z,L opp) & ex_inf_of Z, L opp by A8,Th10,Th12;
hence thesis by A1,A6;
end;
let x be set; assume x in fininfs Y;
then consider Z being finite Subset of Y such that
A9: x = "/\"(Z,L opp) & ex_inf_of Z,L opp by A6;
x = "\/"(Z,L) & ex_sup_of Z, L by A9,Th10,Th12;
hence thesis by A1,A7;
end;
theorem Th19:
for L being RelStr
for X being Subset of L, Y being Subset of L opp st X = Y
holds downarrow X = uparrow Y & uparrow X = downarrow Y
proof let L be RelStr;
let X be Subset of L, Y be Subset of L opp such that
A1: X = Y;
thus downarrow X c= uparrow Y
proof let x be set; assume
A2: x in downarrow X;
then reconsider x as Element of L;
consider y being Element of L such that
A3: y >= x & y in X by A2,WAYBEL_0:def 15;
y~ <= x~ & y~ = y & x~ = x by A3,LATTICE3:9,def 6;
hence thesis by A1,A3,WAYBEL_0:def 16;
end;
thus uparrow Y c= downarrow X
proof let x be set; assume
A4: x in uparrow Y;
then reconsider x as Element of L opp;
consider y being Element of L opp such that
A5: y <= x & y in Y by A4,WAYBEL_0:def 16;
~y >= ~x & ~y = y & ~x = x by A5,Th1,LATTICE3:def 7;
hence thesis by A1,A5,WAYBEL_0:def 15;
end;
thus uparrow X c= downarrow Y
proof let x be set; assume
A6: x in uparrow X;
then reconsider x as Element of L;
consider y being Element of L such that
A7: y <= x & y in X by A6,WAYBEL_0:def 16;
y~ >= x~ & y~ = y & x~ = x by A7,LATTICE3:9,def 6;
hence thesis by A1,A7,WAYBEL_0:def 15;
end;
let x be set; assume
A8: x in downarrow Y;
then reconsider x as Element of L opp;
consider y being Element of L opp such that
A9: y >= x & y in Y by A8,WAYBEL_0:def 15;
~y <= ~x & ~y = y & ~x = x by A9,Th1,LATTICE3:def 7;
hence thesis by A1,A9,WAYBEL_0:def 16;
end;
theorem
for L being non empty RelStr
for x being Element of L, y being Element of L opp st x = y
holds downarrow x = uparrow y & uparrow x = downarrow y
proof let L be non empty RelStr;
let x be Element of L, y be Element of L opp;
downarrow x = downarrow {x} & downarrow y = downarrow {y} &
uparrow x = uparrow {x} & uparrow y = uparrow {y}
by WAYBEL_0:def 17,def 18;
hence thesis by Th19;
end;
theorem Th21:
for L being with_infima Poset, x,y being Element of L
holds x"/\"y = (x~)"\/"(y~)
proof let L be with_infima Poset, x,y be Element of L;
x"/\"y <= x & x"/\"y <= y by YELLOW_0:23;
then A1: (x"/\"y)~ >= x~ & (x"/\"y)~ >= y~ by LATTICE3:9;
A2: x~ = x & ~(x~) = x~ & y~ = y & ~(y~) = y~ by LATTICE3:def 6,def 7;
now let d be Element of L opp; assume d >= x~ & d >= y~;
then ~d <= x & ~d <= y by A2,Th1;
then ~d <= x"/\"y & (~d)~ = ~d & ~d = d by LATTICE3:def 6,def 7,YELLOW_0:
23;
hence (x"/\"y)~ <= d by LATTICE3:9;
end;
then (x"/\"y)~ = (x~)"\/"(y~) by A1,YELLOW_0:22;
hence thesis by LATTICE3:def 6;
end;
theorem Th22:
for L being with_infima Poset, x,y being Element of L opp
holds (~x)"/\"(~y) = x"\/"y
proof let L be with_infima Poset, x,y be Element of L opp;
~x = x & (~x)~ = ~x & ~y = y & (~y)~ = ~y by LATTICE3:def 6,def 7;
hence thesis by Th21;
end;
theorem Th23:
for L being with_suprema Poset, x,y being Element of L
holds x"\/"y = (x~)"/\"(y~)
proof let L be with_suprema Poset, x,y be Element of L;
x"\/"y >= x & x"\/"y >= y by YELLOW_0:22;
then A1: (x"\/"y)~ <= x~ & (x"\/"y)~ <= y~ by LATTICE3:9;
A2: x~ = x & ~(x~) = x~ & y~ = y & ~(y~) = y~ by LATTICE3:def 6,def 7;
now let d be Element of L opp; assume d <= x~ & d <= y~;
then ~d >= x & ~d >= y by A2,Th1;
then ~d >= x"\/"y & (~d)~ = ~d & ~d = d by LATTICE3:def 6,def 7,YELLOW_0:
22;
hence (x"\/"y)~ >= d by LATTICE3:9;
end;
then (x"\/"y)~ = (x~)"/\"(y~) by A1,YELLOW_0:23;
hence thesis by LATTICE3:def 6;
end;
theorem Th24:
for L being with_suprema Poset, x,y being Element of L opp
holds (~x)"\/"(~y) = x"/\"y
proof let L be with_suprema Poset, x,y be Element of L opp;
~x = x & (~x)~ = ~x & ~y = y & (~y)~ = ~y by LATTICE3:def 6,def 7;
hence thesis by Th23;
end;
theorem Th25:
for L being LATTICE holds
L is distributive iff L opp is distributive
proof let L be LATTICE;
hereby assume
A1: L is distributive;
thus L opp is distributive
proof let x,y,z be Element of L opp;
A2: ~(y"\/"z) = y"\/"z & ~(x"/\"y) = x"/\"y & ~(x"/\"z) = x"/\"
z by LATTICE3:def 7;
thus x "/\" (y "\/" z)
= (~x)"\/"~(y "\/" z) by Th24
.= (~x)"\/"((~y)"/\"~z) by A2,Th22
.= ((~x)"\/"(~y))"/\"((~x)"\/"~z) by A1,WAYBEL_1:6
.= (~(x"/\"y))"/\"((~x)"\/"~z) by A2,Th24
.= (~(x"/\"y))"/\"~(x"/\"z) by A2,Th24
.= (x "/\" y) "\/" (x "/\" z) by Th22;
end;
end;
assume
A3: L opp is distributive;
let x,y,z be Element of L;
A4: (y"\/"z)~ = y"\/"z & (x"/\"y)~ = x"/\"y & (x"/\"z)~ = x"/\"
z by LATTICE3:def 6;
thus x "/\" (y "\/" z)
= (x~)"\/"((y "\/" z)~) by Th21
.= (x~)"\/"((y~)"/\"(z~)) by A4,Th23
.= ((x~)"\/"(y~))"/\"((x~)"\/"(z~)) by A3,WAYBEL_1:6
.= ((x"/\"y)~)"/\"((x~)"\/"(z~)) by A4,Th21
.= ((x"/\"y)~)"/\"((x"/\"z)~) by A4,Th21
.= (x "/\" y) "\/" (x "/\" z) by Th23;
end;
definition
let L be distributive LATTICE;
cluster L opp -> distributive;
coherence by Th25;
end;
theorem Th26:
for L being RelStr, x be set holds
x is directed Subset of L iff x is filtered Subset of L opp
proof let L be RelStr, x be set;
A1: L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
hereby assume x is directed Subset of L;
then reconsider X = x as directed Subset of L;
reconsider Y = X as Subset of L opp by A1;
Y is filtered
proof let x,y be Element of L opp; assume
A2: x in Y & y in Y;
x = ~x & y = ~y by LATTICE3:def 7;
then consider z being Element of L such that
A3: z in X & z >= ~x & z >= ~y by A2,WAYBEL_0:def 1;
take z~; z = z~ & ~(z~) = z~ by LATTICE3:def 6,def 7;
hence thesis by A3,Th1;
end;
hence x is filtered Subset of L opp;
end;
assume x is filtered Subset of L opp;
then reconsider X = x as filtered Subset of L opp;
reconsider Y = X as Subset of L by A1;
Y is directed
proof let x,y be Element of L; assume
A4: x in Y & y in Y;
x = x~ & y = y~ by LATTICE3:def 6;
then consider z being Element of L opp such that
A5: z in X & z <= x~ & z <= y~ by A4,WAYBEL_0:def 2;
take ~z; z = ~z & (~z)~ = ~z by LATTICE3:def 6,def 7;
hence thesis by A5,LATTICE3:9;
end;
hence thesis;
end;
theorem
for L being RelStr, x be set holds
x is directed Subset of L opp iff x is filtered Subset of L
proof let L be RelStr, x be set;
L opp~ = the RelStr of L by LATTICE3:8;
then x is filtered Subset of L iff x is filtered Subset of L opp~
by WAYBEL_0:4;
hence thesis by Th26;
end;
theorem Th28:
for L being RelStr, x be set holds
x is lower Subset of L iff x is upper Subset of L opp
proof let L be RelStr, x be set;
A1: L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
hereby assume x is lower Subset of L;
then reconsider X = x as lower Subset of L;
reconsider Y = X as Subset of L opp by A1;
Y is upper
proof let x,y be Element of L opp; assume
A2: x in Y & x <= y;
then x = ~x & y = ~y & ~x >= ~y by Th1,LATTICE3:def 7;
hence thesis by A2,WAYBEL_0:def 19;
end;
hence x is upper Subset of L opp;
end;
assume x is upper Subset of L opp;
then reconsider X = x as upper Subset of L opp;
reconsider Y = X as Subset of L by A1;
Y is lower
proof let x,y be Element of L; assume
A3: x in Y & x >= y;
then x = x~ & y = y~ & x~ <= y~ by LATTICE3:9,def 6;
hence thesis by A3,WAYBEL_0:def 20;
end;
hence thesis;
end;
theorem
for L being RelStr, x be set holds
x is lower Subset of L opp iff x is upper Subset of L
proof let L be RelStr, x be set;
L opp~ = the RelStr of L by LATTICE3:8;
then x is upper Subset of L iff x is upper Subset of L opp~
by WAYBEL_0:25;
hence thesis by Th28;
end;
theorem Th30:
for L being RelStr holds L is lower-bounded iff L opp is upper-bounded
proof let L be RelStr;
A1: L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
thus L is lower-bounded implies L opp is upper-bounded
proof given x being Element of L such that
A2: x is_<=_than the carrier of L;
take x~; thus thesis by A1,A2,Th8;
end;
given x being Element of L opp such that
A3: x is_>=_than the carrier of L opp;
take ~x; thus thesis by A1,A3,Th9;
end;
theorem Th31:
for L being RelStr holds L opp is lower-bounded iff L is upper-bounded
proof let L be RelStr;
A1: L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
thus L opp is lower-bounded implies L is upper-bounded
proof given x being Element of L opp such that
A2: x is_<=_than the carrier of L opp;
take ~x; thus thesis by A1,A2,Th9;
end;
given x being Element of L such that
A3: x is_>=_than the carrier of L;
take x~; thus thesis by A1,A3,Th8;
end;
theorem
for L being RelStr holds L is bounded iff L opp is bounded
proof let L be RelStr;
thus L is bounded implies L opp is bounded
proof assume L is lower-bounded upper-bounded;
hence L opp is lower-bounded upper-bounded by Th30,Th31;
end;
assume L opp is lower-bounded upper-bounded;
hence L is lower-bounded upper-bounded by Th30,Th31;
end;
theorem Th33:
for L being lower-bounded antisymmetric non empty RelStr holds
(Bottom L)~ = Top (L opp) & ~Top (L opp) = Bottom L
proof let L be lower-bounded antisymmetric non empty RelStr;
ex_sup_of {},L by YELLOW_0:42;
then A1: "\/"({},L) = "/\"({},L opp) & (Bottom L)~ = Bottom
L by Th12,LATTICE3:def 6;
hence (Bottom L)~ = "/\"({}
,L opp) by YELLOW_0:def 11 .= Top (L opp) by YELLOW_0:def 12;
hence ~Top (L opp) = Bottom L by A1,LATTICE3:def 7;
end;
theorem Th34:
for L being upper-bounded antisymmetric non empty RelStr holds
(Top L)~ = Bottom (L opp) & ~Bottom (L opp) = Top L
proof let L be upper-bounded antisymmetric non empty RelStr;
ex_inf_of {},L by YELLOW_0:43;
then A1: "/\"({},L) = "\/"({},L opp) & (Top L)~ = Top L by Th13,LATTICE3:def 6
;
hence (Top L)~ = "\/"({}
,L opp) by YELLOW_0:def 12 .= Bottom (L opp) by YELLOW_0:def 11;
hence thesis by A1,LATTICE3:def 7;
end;
theorem Th35:
for L being bounded LATTICE, x,y being Element of L holds
y is_a_complement_of x iff y~ is_a_complement_of x~
proof let L be bounded LATTICE, x,y be Element of L;
hereby assume y is_a_complement_of x;
then A1: x "\/" y = Top L & x "/\" y = Bottom L by WAYBEL_1:def 23;
thus y~ is_a_complement_of x~
proof
thus (x~)"\/"(y~) = x"/\"y by Th21 .= (Bottom L)~ by A1,LATTICE3:def 6
.= Top (L opp) by Th33;
thus (x~)"/\"(y~) = x"\/"y by Th23 .= (Top L)~ by A1,LATTICE3:def 6
.= Bottom (L opp) by Th34;
end;
end;
assume
A2: (x~)"\/"(y~) = Top (L opp) & (x~)"/\"(y~) = Bottom (L opp);
thus x "\/" y = (x~)"/\"(y~) by Th23 .= (Top L)~ by A2,Th34
.= Top L by LATTICE3:def 6;
thus x "/\" y = (x~)"\/"(y~) by Th21 .= (Bottom L)~ by A2,Th33
.= Bottom L by LATTICE3:def 6;
end;
theorem Th36:
for L being bounded LATTICE holds L is complemented iff L opp is complemented
proof let L be bounded LATTICE;
thus L is complemented implies L opp is complemented
proof assume
A1: for x being Element of L ex y being Element of L st
y is_a_complement_of x;
let x be Element of L opp;
consider y being Element of L such that
A2: y is_a_complement_of ~x by A1;
take y~; ~x = x & (~x)~ = ~x by LATTICE3:def 6,def 7;
hence y~ is_a_complement_of x by A2,Th35;
end;
assume
A3: for x being Element of L opp ex y being Element of L opp st
y is_a_complement_of x;
let x be Element of L;
consider y being Element of L opp such that
A4: y is_a_complement_of x~ by A3;
take ~y; ~y = y & (~y)~ = ~y by LATTICE3:def 6,def 7;
hence thesis by A4,Th35;
end;
definition
let L be lower-bounded RelStr;
cluster L opp -> upper-bounded;
coherence by Th30;
end;
definition
let L be upper-bounded RelStr;
cluster L opp -> lower-bounded;
coherence by Th31;
end;
definition
let L be complemented (bounded LATTICE);
cluster L opp -> complemented;
coherence by Th36;
end;
:: Collorary: L is Boolean -> L opp is Boolean
theorem
for L being Boolean LATTICE, x being Element of L holds
'not'(x~) = 'not' x
proof let L be Boolean LATTICE, x be Element of L;
for x being Element of L holds 'not' 'not' x = x by WAYBEL_1:90;
then 'not' x is_a_complement_of x by WAYBEL_1:89;
then ('not' x)~ is_a_complement_of x~ by Th35;
then 'not'(x~) = ('not' x)~ by YELLOW_5:11;
hence thesis by LATTICE3:def 6;
end;
definition
let L be non empty RelStr;
func ComplMap L -> map of L, L opp means:
Def1:
for x being Element of L holds it.x = 'not' x;
existence
proof deffunc N(Element of L) = 'not' $1;
consider f being map of L,L such that
A1: for x being Element of L holds f.x = N(x) from LambdaMD;
L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
then reconsider f as map of L,L opp;
take f; thus thesis by A1;
end;
correctness
proof let f1,f2 be map of L,L opp such that
A2: not thesis;
now let x be Element of L;
thus f1.x = 'not' x by A2 .= f2.x by A2;
end;
hence thesis by A2,YELLOW_2:9;
end;
end;
definition
let L be Boolean LATTICE;
cluster ComplMap L -> one-to-one;
coherence
proof set f = ComplMap L;
let a,b be Element of L;
f.a = 'not' a & f.b = 'not' b & 'not' 'not' a = a & 'not' 'not'
b = b by Def1,WAYBEL_1:90;
hence thesis;
end;
end;
definition
let L be Boolean LATTICE;
cluster ComplMap L -> isomorphic;
coherence
proof set f = ComplMap L;
A1: L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
A2: dom f = the carrier of L by FUNCT_2:def 1;
A3: rng f = the carrier of L opp
proof thus rng f c= the carrier of L opp;
let x be set; assume x in the carrier of L opp;
then reconsider x as Element of L by A1;
x = 'not' 'not' x by WAYBEL_1:90;
then f.'not' x = x by Def1;
hence thesis by A2,FUNCT_1:def 5;
end;
now let x,y be Element of L;
f.x = 'not' x & f.y = 'not' y by Def1;
then f.x = ('not' x)~ & f.y = ('not' y)~ by LATTICE3:def 6;
then ('not' x >= 'not' y iff f.x <= f.y) & x = 'not' 'not' x &
y = 'not' 'not'
y by LATTICE3:9,WAYBEL_1:90;
hence x <= y iff f.x <= f.y by WAYBEL_1:86;
end;
hence thesis by A3,WAYBEL_0:66;
end;
end;
theorem
for L being Boolean LATTICE holds L, L opp are_isomorphic
proof let L be Boolean LATTICE;
take ComplMap L; thus thesis;
end;
theorem
for S,T being non empty RelStr, f be set holds
(f is map of S,T iff f is map of S opp,T) &
(f is map of S,T iff f is map of S,T opp) &
(f is map of S,T iff f is map of S opp,T opp)
proof let S,T be non empty RelStr;
S~ = RelStr(#the carrier of S, (the InternalRel of S)~#) &
T~ = RelStr(#the carrier of T, (the InternalRel of T)~#) by LATTICE3:def 5;
hence thesis;
end;
theorem
for S,T being non empty RelStr
for f being map of S,T, g being map of S,T opp st f = g holds
(f is monotone iff g is antitone) &
(f is antitone iff g is monotone)
proof let S,T be non empty RelStr;
let f be map of S,T, g be map of S,T~ such that
A1: f = g;
thus f is monotone implies g is antitone
proof assume
A2: for x,y being Element of S st x <= y holds f.x <= f.y;
let x,y be Element of S; assume x <= y;
then f.x <= f.y & (f.x)~ = f.x & (f.y)~ = f.y by A2,LATTICE3:def 6;
hence thesis by A1,LATTICE3:9;
end;
thus g is antitone implies f is monotone
proof assume
A3: for x,y being Element of S st x <= y
for a,b being Element of T opp st a = g.x & b = g.y holds a >= b;
let x,y be Element of S; assume x <= y;
then g.y <= g.x & ~(g.x) = g.x & ~(g.y) = g.y by A3,LATTICE3:def 7;
hence thesis by A1,Th1;
end;
thus f is antitone implies g is monotone
proof assume
A4: for x,y being Element of S st x <= y
for a,b being Element of T st a = f.x & b = f.y holds a >= b;
let x,y be Element of S; assume x <= y;
then f.y <= f.x & (f.x)~ = f.x & (f.y)~ = f.y by A4,LATTICE3:def 6;
hence thesis by A1,LATTICE3:9;
end;
thus g is monotone implies f is antitone
proof assume
A5: for x,y being Element of S st x <= y holds g.x <= g.y;
let x,y be Element of S; assume x <= y;
then g.y >= g.x & ~(g.x) = g.x & ~(g.y) = g.y by A5,LATTICE3:def 7;
hence thesis by A1,Th1;
end;
end;
theorem
for S,T being non empty RelStr
for f being map of S,T opp, g being map of S opp,T st f = g holds
(f is monotone iff g is monotone) &
(f is antitone iff g is antitone)
proof let S,T be non empty RelStr;
let f be map of S,T~, g be map of S~,T such that
A1: f = g;
thus f is monotone implies g is monotone
proof assume
A2: for x,y being Element of S st x <= y holds f.x <= f.y;
let x,y be Element of S~; assume x <= y;
then ~y <= ~x by Th1;
then f.~y <= f.~x & ~y = y & ~x = x & ~(f.~x) = f.~x & ~(f.~y) = f.~y
by A2,LATTICE3:def 7;
hence thesis by A1,Th1;
end;
thus g is monotone implies f is monotone
proof assume
A3: for x,y being Element of S opp st x <= y holds g.x <= g.y;
let x,y be Element of S; assume x <= y;
then y~ <= x~ by LATTICE3:9;
then g.(y~) <= g.(x~) & y~ = y & x~ = x & (g.(x~))~ = g.(x~) &
(g.(y~))~ = g.(y~) by A3,LATTICE3:def 6;
hence thesis by A1,LATTICE3:9;
end;
thus f is antitone implies g is antitone
proof assume
A4: for x,y being Element of S st x <= y
for a,b being Element of T~ st a = f.x & b = f.y holds a >= b;
let x,y be Element of S~; assume x <= y;
then ~y <= ~x by Th1;
then f.~y >= f.~x & ~y = y & ~x = x & ~(f.~x) = f.~x & ~(f.~y) = f.~y
by A4,LATTICE3:def 7;
hence thesis by A1,Th1;
end;
thus g is antitone implies f is antitone
proof assume
A5: for x,y being Element of S opp st x <= y
for a,b being Element of T st a = g.x & b = g.y holds a >= b;
let x,y be Element of S; assume x <= y;
then y~ <= x~ by LATTICE3:9;
then g.(y~) >= g.(x~) & y~ = y & x~ = x & (g.(x~))~ = g.(x~) &
(g.(y~))~ = g.(y~) by A5,LATTICE3:def 6;
hence thesis by A1,LATTICE3:9;
end;
end;
theorem Th42:
for S,T being non empty RelStr
for f being map of S,T, g being map of S opp,T opp st f = g holds
(f is monotone iff g is monotone) &
(f is antitone iff g is antitone)
proof let S,T be non empty RelStr;
let f be map of S,T, g be map of S~,T~ such that
A1: f = g;
thus f is monotone implies g is monotone
proof assume
A2: for x,y being Element of S st x <= y holds f.x <= f.y;
let x,y be Element of S~; assume x <= y;
then ~y <= ~x by Th1;
then f.~y <= f.~x & ~y = y & ~x = x & (f.~x)~ = f.~x & (f.~y)~ = f.~y
by A2,LATTICE3:def 6,def 7;
hence thesis by A1,LATTICE3:9;
end;
thus g is monotone implies f is monotone
proof assume
A3: for x,y being Element of S~ st x <= y holds g.x <= g.y;
let x,y be Element of S; assume x <= y;
then y~ <= x~ by LATTICE3:9;
then g.(y~) <= g.(x~) & y~ = y & x~ = x & ~(g.(x~)) = g.(x~) &
~(g.(y~)) = g.(y~) by A3,LATTICE3:def 6,def 7;
hence thesis by A1,Th1;
end;
thus f is antitone implies g is antitone
proof assume
A4: for x,y being Element of S st x <= y
for a,b being Element of T st a = f.x & b = f.y holds a >= b;
let x,y be Element of S~; assume x <= y;
then ~y <= ~x by Th1;
then f.~y >= f.~x & ~y = y & ~x = x & (f.~x)~ = f.~x & (f.~y)~ = f.~y
by A4,LATTICE3:def 6,def 7;
hence thesis by A1,LATTICE3:9;
end;
thus g is antitone implies f is antitone
proof assume
A5: for x,y being Element of S opp st x <= y
for a,b being Element of T opp st a = g.x & b = g.y holds a >= b;
let x,y be Element of S; assume x <= y;
then y~ <= x~ by LATTICE3:9;
then g.(y~) >= g.(x~) & y~ = y & x~ = x & ~(g.(x~)) = g.(x~) &
~(g.(y~)) = g.(y~) by A5,LATTICE3:def 6,def 7;
hence thesis by A1,Th1;
end;
end;
theorem
for S,T being non empty RelStr, f be set holds
(f is Connection of S,T iff f is Connection of S~,T) &
(f is Connection of S,T iff f is Connection of S,T~) &
(f is Connection of S,T iff f is Connection of S~,T~)
proof let S,T be non empty RelStr;
A1: S~ = RelStr(#the carrier of S, (the InternalRel of S)~#) &
T~ = RelStr(#the carrier of T, (the InternalRel of T)~#) by LATTICE3:def 5;
now let S,S1,T,T1 be RelStr; assume
A2: the carrier of S = the carrier of S1 &
the carrier of T = the carrier of T1;
let a be Connection of S,T;
consider f being map of S,T, g being map of T,S such that
A3: a = [f,g] by WAYBEL_1:def 9;
reconsider f as map of S1,T1 by A2;
reconsider g as map of T1,S1 by A2;
a = [f,g] by A3;
hence a is Connection of S1,T1;
end;
hence thesis by A1;
end;
theorem
for S,T being non empty Poset
for f1 being map of S,T, g1 being map of T,S
for f2 being map of S~,T~, g2 being map of T~,S~ st f1 = f2 & g1 = g2 holds
[f1,g1] is Galois iff [g2,f2] is Galois
proof let S,T be non empty Poset;
let f1 be map of S,T, g1 be map of T,S;
let f2 be map of S~,T~, g2 be map of T~,S~ such that
A1: f1 = f2 & g1 = g2;
hereby assume A2: [f1,g1] is Galois;
then g1 is monotone & f1 is monotone &
for t being Element of T, s being Element of S holds t <= f1.s iff g1.t <=
s
by WAYBEL_1:9;
then A3: g2 is monotone & f2 is monotone by A1,Th42;
now let s be Element of S~, t be Element of T~;
~s = s & ~t = t & (f1.~s)~ = f1.~s & (g1.~t)~ = g1.~t &
(~t <= f1.~s iff g1.~t <= ~s) by A2,LATTICE3:def 6,def 7,WAYBEL_1:9;
hence g2.t >= s iff t >= f2.s by A1,Th2;
end;
hence [g2,f2] is Galois by A3,WAYBEL_1:9;
end;
assume A4: [g2,f2] is Galois;
then g2 is monotone & f2 is monotone &
for s being Element of S~, t being Element of T~ holds
s <= g2.t iff f2.s <= t by WAYBEL_1:9;
then A5: g1 is monotone & f1 is monotone by A1,Th42;
now let t be Element of T, s be Element of S;
s~ = s & t~ = t & ~(f2.(s~)) = f2.(s~) & ~(g2.(t~)) = g2.(t~) &
(s~ <= g2.(t~) iff f2.(s~) <= t~) by A4,LATTICE3:def 6,def 7,WAYBEL_1:9;
hence t <= f1.s iff g1.t <= s by A1,Th2;
end;
hence [f1,g1] is Galois by A5,WAYBEL_1:9;
end;
theorem Th45:
for J being set, D being non empty set, K being ManySortedSet of J
for F being DoubleIndexedSet of K,D holds doms F = K
proof let J be set, D be non empty set, K be ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
A1: dom F = J & dom K = J & F"rng F = dom F & dom doms F = F"SubFuncs rng F
by FUNCT_6:def 2,PBOOLE:def 3,RELAT_1:169;
A2: SubFuncs rng F = rng F
proof thus SubFuncs rng F c= rng F by FUNCT_6:27;
let x be set; assume
A3: x in rng F;
then ex y being set st y in dom F & x = F.y by FUNCT_1:def 5;
hence thesis by A3,FUNCT_6:def 1;
end;
now let j be set; assume
A4: j in J; set f = F.j;
(J --> D).j = D by A4,FUNCOP_1:13;
then (doms F).j = dom f & f is Function of K.j,D
by A1,A4,FUNCT_6:31,MSUALG_1:def 2;
hence (doms F).j = K.j by FUNCT_2:def 1;
end;
hence thesis by A1,A2,FUNCT_1:9;
end;
definition
let J, D be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
let j be Element of J;
let k be Element of K.j;
redefine func F..(j,k) -> Element of D;
coherence
proof dom (F.j) = K.j & dom F = J by FUNCT_2:def 1,PBOOLE:def 3;
then F..(j,k) = (F.j).k by FUNCT_6:44;
hence thesis;
end;
end;
theorem Th46:
for L being non empty RelStr
for J being set, K being ManySortedSet of J
for x being set holds
x is DoubleIndexedSet of K,L iff x is DoubleIndexedSet of K,L opp
proof let L be non empty RelStr;
L opp = RelStr(#the carrier of L, (the InternalRel of L)~#)
by LATTICE3:def 5;
hence thesis;
end;
theorem Th47:
for L being complete LATTICE
for J being non empty set, K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup Infs F <= Inf Sups Frege F
proof let L be complete LATTICE;
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, L;
Inf Sups Frege F is_>=_than rng Infs F
proof let x be Element of L; assume
x in rng Infs F;
then consider a being Element of J such that
A1: x = Inf (F.a) by WAYBEL_5:14;
A2: x = inf rng (F.a) by A1,YELLOW_2:def 6;
x is_<=_than rng Sups Frege F
proof let y be Element of L; assume
A3: y in rng Sups Frege F;
reconsider J' = product doms F as non empty set;
reconsider K' = J' --> J as ManySortedSet of J';
reconsider G = Frege F as DoubleIndexedSet of K', L;
consider f being Element of J' such that
A4: y = Sup (G.f) by A3,WAYBEL_5:14;
reconsider f as Element of product doms F;
A5: y = sup rng ((Frege F).f) by A4,YELLOW_2:def 5;
A6: dom F = J & dom Frege F = product doms F by PBOOLE:def 3;
then f.a in dom (F.a) by WAYBEL_5:9;
then reconsider j = f.a as Element of K.a;
j in dom (F.a) by A6,WAYBEL_5:9;
then (F.a).j in rng (F.a) & (F.a).j in rng ((Frege F).f)
by A6,FUNCT_1:def 5,WAYBEL_5:9;
then x <= (F.a).j & (F.a).j <= y by A2,A5,YELLOW_2:24;
hence x <= y by ORDERS_1:26;
end;
then x <= inf rng Sups Frege F by YELLOW_0:33;
hence thesis by YELLOW_2:def 6;
end;
then sup rng Infs F <= Inf Sups Frege F by YELLOW_0:32;
hence thesis by YELLOW_2:def 5;
end;
theorem Th48:
for L being complete LATTICE holds
L is completely-distributive
iff
for J being non empty set, K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup Infs F = Inf Sups Frege F
proof let L be complete LATTICE;
thus L is completely-distributive implies
for J being non empty set, K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup Infs F = Inf Sups Frege F
proof assume that L is complete and
A1: for J being non empty set, K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K, L holds
Inf Sups F = Sup Infs Frege F;
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K,L;
A2: Sup Infs F <= Inf Sups Frege F by Th47;
A3: Inf Sups Frege F = Sup Infs Frege Frege F by A1;
A4: dom Frege F = product doms F & doms F = K & dom K = J &
doms Frege F = (product doms F) --> J & dom F = J &
dom Frege Frege F = product doms Frege F by Th45,PBOOLE:def 3;
rng Infs Frege Frege F is_<=_than Sup Infs F
proof let a be Element of L; assume
A5: a in rng Infs Frege Frege F;
reconsider J' = product doms Frege F as non empty set;
reconsider K' = J' --> product doms F as ManySortedSet of J';
reconsider G = Frege Frege F as DoubleIndexedSet of K', L;
consider g being Element of J' such that
A6: a = Inf (G.g) by A5,WAYBEL_5:14;
ex g' being Function st g = g' & dom g' = dom doms Frege F &
for x being set st x in dom doms Frege F holds g'.x in
(doms Frege F).x
by CARD_3:def 5;
then reconsider g' = g as Function;
deffunc XX(set) = {f.(g'.f) where f is Element of product doms F:
g'.f = $1};
A7: (J' --> J).g = J & dom ((product doms F) --> J) = product doms F
by FUNCOP_1:13,19;
now assume
A8: for j being Element of J holds (K.j) \ XX(j) <> {};
defpred P[set,set] means $2 in (K.$1) \ XX($1);
A9: now let j be set; assume j in J;
then reconsider i = j as Element of J;
consider k being Element of (K.i)\XX(j);
(K.i)\XX(i) <> {} by A8;
then k in (K.i)\XX(i);
hence ex k being set st P[j,k];
end;
consider h being Function such that
A10: dom h = J & for j being set st j in J holds P[j,h.j]
from NonUniqFuncEx(A9);
now let j be set; assume j in J;
then h.j in (K.j) \ XX(j) by A10;
hence h.j in (doms F).j by A4,XBOOLE_0:def 4;
end;
then reconsider h as Element of product doms F by A4,A10,CARD_3:18;
g'.h in (doms Frege F).h by A4,A7,CARD_3:18;
then reconsider j = g'.h as Element of J by A4,FUNCOP_1:13;
h.(g'.h) in XX(j) & h.j in (K.j) \ XX(j) by A10;
hence contradiction by XBOOLE_0:def 4;
end;
then consider j being Element of J such that
A11: (K.j) \ XX(j) = {};
A12: ex_inf_of rng (G.g), L & ex_inf_of rng (F.j),L
by YELLOW_0:17;
rng (F.j) c= rng (G.g)
proof let z be set; assume z in rng (F.j);
then consider u being set such that
A13: u in dom (F.j) & z = (F.j).u by FUNCT_1:def 5;
reconsider u as Element of K.j by A13;
u in XX(j) by A11,XBOOLE_0:def 4;
then consider f being Element of product doms F such that
A14: u = f.(g'.f) & g'.f = j;
A15: dom (G.g) = K'.g & K'.g = product doms F
by FUNCOP_1:13,FUNCT_2:def 1;
G.g = (Frege F)..g' & (Frege F).f = F..f by PRALG_2:def 8;
then (G.g).f = (F..f).j by A4,A14,PRALG_1:def 18;
then (G.g).f = z by A4,A13,A14,PRALG_1:def 18;
hence thesis by A15,FUNCT_1:def 5;
end;
then inf rng (G.g) <= inf rng (F.j) by A12,YELLOW_0:35;
then a <= inf rng (F.j) & Inf (F.j) in rng Infs F
by A6,WAYBEL_5:14,YELLOW_2:def 6;
then a <= Inf (F.j) & Inf (F.j) <=
sup rng Infs F by YELLOW_2:24,def 6;
then a <= sup rng Infs F by ORDERS_1:26;
hence thesis by YELLOW_2:def 5;
end;
then sup rng Infs Frege Frege F <= Sup Infs F by YELLOW_0:32;
then Sup Infs Frege Frege F <= Sup Infs F by YELLOW_2:def 5;
hence Sup Infs F = Inf Sups Frege F by A2,A3,ORDERS_1:25;
end;
assume
A16: for J being non empty set, K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K, L holds
Sup Infs F = Inf Sups Frege F;
thus L is complete;
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K,L;
A17: Inf Sups F >= Sup Infs Frege F by WAYBEL_5:16;
A18: Sup Infs Frege F = Inf Sups Frege Frege F by A16;
A19: dom Frege F = product doms F & doms F = K & dom K = J &
doms Frege F = (product doms F) --> J & dom F = J &
dom Frege Frege F = product doms Frege F by Th45,PBOOLE:def 3;
rng Sups Frege Frege F is_>=_than Inf Sups F
proof let a be Element of L; assume
A20: a in rng Sups Frege Frege F;
reconsider J' = product doms Frege F as non empty set;
reconsider K' = J' --> product doms F as ManySortedSet of J';
reconsider G = Frege Frege F as DoubleIndexedSet of K', L;
consider g being Element of J' such that
A21: a = Sup (G.g) by A20,WAYBEL_5:14;
ex g' being Function st g = g' & dom g' = dom doms Frege F &
for x being set st x in dom doms Frege F holds g'.x in (doms Frege F).x
by CARD_3:def 5;
then reconsider g' = g as Function;
deffunc XX(set) = {f.(g'.f) where f is Element of product doms F:
g'.f = $1};
A22: (J' --> J).g = J & dom ((product doms F) --> J) = product doms F
by FUNCOP_1:13,19;
now assume
A23: for j being Element of J holds (K.j) \ XX(j) <> {};
defpred P[set,set] means $2 in (K.$1) \ XX($1);
A24: now let j be set; assume j in J;
then reconsider i = j as Element of J;
consider k being Element of (K.i)\XX(j);
(K.i)\XX(i) <> {} by A23;
then k in (K.i)\XX(i);
hence ex k being set st P[j,k];
end;
consider h being Function such that
A25: dom h = J & for j being set st j in J holds P[j,h.j]
from NonUniqFuncEx(A24);
now let j be set; assume j in J;
then h.j in (K.j) \ XX(j) by A25;
hence h.j in (doms F).j by A19,XBOOLE_0:def 4;
end;
then reconsider h as Element of product doms F by A19,A25,CARD_3:18;
g'.h in (doms Frege F).h by A19,A22,CARD_3:18;
then reconsider j = g'.h as Element of J by A19,FUNCOP_1:13;
h.(g'.h) in XX(j) & h.j in (K.j) \ XX(j) by A25;
hence contradiction by XBOOLE_0:def 4;
end;
then consider j being Element of J such that
A26: (K.j) \ XX(j) = {};
A27: ex_sup_of rng (G.g), L & ex_sup_of rng (F.j),L
by YELLOW_0:17;
rng (F.j) c= rng (G.g)
proof let z be set; assume z in rng (F.j);
then consider u being set such that
A28: u in dom (F.j) & z = (F.j).u by FUNCT_1:def 5;
reconsider u as Element of K.j by A28;
u in XX(j) by A26,XBOOLE_0:def 4;
then consider f being Element of product doms F such that
A29: u = f.(g'.f) & g'.f = j;
A30: dom (G.g) = K'.g & K'.g = product doms F
by FUNCOP_1:13,FUNCT_2:def 1;
G.g = (Frege F)..g' & (Frege F).f = F..f by PRALG_2:def 8;
then (G.g).f = (F..f).j by A19,A29,PRALG_1:def 18;
then (G.g).f = z by A19,A28,A29,PRALG_1:def 18;
hence thesis by A30,FUNCT_1:def 5;
end;
then sup rng (G.g) >= sup rng (F.j) by A27,YELLOW_0:34;
then a >= sup rng (F.j) & Sup (F.j) in rng Sups F
by A21,WAYBEL_5:14,YELLOW_2:def 5;
then a >= Sup (F.j) & Sup (F.j) >= inf rng Sups F by YELLOW_2:24,def 5;
then a >= inf rng Sups F by ORDERS_1:26;
hence thesis by YELLOW_2:def 6;
end;
then inf rng Sups Frege Frege F >= Inf Sups F by YELLOW_0:33;
then Inf Sups Frege Frege F >= Inf Sups F by YELLOW_2:def 6;
hence Inf Sups F = Sup Infs Frege F by A17,A18,ORDERS_1:25;
end;
theorem Th49:
for L being complete antisymmetric (non empty RelStr), F be Function holds
\\/(F, L) = //\(F, L opp) & //\(F, L) = \\/(F, L opp)
proof let L be complete antisymmetric (non empty RelStr), F be Function;
A1: ex_sup_of rng F,L & ex_inf_of rng F, L by YELLOW_0:17;
thus \\/(F, L) = "\/"(rng F, L) by YELLOW_2:def 5
.= "/\"(rng F, L opp) by A1,Th12
.= //\(F, L opp) by YELLOW_2:def 6;
thus //\(F,L) = "/\"(rng F, L) by YELLOW_2:def 6
.= "\/"(rng F, L opp) by A1,Th13
.= \\/(F, L opp) by YELLOW_2:def 5;
end;
theorem Th50:
for L being complete antisymmetric (non empty RelStr)
for F be Function-yielding Function holds
\//(F, L) = /\\(F, L opp) & /\\(F, L) = \//(F, L opp)
proof let L be complete antisymmetric (non empty RelStr);
let F be Function-yielding Function;
A1: dom \//(F,L) = dom F & dom /\\(F,L opp) = dom F by FUNCT_2:def 1;
now let x be set; assume x in dom F;
then \//(F,L).x = \\/(F.x,L) & /\\(F,L opp).x = //\(F.x,L opp)
by WAYBEL_5:def 1,def 2;
hence \//(F,L).x = /\\(F,L opp).x by Th49;
end;
hence \//(F,L) = /\\(F,L opp) by A1,FUNCT_1:9;
A2: dom /\\(F,L) = dom F & dom \//(F,L opp) = dom F by FUNCT_2:def 1;
now let x be set; assume x in dom F;
then /\\(F,L).x = //\(F.x,L) & \//(F,L opp).x = \\/(F.x,L opp)
by WAYBEL_5:def 1,def 2;
hence /\\(F,L).x = \//(F,L opp).x by Th49;
end;
hence /\\(F,L) = \//(F,L opp) by A2,FUNCT_1:9;
end;
definition
cluster completely-distributive -> complete (non empty RelStr);
coherence by WAYBEL_5:def 3;
end;
definition
cluster completely-distributive trivial strict (non empty Poset);
existence
proof consider R being trivial strict (non empty Poset);
take R; thus thesis;
end;
end;
theorem
for L being non empty Poset holds
L is completely-distributive iff L opp is completely-distributive
proof let L be non empty Poset;
thus L is completely-distributive implies L opp is completely-distributive
proof assume L is completely-distributive;
then A1: L is completely-distributive (non empty Poset);
hence L opp is complete by Th17;
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, L opp;
reconsider G = F as DoubleIndexedSet of K, L by Th46;
thus Inf Sups F
= \\/(Sups F, L) by A1,Th49
.= Sup Infs G by A1,Th50
.= Inf Sups Frege G by A1,Th48
.= //\(Infs Frege F, L) by A1,Th50
.= Sup Infs Frege F by A1,Th49;
end;
assume L opp is completely-distributive;
then A2: L opp is completely-distributive (non empty Poset);
then A3: L is complete (non empty Poset) by Th17;
thus L is complete by A2,Th17;
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, L;
reconsider G = F as DoubleIndexedSet of K, L opp by Th46;
thus Inf Sups F
= \\/(Sups F, L opp) by A3,Th49
.= Sup Infs G by A3,Th50
.= Inf Sups Frege G by A2,Th48
.= //\(Infs Frege F, L opp) by A3,Th50
.= Sup Infs Frege F by A3,Th49;
end;