:: Duality in Relation Structures
:: by Grzegorz Bancerek
::
:: Received November 12, 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 ORDERS_2, ARYTM_0, RELAT_1, SUBSET_1, XXREAL_0, XBOOLE_0,
RELAT_2, STRUCT_0, LATTICE3, YELLOW_0, EQREL_1, LATTICES, REWRITE1,
WAYBEL_0, TARSKI, FINSET_1, XXREAL_2, XBOOLEAN, FUNCT_1, CAT_1, WELLORD1,
SEQM_3, WAYBEL_1, PBOOLE, WAYBEL_5, FUNCT_6, FUNCOP_1, FINSEQ_4,
YELLOW_2, ORDINAL2, CARD_3, YELLOW_7, CARD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1,
FUNCT_2, FINSET_1, CARD_3, FUNCT_6, PRALG_1, PBOOLE, FUNCOP_1, STRUCT_0,
ORDERS_2, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_5;
constructors DOMAIN_1, LATTICE3, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1,
WAYBEL_5, RELSET_1;
registrations RELSET_1, FUNCOP_1, FINSET_1, CARD_3, PBOOLE, STRUCT_0,
LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_5, FUNCT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_2, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1,
WAYBEL_5, XBOOLE_0;
equalities LATTICE3, YELLOW_0, WAYBEL_0, XBOOLE_0, FUNCT_6;
expansions RELAT_2, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_1;
theorems RELAT_1, FUNCT_1, FUNCT_2, CARD_3, ORDERS_2, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_2, WAYBEL_1, WAYBEL_5, PBOOLE, FUNCT_6, FUNCOP_1,
PRALG_2, YELLOW_5, PRALG_1, XBOOLE_0, FUNCT_5, PARTFUN1;
schemes CLASSES1, FUNCT_2;
begin
notation
let L be RelStr;
synonym L opp for L~;
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 & (~y)~ = ~y;
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~;
hence thesis by Th1;
end;
theorem
for L being RelStr holds L is empty iff L opp is empty;
theorem Th4:
for L being RelStr holds L is reflexive iff L opp is reflexive
proof
let L be RelStr;
thus L is reflexive implies L opp is reflexive
proof
assume L is reflexive;
then
A1: the InternalRel of L is_reflexive_in the carrier of L;
let x be object;
assume x in the carrier of L opp;
then [x,x] in the InternalRel of L by A1;
hence thesis by RELAT_1:def 7;
end;
assume L opp is reflexive;
then
A2: the InternalRel of L opp is_reflexive_in the carrier of L opp;
let x be object;
assume x in the carrier of L;
then [x,x] in the InternalRel of L opp by A2;
hence thesis by 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;
hence thesis by A1;
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;
hence thesis by A2;
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;
hence thesis by Th1,A1;
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;
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;
registration
let L be reflexive RelStr;
cluster L opp -> reflexive;
coherence by Th4;
end;
registration
let L be transitive RelStr;
cluster L opp -> transitive;
coherence by Th6;
end;
registration
let L be antisymmetric RelStr;
cluster L opp -> antisymmetric;
coherence by Th5;
end;
registration
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
let L be RelStr, x be Element of L, X be set;
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 a in X;
then (~a)~ = ~a & x <= ~a by A2;
hence thesis by LATTICE3:9;
end;
end;
A3: now
let L be RelStr, x be Element of L, X be set;
assume
A4: x is_>=_than X;
thus x~ is_<=_than X
proof
let a be Element of L opp;
assume a in X;
then (~a)~ = ~a & x >= ~a by A4;
hence thesis by LATTICE3:9;
end;
end;
x~~ is_<=_than X implies x is_<=_than X by YELLOW_0:2;
hence x is_<=_than X iff x~ is_>=_than X by A1,A3;
x~~ is_>=_than X implies x is_>=_than X by YELLOW_0:2;
hence thesis by A1,A3;
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;
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;
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;
hence b <= a~ by Th2,A2;
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;
hence b >= ~c by Th2,A5;
end;
hence thesis by A3,A4;
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;
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;
hence b >= ~a by Th2,A7;
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;
hence b <= c~ by Th2,A10;
end;
hence thesis by A8,A9;
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;
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
A1: ex_sup_of X,L or ex_inf_of X,L opp;
then
A2: ex_sup_of X,L by Th10;
then "\/"(X,L) is_>=_than X by YELLOW_0:def 9;
then
A3: "\/"(X,L)~ is_<=_than X by Th8;
A4: 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 A2,YELLOW_0:def 9;
hence x <= "\/"(X,L)~ by Th2;
end;
ex_inf_of X,L opp by A1,Th10;
hence thesis by A3,A4,YELLOW_0:def 10;
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
A1: ex_inf_of X,L or ex_sup_of X,L opp;
then
A2: ex_inf_of X,L by Th11;
then "/\"(X,L) is_<=_than X by YELLOW_0:def 10;
then
A3: "/\"(X,L)~ is_>=_than X by Th8;
A4: 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 A2,YELLOW_0:def 10;
hence x >= "/\"(X,L)~ by Th2;
end;
ex_sup_of X,L opp by A1,Th11;
hence thesis by A3,A4,YELLOW_0:def 9;
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 z9 being Element of L1 st z9 <= x & z9 <= y holds z9 <= 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 z9 being Element of L1 st z9 <= x & z9 <= y holds z9 <= z by A2;
reconsider c = z as Element of L2 by A1;
take c;
thus c <= a & c <= b by A1,A3;
let d be Element of L2;
reconsider z9 = d as Element of L1 by A1;
assume d <= a & d <= b;
then z9 <= x & z9 <= y by A1;
then z9 <= z by A4;
hence thesis by A1;
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 z9 being Element of L1 st z9 >= x & z9 >= y holds z9 >= 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 z9 being Element of L1 st z9 >= x & z9 >= y holds z9 >= z by A2;
reconsider c = z as Element of L2 by A1;
take c;
thus c >= a & c >= b by A1,A3;
let d be Element of L2;
reconsider z9 = d as Element of L1 by A1;
assume d >= a & d >= b;
then z9 >= x & z9 >= y by A1;
then z9 >= z by A4;
hence thesis by A1;
end;
theorem Th16:
for L being RelStr holds L is with_infima iff L opp is with_suprema
proof
let L be RelStr;
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
let L be non empty RelStr;
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 and
A4: for b being Element of L st Y is_<=_than b holds a <= b by A2;
take x = a~;
thus X is_<=_than x
proof
let y be Element of L opp;
assume
A5: y in X;
Y is_<=_than ~y
proof
let b be Element of L;
assume b in Y;
then ex z being Element of L st b = z & z is_<=_than X;
hence thesis by A5;
end;
hence thesis by Th2,A4;
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
A6: a >= ~y by A3;
~x = x;
hence thesis by A6,Th1;
end;
end;
L opp~ is complete implies L is complete by YELLOW_0:3;
hence thesis by A1;
end;
registration
let L be with_infima RelStr;
cluster L opp -> with_suprema;
coherence by Th16;
end;
registration
let L be with_suprema RelStr;
cluster L opp -> with_infima;
coherence by LATTICE3:10;
end;
registration
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;
thus fininfs X c= finsups Y
proof
let x be object;
assume x in fininfs X;
then consider Z being finite Subset of X such that
A2: x = "/\"(Z,L) & ex_inf_of Z,L;
x = "\/"(Z,L opp) & ex_sup_of Z, L opp by A2,Th11,Th13;
hence thesis by A1;
end;
thus finsups Y c= fininfs X
proof
let x be object;
assume x in finsups Y;
then consider Z being finite Subset of Y such that
A3: x = "\/"(Z,L opp) & ex_sup_of Z,L opp;
x = "/\"(Z,L) & ex_inf_of Z, L by A3,Th11,Th13;
hence thesis by A1;
end;
thus finsups X c= fininfs Y
proof
let x be object;
assume x in finsups X;
then consider Z being finite Subset of X such that
A4: x = "\/"(Z,L) & ex_sup_of Z,L;
x = "/\"(Z,L opp) & ex_inf_of Z, L opp by A4,Th10,Th12;
hence thesis by A1;
end;
let x be object;
assume x in fininfs Y;
then consider Z being finite Subset of Y such that
A5: x = "/\"(Z,L opp) & ex_inf_of Z,L opp;
x = "\/"(Z,L) & ex_sup_of Z, L by A5,Th10,Th12;
hence thesis by A1;
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 object;
assume
A2: x in downarrow X;
then reconsider x as Element of L;
consider y being Element of L such that
A3: y >= x and
A4: y in X by A2,WAYBEL_0:def 15;
y~ <= x~ by A3,LATTICE3:9;
hence thesis by A1,A4,WAYBEL_0:def 16;
end;
thus uparrow Y c= downarrow X
proof
let x be object;
assume
A5: x in uparrow Y;
then reconsider x as Element of L opp;
consider y being Element of L opp such that
A6: y <= x and
A7: y in Y by A5,WAYBEL_0:def 16;
~y >= ~x by A6,Th1;
hence thesis by A1,A7,WAYBEL_0:def 15;
end;
thus uparrow X c= downarrow Y
proof
let x be object;
assume
A8: x in uparrow X;
then reconsider x as Element of L;
consider y being Element of L such that
A9: y <= x and
A10: y in X by A8,WAYBEL_0:def 16;
y~ >= x~ by A9,LATTICE3:9;
hence thesis by A1,A10,WAYBEL_0:def 15;
end;
let x be object;
assume
A11: x in downarrow Y;
then reconsider x as Element of L opp;
consider y being Element of L opp such that
A12: y >= x and
A13: y in Y by A11,WAYBEL_0:def 15;
~y <= ~x by A12,Th1;
hence thesis by A1,A13,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 by
Th19;
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 <= y by YELLOW_0:23;
then
A1: (x"/\"y)~ >= y~ by LATTICE3:9;
A2: ~(x~) = x~ & ~(y~) = y~;
A3: now
let d be Element of L opp;
assume d >= x~ & d >= y~;
then ~d <= x & ~d <= y by A2,Th1;
then
A4: ~d <= x"/\"y by YELLOW_0:23;
(~d)~ = ~d;
hence (x"/\"y)~ <= d by A4,LATTICE3:9;
end;
x"/\"y <= x by YELLOW_0:23;
then (x"/\"y)~ >= x~ by LATTICE3:9;
hence thesis by A1,A3,YELLOW_0:22;
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 & (~y)~ = ~y;
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 >= y by YELLOW_0:22;
then
A1: (x"\/"y)~ <= y~ by LATTICE3:9;
A2: ~(x~) = x~ & ~(y~) = y~;
A3: now
let d be Element of L opp;
assume d <= x~ & d <= y~;
then ~d >= x & ~d >= y by A2,Th1;
then
A4: ~d >= x"\/"y by YELLOW_0:22;
(~d)~ = ~d;
hence (x"\/"y)~ >= d by A4,LATTICE3:9;
end;
x"\/"y >= x by YELLOW_0:22;
then (x"\/"y)~ <= x~ by LATTICE3:9;
hence thesis by A1,A3,YELLOW_0:23;
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 & (~y)~ = ~y;
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;
thus x "/\" (y "\/" z) = (~x)"\/"~(y "\/" z) by Th24
.= (~x)"\/"((~y)"/\"~z) by Th22
.= ((~x)"\/"(~y))"/\"((~x)"\/"~z) by A1,WAYBEL_1:5
.= (~(x"/\"y))"/\"((~x)"\/"~z) by Th24
.= (~(x"/\"y))"/\"~(x"/\"z) by Th24
.= (x "/\" y) "\/" (x "/\" z) by Th22;
end;
end;
assume
A2: L opp is distributive;
let x,y,z be Element of L;
thus x "/\" (y "\/" z) = (x~)"\/"((y "\/" z)~) by Th21
.= (x~)"\/"((y~)"/\"(z~)) by Th23
.= ((x~)"\/"(y~))"/\"((x~)"\/"(z~)) by A2,WAYBEL_1:5
.= ((x"/\"y)~)"/\"((x~)"\/"(z~)) by Th21
.= ((x"/\"y)~)"/\"((x"/\"z)~) by Th21
.= (x "/\" y) "\/" (x "/\" z) by Th23;
end;
registration
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;
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;
Y is filtered
proof
let x,y be Element of L opp;
assume x in Y & y in Y;
then consider z being Element of L such that
A1: z in X & z >= ~x & z >= ~y by WAYBEL_0:def 1;
take z~;
~(z~) = z~;
hence thesis by A1,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;
Y is directed
proof
let x,y be Element of L;
assume x in Y & y in Y;
then consider z being Element of L opp such that
A2: z in X & z <= x~ & z <= y~ by WAYBEL_0:def 2;
take ~z;
(~z)~ = ~z;
hence thesis by A2,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;
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;
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;
Y is upper
proof
let x,y be Element of L opp;
assume that
A1: x in Y and
A2: x <= y;
~x >= ~y by A2,Th1;
hence thesis by A1,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;
Y is lower
proof
let x,y be Element of L;
assume that
A3: x in Y and
A4: x >= y;
x~ <= y~ by A4,LATTICE3:9;
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;
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;
thus L is lower-bounded implies L opp is upper-bounded
proof
given x being Element of L such that
A1: x is_<=_than the carrier of L;
take x~;
thus thesis by A1,Th8;
end;
given x being Element of L opp such that
A2: x is_>=_than the carrier of L opp;
take ~x;
thus thesis by A2,Th9;
end;
theorem Th31:
for L being RelStr holds L opp is lower-bounded iff L is upper-bounded
proof
let L be RelStr;
thus L opp is lower-bounded implies L is upper-bounded
proof
given x being Element of L opp such that
A1: x is_<=_than the carrier of L opp;
take ~x;
thus thesis by A1,Th9;
end;
given x being Element of L such that
A2: x is_>=_than the carrier of L;
take x~;
thus thesis by A2,Th8;
end;
theorem
for L being RelStr holds L is bounded iff L opp is bounded
by Th30,Th31;
theorem
for L being lower-bounded antisymmetric non empty RelStr holds (Bottom
L)~ = Top (L opp) & ~Top (L opp) = Bottom L by Th12,YELLOW_0:42;
theorem
for L being upper-bounded antisymmetric non empty RelStr holds (Top L)
~ = Bottom (L opp) & ~Bottom (L opp) = Top L by Th13,YELLOW_0:43;
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
A1: y is_a_complement_of x;
then
A2: (x~)"\/"(y~) = (Bottom L)~ by Th21
.= Top (L opp) by Th12,YELLOW_0:42;
(x~)"/\"(y~) = (Top L)~ by Th23,A1
.= Bottom (L opp) by Th13,YELLOW_0:43;
hence y~ is_a_complement_of x~ by A2;
end;
assume that
A3: (x~)"\/"(y~) = Top (L opp) and
A4: (x~)"/\"(y~) = Bottom (L opp);
thus x "\/" y = (x~)"/\"(y~) by Th23
.= Top L by A4,Th13,YELLOW_0:43;
thus x "/\" y = (x~)"\/"(y~) by Th21
.= Bottom L by A3,Th12,YELLOW_0:42;
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;
hence thesis 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;
hence thesis by A4,Th35;
end;
registration
let L be lower-bounded RelStr;
cluster L opp -> upper-bounded;
coherence by Th30;
end;
registration
let L be upper-bounded RelStr;
cluster L opp -> lower-bounded;
coherence by Th31;
end;
registration
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:87;
then 'not' x is_a_complement_of x by WAYBEL_1:86;
then ('not' x)~ is_a_complement_of x~ by Th35;
hence thesis by YELLOW_5:11;
end;
definition
let L be non empty RelStr;
func ComplMap L -> Function 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 Function of L,L such that
A1: for x being Element of L holds f.x = N(x) from FUNCT_2:sch 4;
reconsider f as Function of L,L opp;
take f;
thus thesis by A1;
end;
correctness
proof
let f1,f2 be Function 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,FUNCT_2:63;
end;
end;
registration
let L be Boolean LATTICE;
cluster ComplMap L -> one-to-one;
coherence
proof
let a,b be Element of L;
set f = ComplMap L;
A1: 'not' 'not' a = a by WAYBEL_1:87;
f.a = 'not' a & f.b = 'not' b by Def1;
hence thesis by A1,WAYBEL_1:87;
end;
end;
registration
let L be Boolean LATTICE;
cluster ComplMap L -> isomorphic;
coherence
proof
set f = ComplMap L;
A1: dom f = the carrier of L by FUNCT_2:def 1;
A2: rng f = the carrier of L opp
proof
thus rng f c= the carrier of L opp;
let x be object;
assume x in the carrier of L opp;
then reconsider x as Element of L;
x = 'not' 'not' x by WAYBEL_1:87;
then f.'not' x = x by Def1;
hence thesis by A1,FUNCT_1:def 3;
end;
now
let x,y be Element of L;
f.x = ('not' x)~ & f.y = ('not' y)~ by Def1;
then
A3: 'not' x >= 'not' y iff f.x <= f.y by LATTICE3:9;
x = 'not' 'not' x & y = 'not' 'not' y by WAYBEL_1:87;
hence x <= y iff f.x <= f.y by A3,WAYBEL_1:83;
end;
hence thesis by A2,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 Function of S,T
iff f is Function of S opp,T) & (f is Function of S,T iff f is Function of S,T
opp) & (f is Function of S,T iff f is Function of S opp,T opp);
theorem
for S,T being non empty RelStr
for f being Function of S,T, g being Function 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 Function of S,T, g be Function 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
A3: f.x <= f.y by A2;
(f.x)~ = f.x & (f.y)~ = f.y;
hence thesis by A1,A3,LATTICE3:9;
end;
thus g is antitone implies f is monotone
proof
assume
A4: 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
A5: g.y <= g.x by A4;
~(g.x) = g.x & ~(g.y) = g.y;
hence thesis by A1,A5,Th1;
end;
thus f is antitone implies g is monotone
proof
assume
A6: 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
A7: f.y <= f.x by A6;
(f.x)~ = f.x & (f.y)~ = f.y;
hence thesis by A1,A7,LATTICE3:9;
end;
thus g is monotone implies f is antitone
proof
assume
A8: 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
A9: g.y >= g.x by A8;
~(g.x) = g.x & ~(g.y) = g.y;
hence thesis by A1,A9,Th1;
end;
end;
theorem
for S,T being non empty RelStr for f being Function of S,T opp, g
being Function 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 Function of S,T~, g be Function 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
A3: f.~y <= f.~x by A2;
~(f.~x) = f.~x & ~(f.~y) = f.~y;
hence thesis by A1,A3,Th1;
end;
thus g is monotone implies f is monotone
proof
assume
A4: 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
A5: g.(y~) <= g.(x~) by A4;
(g.(x~))~ = g.(x~) & (g.(y~))~ = g.(y~);
hence thesis by A1,A5,LATTICE3:9;
end;
thus f is antitone implies g is antitone
proof
assume
A6: 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
A7: f.~y >= f.~x by A6;
~(f.~x) = f.~x & ~(f.~y) = f.~y;
hence thesis by A1,A7,Th1;
end;
thus g is antitone implies f is antitone
proof
assume
A8: 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
A9: g.(y~) >= g.(x~) by A8;
(g.(x~))~ = g.(x~) & (g.(y~))~ = g.(y~);
hence thesis by A1,A9,LATTICE3:9;
end;
end;
theorem Th42:
for S,T being non empty RelStr for f being Function of S,T, g
being Function 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 Function of S,T, g be Function 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
A3: f.~y <= f.~x by A2;
(f.~x)~ = f.~x & (f.~y)~ = f.~y;
hence thesis by A1,A3,LATTICE3:9;
end;
thus g is monotone implies f is monotone
proof
assume
A4: 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
A5: g.(y~) <= g.(x~) by A4;
~(g.(x~)) = g.(x~) & ~(g.(y~)) = g.(y~);
hence thesis by A1,A5,Th1;
end;
thus f is antitone implies g is antitone
proof
assume
A6: 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
A7: f.~y >= f.~x by A6;
(f.~x)~ = f.~x & (f.~y)~ = f.~y;
hence thesis by A1,A7,LATTICE3:9;
end;
thus g is antitone implies f is antitone
proof
assume
A8: 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
A9: g.(y~) >= g.(x~) by A8;
~(g.(x~)) = g.(x~) & ~(g.(y~)) = g.(y~);
hence thesis by A1,A9,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: 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 Function of S,T, g being Function of T,S such that
A3: a = [f,g] by WAYBEL_1:def 9;
reconsider g as Function of T1,S1 by A2;
reconsider f as Function of S1,T1 by A2;
a = [f,g] by A3;
hence a is Connection of S1,T1;
end;
S~ = RelStr(#the carrier of S, (the InternalRel of S)~#) & T~ = RelStr(#
the carrier of T, (the InternalRel of T)~#);
hence thesis by A1;
end;
theorem
for S,T being non empty Poset
for f1 being Function of S,T, g1 being Function of T,S
for f2 being Function of S~,T~, g2 being Function 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 Function of S,T, g1 be Function of T,S;
let f2 be Function of S~,T~, g2 be Function of T~,S~ such that
A1: f1 = f2 and
A2: g1 = g2;
hereby
assume
A3: [f1,g1] is Galois;
then f1 is monotone by WAYBEL_1:8;
then
A4: f2 is monotone by A1,Th42;
A5: now
let s be Element of S~, t be Element of T~;
A6: (f1.~s)~ = f1.~s & (g1.~t)~ = g1.~t;
~t <= f1.~s iff g1.~t <= ~s by A3,WAYBEL_1:8;
hence g2.t >= s iff t >= f2.s by A1,A2,A6,Th2;
end;
g1 is monotone by A3,WAYBEL_1:8;
then g2 is monotone by A2,Th42;
hence [g2,f2] is Galois by A4,A5;
end;
assume
A7: [g2,f2] is Galois;
then f2 is monotone by WAYBEL_1:8;
then
A8: f1 is monotone by A1,Th42;
A9: now
let t be Element of T, s be Element of S;
A10: ~(f2.(s~)) = f2.(s~) & ~(g2.(t~)) = g2.(t~);
s~ <= g2.(t~) iff f2.(s~) <= t~ by A7,WAYBEL_1:8;
hence t <= f1.s iff g1.t <= s by A1,A2,A10,Th2;
end;
g2 is monotone by A7,WAYBEL_1:8;
then g1 is monotone by A2,Th42;
hence thesis by A8,A9;
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 doms F = dom F by FUNCT_6:def 2;
A2: dom F = J by PARTFUN1:def 2;
A3: now
let j be object;
set f = F.j;
assume
A4: j in J;
then (J --> D).j = D by FUNCOP_1:7;
then
A5: f is Function of K.j,D by A4,PBOOLE:def 15;
(doms F).j = dom f by A2,A4,FUNCT_6:22;
hence (doms F).j = K.j by A5,FUNCT_2:def 1;
end;
dom K = J & F"rng F = dom F by PARTFUN1:def 2,RELAT_1:134;
hence thesis by A2,A1,A3,FUNCT_1:2;
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; :: redefines .. (FUNCT_6, definition)
coherence
proof
dom (F.j) = K.j & dom F = J by FUNCT_2:def 1,PARTFUN1:def 2;
then F..(j,k) = (F.j).k by FUNCT_5:38;
hence thesis;
end;
end;
theorem
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;
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
reconsider J9 = product doms F as non empty set;
let y be Element of L;
reconsider K9 = J9 --> J as ManySortedSet of J9;
reconsider G = Frege F as DoubleIndexedSet of K9, L;
assume y in rng Sups Frege F;
then consider f being Element of J9 such that
A3: y = Sup (G.f) by WAYBEL_5:14;
reconsider f as Element of product doms F;
A4: dom F = J & dom Frege F = product doms F by PARTFUN1:def 2;
then f.a in dom (F.a) by WAYBEL_5:9;
then reconsider j = f.a as Element of K.a;
A5: (F.a).j in rng ((Frege F).f) by A4,WAYBEL_5:9;
j in dom (F.a) by A4,WAYBEL_5:9;
then (F.a).j in rng (F.a) by FUNCT_1:def 3;
then
A6: x <= (F.a).j by A2,YELLOW_2:22;
y = sup rng ((Frege F).f) by A3,YELLOW_2:def 5;
then (F.a).j <= y by A5,YELLOW_2:22;
hence x <= y by A6,ORDERS_2:3;
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: Inf Sups Frege F = Sup Infs Frege Frege F by A1;
A3: dom K = J by PARTFUN1:def 2;
A4: doms Frege F = (product doms F) --> J by Th45;
A6: doms F = K by Th45;
rng Infs Frege Frege F is_<=_than Sup Infs F
proof
reconsider J9 = product doms Frege F as non empty set;
let a be Element of L;
reconsider K9 = J9 --> product doms F as ManySortedSet of J9;
reconsider G = Frege Frege F as DoubleIndexedSet of K9, L;
assume a in rng Infs Frege Frege F;
then consider g being Element of J9 such that
A8: a = Inf (G.g) by WAYBEL_5:14;
reconsider g9 = g as Function;
deffunc XX(object) =
{f.(g9.f) where f is Element of product doms F: g9.f = $1};
A9: dom ((product doms F) --> J) = product doms F;
now
defpred P[object,object] means $2 in (K.$1) \ XX($1);
assume
A10: for j being Element of J holds (K.j) \ XX(j) <> {};
A11: now
let j be object;
assume j in J;
then reconsider i = j as Element of J;
set k = the Element of (K.i)\XX(j);
(K.i)\XX(i) <> {} by A10;
then k in (K.i)\XX(i);
hence ex k being object st P[j,k];
end;
consider h being Function such that
A12: dom h = J & for j being object st j in J holds P[j,h.j] from
CLASSES1:sch 1(A11);
now
let j be object;
assume j in J;
then h.j in (K.j) \ XX(j) by A12;
hence h.j in (doms F).j by A6;
end;
then reconsider h as Element of product doms F by A6,A3,A12,CARD_3:9;
g9.h in (doms Frege F).h by A4,A9,CARD_3:9;
then reconsider j = g9.h as Element of J by A4;
h.(g9.h) in XX(j) & h.j in (K.j) \ XX(j) by A12;
hence contradiction by XBOOLE_0:def 5;
end;
then consider j being Element of J such that
A13: (K.j) \ XX(j) = {};
A14: rng (F.j) c= rng (G.g)
proof
let z be object;
assume z in rng (F.j);
then consider u being object such that
A15: u in dom (F.j) and
A16: z = (F.j).u by FUNCT_1:def 3;
reconsider u as Element of K.j by A15;
u in XX(j) by A13,XBOOLE_0:def 5;
then consider f being Element of product doms F such that
A17: u = f.(g9.f) and
A18: g9.f = j;
A: G.g = (Frege F)..g9 & (Frege F).f = F..f by PRALG_2:def 2;
consider gg being Function such that
BB: f = gg & dom gg = dom doms F &
for y being object st y in dom doms F holds gg.y in (doms F).y
by CARD_3:def 5;
A25: dom F = J by PARTFUN1:def 2;
BC: dom f = dom F by FUNCT_6:def 2,BB;
j in dom F /\ dom f by A25,BC; then
j in dom (F..f) by PRALG_1:def 19; then
WW: (F..f).j = (F.j).(f.j) by PRALG_1:def 19;
A27: dom Frege F = product doms F by PARTFUN1:def 2;
consider gg1 being Function such that
BB: g = gg1 & dom gg1 = dom doms Frege F &
for y being object st y in dom doms Frege F holds
gg1.y in (doms Frege F).y by CARD_3:def 5;
f in dom Frege F by A27; then
f in dom doms Frege F by FUNCT_6:def 2; then
f in dom Frege F /\ dom g9 by A27,BB,XBOOLE_0:def 4; then
f in dom ((Frege F)..g9) by PRALG_1:def 19;
then (G.g).f = (F..f).j by A18,PRALG_1:def 19,A; then
A19: (G.g).f = z by A16,A17,A18,WW;
dom (G.g) = K9.g & K9.g = product doms F by FUNCT_2:def 1;
hence thesis by A19,FUNCT_1:def 3;
end;
ex_inf_of rng (G.g), L & ex_inf_of rng (F.j),L by YELLOW_0:17;
then inf rng (G.g) <= inf rng (F.j) by A14,YELLOW_0:35;
then a <= inf rng (F.j) by A8,YELLOW_2:def 6;
then
A20: a <= Inf (F.j) by YELLOW_2:def 6;
Inf (F.j) in rng Infs F by WAYBEL_5:14;
then Inf (F.j) <= sup rng Infs F by YELLOW_2:22;
then a <= sup rng Infs F by A20,ORDERS_2:3;
hence thesis by YELLOW_2:def 5;
end;
then sup rng Infs Frege Frege F <= Sup Infs F by YELLOW_0:32;
then
A21: Sup Infs Frege Frege F <= Sup Infs F by YELLOW_2:def 5;
Sup Infs F <= Inf Sups Frege F by Th47;
hence thesis by A2,A21,ORDERS_2:2;
end;
assume
A22: 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;
A23: dom K = J by PARTFUN1:def 2;
A24: doms Frege F = (product doms F) --> J by Th45;
A25: dom F = J by PARTFUN1:def 2;
A26: doms F = K by Th45;
A27: dom Frege F = product doms F by PARTFUN1:def 2;
rng Sups Frege Frege F is_>=_than Inf Sups F
proof
reconsider J9 = product doms Frege F as non empty set;
let a be Element of L;
reconsider K9 = J9 --> product doms F as ManySortedSet of J9;
reconsider G = Frege Frege F as DoubleIndexedSet of K9, L;
assume a in rng Sups Frege Frege F;
then consider g being Element of J9 such that
A28: a = Sup (G.g) by WAYBEL_5:14;
reconsider g9 = g as Function;
deffunc XX(object) =
{f.(g9.f) where f is Element of product doms F: g9.f = $1};
A29: dom ((product doms F) --> J) = product doms F;
now
defpred P[object,object] means $2 in (K.$1) \ XX($1);
assume
A30: for j being Element of J holds (K.j) \ XX(j) <> {};
A31: now
let j be object;
assume j in J;
then reconsider i = j as Element of J;
set k = the Element of (K.i)\XX(j);
(K.i)\XX(i) <> {} by A30;
then k in (K.i)\XX(i);
hence ex k being object st P[j,k];
end;
consider h being Function such that
A32: dom h = J & for j being object st j in J holds P[j,h.j] from
CLASSES1:sch 1(A31);
now
let j be object;
assume j in J;
then h.j in (K.j) \ XX(j) by A32;
hence h.j in (doms F).j by A26;
end;
then reconsider h as Element of product doms F by A26,A23,A32,CARD_3:9;
g9.h in (doms Frege F).h by A24,A29,CARD_3:9;
then reconsider j = g9.h as Element of J by A24;
h.(g9.h) in XX(j) & h.j in (K.j) \ XX(j) by A32;
hence contradiction by XBOOLE_0:def 5;
end;
then consider j being Element of J such that
A33: (K.j) \ XX(j) = {};
A34: rng (F.j) c= rng (G.g)
proof
let z be object;
assume z in rng (F.j);
then consider u being object such that
A35: u in dom (F.j) and
A36: z = (F.j).u by FUNCT_1:def 3;
reconsider u as Element of K.j by A35;
u in XX(j) by A33,XBOOLE_0:def 5;
then consider f being Element of product doms F such that
A37: u = f.(g9.f) and
A38: g9.f = j;
a37: G.g = (Frege F)..g9 & (Frege F).f = F..f by PRALG_2:def 2;
consider gg being Function such that
BB: f = gg & dom gg = dom doms F &
for y being object st y in dom doms F holds gg.y in (doms F).y
by CARD_3:def 5;
dom F = dom f by BB,FUNCT_6:def 2; then
j in dom F /\ dom f by A25; then
Z1: j in dom (F..f) by PRALG_1:def 19;
consider gg1 being Function such that
BB: g = gg1 & dom gg1 = dom doms Frege F &
for y being object st y in dom doms Frege F holds
gg1.y in (doms Frege F).y by CARD_3:def 5;
f in dom Frege F by A27; then
f in dom g9 by BB,FUNCT_6:def 2; then
f in dom (Frege F) /\ dom g9 by A27,XBOOLE_0:def 4; then
a38: f in dom ((Frege F)..g9) by PRALG_1:def 19;
(G.g).f = ((Frege F).f).(g9.f) by a37,a38,PRALG_1:def 19; then
A39: (G.g).f = z by Z1,A36,a37,A37,A38,PRALG_1:def 19;
dom (G.g) = K9.g & K9.g = product doms F by FUNCT_2:def 1;
hence thesis by A39,FUNCT_1:def 3;
end;
ex_sup_of rng (G.g), L & ex_sup_of rng (F.j),L by YELLOW_0:17;
then sup rng (G.g) >= sup rng (F.j) by A34,YELLOW_0:34;
then a >= sup rng (F.j) by A28,YELLOW_2:def 5;
then
A40: a >= Sup (F.j) by YELLOW_2:def 5;
Sup (F.j) in rng Sups F by WAYBEL_5:14;
then Sup (F.j) >= inf rng Sups F by YELLOW_2:22;
then a >= inf rng Sups F by A40,ORDERS_2:3;
hence thesis by YELLOW_2:def 6;
end;
then inf rng Sups Frege Frege F >= Inf Sups F by YELLOW_0:33;
then
A41: Inf Sups Frege Frege F >= Inf Sups F by YELLOW_2:def 6;
Inf Sups F >= Sup Infs Frege F & Sup Infs Frege F = Inf Sups Frege
Frege F by A22,WAYBEL_5:16;
hence thesis by A41,ORDERS_2:2;
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;
thus \\/(F, L) = "\/"(rng F, L) by YELLOW_2:def 5
.= "/\"(rng F, L opp) by YELLOW_0:17,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 YELLOW_0:17,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: now
let x be object;
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;
dom \//(F,L) = dom F & dom /\\(F,L opp) = dom F by FUNCT_2:def 1;
hence \//(F,L) = /\\(F,L opp) by A1,FUNCT_1:2;
A2: now
let x be object;
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;
dom /\\(F,L) = dom F & dom \//(F,L opp) = dom F by FUNCT_2:def 1;
hence thesis by A2,FUNCT_1:2;
end;
registration
cluster completely-distributive -> complete for non empty RelStr;
coherence by WAYBEL_5:def 3;
end;
registration
cluster completely-distributive strict for 1-element Poset;
existence
proof
set R = the 1-element strict 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
A1: L is completely-distributive;
hence L opp is complete;
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;
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
A2: L opp is completely-distributive;
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;
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;