:: Quantales
:: by Grzegorz Bancerek
::
:: Received May 9, 1994
:: Copyright (c) 1994-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, SUBSET_1, TARSKI, LATTICES, STRUCT_0, ALGSTR_0,
EQREL_1, PBOOLE, LATTICE3, BINOP_1, FUNCT_1, WAYBEL_0, FINSET_1, RELAT_1,
VECTSP_1, FINSEQ_1, GROUP_1, REWRITE1, SETWISEO, ZFMISC_1, SEQM_3,
GRAPH_1, FUNCT_3, SETFAM_1, QUANTAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1,
SETWISEO, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, FINSET_1,
DOMAIN_1, LATTICES, LATTICE3, MONOID_0;
constructors SETFAM_1, BINOP_1, DOMAIN_1, SETWISEO, VECTSP_1, LATTICE3,
RELSET_1, GROUP_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
STRUCT_0, LATTICES, LATTICE3, ALGSTR_0, RELSET_1;
requirements BOOLE, SUBSET;
definitions TARSKI, BINOP_1, SETWISEO, LATTICE3, MONOID_0, STRUCT_0, XBOOLE_0;
equalities LATTICES, ALGSTR_0;
expansions BINOP_1, SETWISEO, LATTICES;
theorems TARSKI, ZFMISC_1, BINOP_1, LATTICES, LATTICE3, SETWISEO, MONOID_0,
FUNCT_1, FUNCT_2, RELSET_1, XBOOLE_1, GROUP_1;
schemes FUNCT_2, FRAENKEL;
begin
scheme
DenestFraenkel {A()->non empty set, B()->non empty set, F(set)->set, G(set)
->Element of B(), P[set]}: {F(a) where a is Element of B(): a in {G(b) where b
is Element of A(): P[b]}} = {F(G(a)) where a is Element of A(): P[a]} proof
thus {F(a) where a is Element of B(): a in {G(b) where b is Element of A():
P[b]}} c= {F(G(a)) where a is Element of A(): P[a]}
proof
let x be object;
assume x in {F(a) where a is Element of B(): a in {G(b) where b is
Element of A(): P[b]}};
then consider a being Element of B() such that
A1: x = F(a) and
A2: a in {G(b) where b is Element of A(): P[b]};
ex b being Element of A() st a = G(b) & P[b] by A2;
hence thesis by A1;
end;
let x be object;
assume x in {F(G(a)) where a is Element of A(): P[a]};
then consider a being Element of A() such that
A3: x = F(G(a)) and
A4: P[a];
G(a) in {G(b) where b is Element of A(): P[b]} by A4;
hence thesis by A3;
end;
scheme
EmptyFraenkel {A() -> non empty set, f(set) -> set, P[set]}: {f(a) where a
is Element of A(): P[a]} = {}
provided
A1: not ex a being Element of A() st P[a]
proof
assume not thesis;
then reconsider X = {f(a) where a is Element of A(): P[a]} as non empty set;
set x = the Element of X;
x in X;
then ex a being Element of A() st x = f(a) & P[a];
hence contradiction by A1;
end;
deffunc carr(non empty LattStr) = the carrier of $1;
deffunc join(LattStr) = the L_join of $1;
deffunc met(LattStr) = the L_meet of $1;
deffunc times(multMagma) = the multF of $1;
theorem
for L1,L2 being non empty LattStr st the LattStr of L1 = the
LattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 =
a2 & b1 = b2 holds a1"\/"b1 = a2"\/"b2 & a1"/\"b1 = a2"/\"b2 & (a1 [= b1 iff a2
[= b2);
theorem Th2:
for L1,L2 being non empty LattStr st the LattStr of L1 = the
LattStr of L2 for a being Element of L1, b being Element of L2, X being set st
a = b holds (a is_less_than X iff b is_less_than X) & (a is_greater_than X iff
b is_greater_than X)
proof
let L1,L2 be non empty LattStr such that
A1: the LattStr of L1 = the LattStr of L2;
let a be Element of L1, b be Element of L2, X be set such that
A2: a = b;
thus a is_less_than X implies b is_less_than X
proof
assume
A3: for c being Element of L1 st c in X holds a [= c;
let c be Element of L2;
reconsider d = c as Element of L1 by A1;
assume c in X;
then a [= d by A3;
hence thesis by A1,A2;
end;
thus b is_less_than X implies a is_less_than X
proof
assume
A4: for c being Element of L2 st c in X holds b [= c;
let c be Element of L1;
reconsider d = c as Element of L2 by A1;
assume c in X;
then b [= d by A4;
hence thesis by A1,A2;
end;
thus a is_greater_than X implies b is_greater_than X
proof
assume
A5: for c being Element of L1 st c in X holds c [= a;
let c be Element of L2;
reconsider d = c as Element of L1 by A1;
assume c in X;
then d [= a by A5;
hence thesis by A1,A2;
end;
assume
A6: for c being Element of L2 st c in X holds c [= b;
let c be Element of L1;
reconsider d = c as Element of L2 by A1;
assume c in X;
then d [= b by A6;
hence thesis by A1,A2;
end;
definition
let L be non empty LattStr, X be Subset of L;
attr X is directed means
for Y being finite Subset of X ex x being Element
of L st "\/"(Y, L) [= x & x in X;
end;
theorem
for L being non empty LattStr, X being Subset of L st X is directed
holds X is non empty
proof
let L be non empty LattStr, X be Subset of L;
assume for Y being finite Subset of X ex x being Element of L st "\/"(Y, L)
[= x & x in X;
then ex x being Element of L st "\/"({}X, L) [= x & x in X;
hence thesis;
end;
definition
struct (LattStr, multMagma) QuantaleStr (# carrier -> set, L_join, L_meet,
multF -> BinOp of the carrier #);
end;
registration
cluster non empty for QuantaleStr;
existence
proof
set A = the non empty set,b1 = the BinOp of A;
take QuantaleStr(#A,b1,b1,b1#);
thus the carrier of QuantaleStr(#A,b1,b1,b1#) is non empty;
end;
end;
definition
struct (QuantaleStr, multLoopStr) QuasiNetStr (# carrier -> set, L_join,
L_meet, multF -> (BinOp of the carrier), OneF -> Element of the carrier #);
end;
registration
cluster non empty for QuasiNetStr;
existence
proof
set A = the non empty set,b1 = the (BinOp of A),e = the Element of A;
take QuasiNetStr(#A,b1,b1,b1,e#);
thus the carrier of QuasiNetStr(#A,b1,b1,b1,e#) is non empty;
end;
end;
definition
let IT be non empty multMagma;
attr IT is with_left-zero means
ex a being Element of IT st for b being Element of IT holds a*b = a;
attr IT is with_right-zero means
ex b being Element of IT st for a being Element of IT holds a*b = b;
end;
definition
let IT be non empty multMagma;
attr IT is with_zero means
IT is with_left-zero with_right-zero;
end;
registration
cluster with_zero -> with_left-zero with_right-zero for
non empty multMagma;
coherence;
cluster with_left-zero with_right-zero -> with_zero for
non empty multMagma;
coherence;
end;
registration
cluster with_zero for non empty multMagma;
existence
proof
set x = the set,f = the BinOp of {x};
take G = multMagma(#{x},f#);
reconsider x as Element of G by TARSKI:def 1;
thus G is with_left-zero
proof
take x;
thus thesis by TARSKI:def 1;
end;
take x;
thus thesis by TARSKI:def 1;
end;
end;
definition
let IT be non empty QuantaleStr;
attr IT is right-distributive means
: Def5:
for a being Element of IT, X
being set holds a [*] "\/"(X,IT) = "\/"({a [*] b where b is Element of IT: b in
X},IT);
attr IT is left-distributive means
: Def6:
for a being Element of IT, X
being set holds "\/"(X,IT) [*] a = "\/"({b [*] a where b is Element of IT: b in
X},IT);
attr IT is times-additive means
for a,b,c being Element of IT holds (a"\/"b)
[*]c = (a[*]c)"\/"(b[*]c) & c[*](a"\/"b) = (c[*]a)"\/"(c[*]b);
attr IT is times-continuous means
for X1, X2 being Subset of IT st X1 is
directed & X2 is directed holds ("\/"X1)[*]("\/"X2) = "\/"({a [*] b where a is
Element of IT, b is Element of IT: a in X1 & b in X2},IT);
end;
reserve x,y,z for set;
theorem Th4:
for Q being non empty QuantaleStr st the LattStr of Q = BooleLatt
{} holds Q is associative commutative unital with_zero complete
right-distributive left-distributive Lattice-like
proof
set B = BooleLatt {};
let Q be non empty QuantaleStr;
set a = the Element of Q;
assume
A1: the LattStr of Q = B;
A2: now
let x, y be Element of Q;
A3: carr(B) = {{}} by LATTICE3:def 1,ZFMISC_1:1;
then x = {} by A1,TARSKI:def 1;
hence x = y by A1,A3,TARSKI:def 1;
end;
set o = times(Q);
thus times(Q) is associative
proof
thus for a,b,c being Element of Q holds o.(a,o.(b,c)) = o.(o.(a,b ),c)
by A2;
end;
A4: ( for p,q,r being Element of Q holds p"/\"(q"/\"r) = (p"/\"q)"/\"r)&
for p,q being Element of Q holds p"/\"(p"\/" q) = p by A2;
thus times(Q) is commutative
proof
thus for a,b be Element of Q holds o.(a,b) = o.(b,a) by A2;
end;
thus times(Q) is having_a_unity
proof
take a;
thus a is_a_left_unity_wrt times(Q)
proof
let b be Element of Q;
thus times(Q).(a,b) = b by A2;
end;
let b be Element of Q;
thus times(Q).(b,a) = b by A2;
end;
thus Q is with_zero
proof
thus Q is with_left-zero
proof
take a;
thus thesis by A2;
end;
take a;
thus thesis by A2;
end;
now
let X be set;
consider p being Element of B such that
A5: X is_less_than p and
A6: for r being Element of B st X is_less_than r holds p [= r by
LATTICE3:def 18;
reconsider p9 = p as Element of Q by A1;
take p9;
thus X is_less_than p9 by A1,A5,Th2;
let r9 be Element of Q;
reconsider r = r9 as Element of B by A1;
assume X is_less_than r9;
then X is_less_than r by A1,Th2;
then p [= r by A6;
hence p9 [= r9 by A1;
end;
hence for X being set ex p being Element of Q st X is_less_than p & for r
being Element of Q st X is_less_than r holds p [= r;
thus Q is right-distributive
by A2;
thus Q is left-distributive
by A2;
A7: ( for p,q being Element of Q holds (p"/\"q)"\/" q = q)& for p,q being
Element of Q holds p"/\"q = q"/\"p by A2;
( for p,q being Element of Q holds p"\/"q = q"\/"p)& for p,q,r being
Element of Q holds p"\/"(q"\/"r) = (p"\/"q)"\/"r by A2;
then Q is join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing by A7,A4;
hence thesis;
end;
registration
let A be non empty set, b1,b2,b3 be BinOp of A;
cluster QuantaleStr(#A,b1,b2,b3#) -> non empty;
coherence;
end;
registration
cluster associative commutative unital with_zero left-distributive
right-distributive complete Lattice-like for non empty QuantaleStr;
existence
proof
set B = BooleLatt {};
set b = the BinOp of B;
take QuantaleStr (#carr(B), join(B), met(B), b#);
thus thesis by Th4;
end;
end;
scheme
LUBFraenkelDistr {Q() -> complete Lattice-like non empty QuantaleStr, f(
set, set) -> Element of Q(), X, Y() -> set}: "\/"({"\/"({f(a,b) where b is
Element of Q(): b in Y()},Q()) where a is Element of Q(): a in X()}, Q()) =
"\/"({f(a,b) where a is Element of Q(), b is Element of Q(): a in X() & b in Y(
)}, Q()) proof
set Q = Q(), X = X(), Y = Y();
set Z = {{f(a,b) where b is Element of Q: b in Y} where a is Element of Q: a
in X};
set W = {"\/"V where V is Subset of Q: V in Z};
set S = {f(a,b) where a is Element of Q, b is Element of Q: a in X & b in Y};
A1: W = {"\/"({f(a,b) where b is Element of Q: b in Y}, Q) where a is
Element of Q: a in X}
proof
thus W c= {"\/" ({f(a,b) where b is Element of Q: b in Y}, Q) where a is
Element of Q: a in X}
proof
let x be object;
assume x in W;
then consider V being Subset of Q such that
A2: x = "\/"V and
A3: V in Z;
ex a being Element of Q st V = {f(a,b) where b is Element of Q: b
in Y} & a in X by A3;
hence thesis by A2;
end;
let x be object;
assume x in {"\/"({f(a,b) where b is Element of Q: b in Y}, Q) where a
is Element of Q: a in X};
then consider a being Element of Q such that
A4: x = "\/"({f(a,b) where b is Element of Q: b in Y}, Q) and
A5: a in X;
A6: {f(a,b) where b is Element of Q: b in Y} c= carr(Q)
proof
let y be object;
assume y in {f(a,b) where b is Element of Q: b in Y};
then ex b being Element of Q st y = f(a,b) & b in Y;
hence thesis;
end;
{f(a,c) where c is Element of Q: c in Y} in Z by A5;
hence thesis by A4,A6;
end;
A7: S = union Z
proof
thus S c= union Z
proof
let x be object;
assume x in S;
then consider a, b being Element of Q such that
A8: x = f(a,b) & a in X & b in Y;
x in {f(a,c) where c is Element of Q: c in Y} & {f(a,d) where d is
Element of Q: d in Y} in Z by A8;
hence thesis by TARSKI:def 4;
end;
let x be object;
assume x in union Z;
then consider V being set such that
A9: x in V and
A10: V in Z by TARSKI:def 4;
consider a being Element of Q such that
A11: V = {f(a,b) where b is Element of Q: b in Y} and
A12: a in X by A10;
ex b being Element of Q st x = f(a,b) & b in Y by A9,A11;
hence thesis by A12;
end;
Z c= bool carr(Q)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in Z;
then consider a being Element of Q such that
A13: x = {f(a,b) where b is Element of Q: b in Y} and
a in X;
xx c= carr(Q)
proof
let y be object;
assume y in xx;
then ex b being Element of Q st y = f(a,b) & b in Y by A13;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1,A7,LATTICE3:48;
end;
reserve Q for left-distributive right-distributive complete Lattice-like non
empty QuantaleStr,
a, b, c, d for Element of Q;
theorem Th5:
for Q for X,Y being set holds "\/"(X,Q) [*] "\/"(Y,Q) = "\/"({a
[*] b: a in X & b in Y}, Q)
proof
let Q;
let X,Y be set;
deffunc F(Element of Q) = $1[*]"\/"(Y,Q);
deffunc G(Element of Q) = "\/"({$1[*]b: b in Y}, Q);
defpred P[set] means $1 in X;
deffunc H(Element of Q,Element of Q) = $1[*]$2;
A1: for a holds F(a) = G(a) by Def5;
{F(c): P[c]} = {G(a): P[a]} from FRAENKEL:sch 5(A1);
hence
"\/"(X,Q) [*] "\/"(Y,Q) = "\/"({"\/"({H(a,b) where b is Element of Q: b
in Y}, Q) where a is Element of Q: a in X}, Q) by Def6
.= "\/"({H(c,d) where c is Element of Q, d is Element of Q: c in X & d
in Y}, Q) from LUBFraenkelDistr;
end;
theorem Th6:
(a"\/"b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a"\/"b) = (c
[*] a) "\/" (c [*] b)
proof
set X1 = {d [*] c: d in {a,b}}, X2 = {c [*] d: d in {a,b}};
now
let x be object;
a in {a,b} & b in {a,b} by TARSKI:def 2;
hence x = a [*] c or x = b [*] c implies x in X1;
assume x in X1;
then ex d st x = d [*] c & d in {a,b};
hence x = a [*] c or x = b [*] c by TARSKI:def 2;
end;
then
A1: X1 = {a [*] c, b [*] c} by TARSKI:def 2;
now
let x be object;
a in {a,b} & b in {a,b} by TARSKI:def 2;
hence x = c [*] a or x = c [*] b implies x in X2;
assume x in X2;
then ex d st x = c [*] d & d in {a,b};
hence x = c [*] a or x = c [*] b by TARSKI:def 2;
end;
then
A2: X2 = {c [*] a, c [*] b} by TARSKI:def 2;
A3: a"\/"b = "\/"{a,b} by LATTICE3:43;
then (a"\/"b) [*] c = "\/"(X1, Q) by Def6;
hence (a"\/"b) [*] c = (a [*] c) "\/" (b [*] c) by A1,LATTICE3:43;
c [*] (a"\/"b) = "\/"(X2, Q) by A3,Def5;
hence thesis by A2,LATTICE3:43;
end;
registration
let A be non empty set, b1,b2,b3 be (BinOp of A), e be Element of A;
cluster QuasiNetStr(#A,b1,b2,b3,e#) -> non empty;
coherence;
end;
registration
cluster complete Lattice-like for non empty QuasiNetStr;
existence
proof
set B = BooleLatt {};
set e = the Element of B,b = the BinOp of B;
take QuasiNetStr (#carr(B), join(B), met(B), b, e#);
thus thesis by Th4;
end;
end;
registration
cluster left-distributive right-distributive -> times-continuous
times-additive for complete Lattice-like non empty QuasiNetStr;
coherence
by Th5,Th6;
end;
registration
cluster associative commutative unital with_zero with_left-zero
left-distributive right-distributive complete Lattice-like for non empty
QuasiNetStr;
existence
proof
set B = BooleLatt {};
set e = the Element of B,b = the BinOp of B;
take Q = QuasiNetStr (#carr(B), join(B), met(B), b, e#);
Q is with_zero unital by Th4;
hence thesis by Th4;
end;
end;
definition
mode Quantale is associative left-distributive right-distributive complete
Lattice-like non empty QuantaleStr;
mode QuasiNet is unital associative with_left-zero times-continuous
times-additive complete Lattice-like non empty QuasiNetStr;
end;
definition
mode BlikleNet is with_zero non empty QuasiNet;
end;
theorem
for Q being unital non empty QuasiNetStr st Q is Quantale holds Q is
BlikleNet
proof
defpred P[set] means $1 in {};
let Q be unital non empty QuasiNetStr;
assume Q is Quantale;
then reconsider Q9 = Q as Quantale;
A1: Bottom Q9 = "\/"({},Q9) by LATTICE3:49;
A2: not ex c being Element of Q9 st P[c];
Q9 is with_zero
proof
hereby
reconsider a = Bottom Q9 as Element of Q9;
take a;
let b be Element of Q9;
deffunc F1(Element of Q9) = $1 [*] b;
{F1(c) where c is Element of Q9: P[c]} = {} from EmptyFraenkel(A2 );
hence a[*]b = a by A1,Def6;
end;
take Bottom Q9;
let a be Element of Q9;
deffunc F2(Element of Q9) = a [*] $1;
{F2(c) where c is Element of Q9: P[c]} = {} from EmptyFraenkel(A2);
hence thesis by A1,Def5;
end;
hence thesis;
end;
reserve Q for Quantale,
a,a9,b,b9,c,d,d1,d2,D for Element of Q;
theorem Th8:
a [= b implies a [*] c [= b [*] c & c [*] a [= c [*] b
by Th6;
theorem Th9:
a [= b & c [= d implies a [*] c [= b [*] d
proof
assume a [= b & c [= d;
then a [*] c [= b [*] c & b [*] c [= b [*] d by Th8;
hence thesis by LATTICES:7;
end;
definition
let f be Function;
attr f is idempotent means
f * f = f;
end;
Lm1: for A being non empty set, f being UnOp of A st f is idempotent for a
being Element of A holds f.(f.a) = f.a
by FUNCT_2:15;
definition
let L be non empty LattStr;
let IT be UnOp of L;
attr IT is inflationary means
for p being Element of L holds p [= IT.p;
attr IT is deflationary means
for p being Element of L holds IT.p [= p;
attr IT is monotone means
for p,q being Element of L st p [= q holds IT.p [= IT.q;
attr IT is \/-distributive means
for X being Subset of L holds IT."\/"X [=
"\/"({IT.a where a is Element of L: a in X}, L);
end;
registration
let L be Lattice;
cluster inflationary deflationary monotone for UnOp of L;
existence
proof
reconsider f = id the carrier of L as UnOp of L;
take f;
thus f is inflationary
proof
let p be Element of L;
thus thesis;
end;
thus f is deflationary
proof
let p be Element of L;
thus thesis;
end;
let p,q be Element of L;
thus thesis;
end;
end;
theorem Th10:
for L being complete Lattice, j being UnOp of L st j is monotone
holds j is \/-distributive iff for X being Subset of L holds j."\/"X = "\/"({j.
a where a is Element of L: a in X}, L)
proof
let L be complete Lattice, j be UnOp of L such that
A1: j is monotone;
thus j is \/-distributive implies for X being Subset of L holds j."\/"X =
"\/"({j.a where a is Element of L: a in X}, L)
proof
assume
A2: for X being Subset of L holds j."\/"X [= "\/" ({j.a where a is
Element of L: a in X}, L);
let X be Subset of L;
{j.a where a is Element of L: a in X} is_less_than j. "\/" X
proof
let x be Element of L;
assume x in {j.a where a is Element of L: a in X};
then consider a being Element of L such that
A3: x = j.a and
A4: a in X;
a [= "\/"X by A4,LATTICE3:38;
hence thesis by A1,A3;
end;
then
A5: "\/"({j.a where a is Element of L: a in X}, L) [= j. "\/"X by
LATTICE3:def 21;
j."\/"X [= "\/" ({j.a where a is Element of L: a in X}, L) by A2;
hence thesis by A5,LATTICES:8;
end;
assume
A6: for X being Subset of L holds j."\/"X = "\/"({j.a where a is
Element of L: a in X}, L);
let X be Subset of L;
j."\/"X [= j."\/"X;
hence thesis by A6;
end;
definition
let Q be non empty QuantaleStr;
let IT be UnOp of Q;
attr IT is times-monotone means
for a,b being Element of Q holds IT.a [*] IT .b [= IT.(a [*] b);
end;
definition
let Q be non empty QuantaleStr, a,b be Element of Q;
func a -r> b -> Element of Q equals
"\/"({ c where c is Element of Q: c [*]
a [= b }, Q);
correctness;
func a -l> b -> Element of Q equals
"\/"({ c where c is Element of Q: a [*]
c [= b }, Q);
correctness;
end;
theorem Th11:
a [*] b [= c iff b [= a -l> c
proof
set X = {d: a [*] d [= c};
X c= carr(Q)
proof
let x be object;
assume x in X;
then ex d st x = d & a [*] d [= c;
hence thesis;
end;
then reconsider X as Subset of Q;
thus a [*] b [= c implies b [= a -l> c
proof
assume a [*] b [= c;
then b in X;
hence thesis by LATTICE3:38;
end;
deffunc F(Element of Q) = a [*] $1;
defpred P1[set] means $1 in X;
defpred P2[Element of Q] means a [*] $1 [= c;
assume b [= a -l> c;
then
A1: a [*] b [= a [*] "\/"X by Th8;
now
let d;
assume d in X;
then ex d1 st d = d1 & a [*] d1 [= c;
hence a [*] d [= c;
end;
then
A2: P1[d] iff P2[d];
A3: {F(d1): P1[d1]} = {F(d2): P2[d2]} from FRAENKEL:sch 3(A2);
A4: {a [*] d: d in X} is_less_than c
proof
let d1;
assume d1 in {a [*] d: d in X};
then ex d2 st d1 = a [*] d2 & a [*] d2 [= c by A3;
hence thesis;
end;
a [*] "\/"X = "\/"({a [*] d: d in X}, Q) by Def5;
then a [*] "\/"X [= c by A4,LATTICE3:def 21;
hence thesis by A1,LATTICES:7;
end;
theorem Th12:
a [*] b [= c iff a [= b -r> c
proof
set X = {d: d [*] b [= c};
X c= carr(Q)
proof
let x be object;
assume x in X;
then ex d st x = d & d [*] b [= c;
hence thesis;
end;
then reconsider X as Subset of Q;
thus a [*] b [= c implies a [= b -r> c
proof
assume a [*] b [= c;
then a in X;
hence thesis by LATTICE3:38;
end;
deffunc F(Element of Q) = $1 [*] b;
defpred P1[set] means $1 in X;
defpred P2[Element of Q] means $1 [*] b [= c;
assume a [= b -r> c;
then
A1: a [*] b [= ("\/"X) [*] b by Th8;
now
let d;
assume d in X;
then ex d1 st d = d1 & d1 [*] b [= c;
hence d [*] b [= c;
end;
then
A2: P1[d] iff P2[d];
A3: {F(d1): P1[d1]} = {F(d2): P2[d2]} from FRAENKEL:sch 3(A2);
A4: {d [*] b: d in X} is_less_than c
proof
let d1;
assume d1 in {d [*] b: d in X};
then ex d2 st d1 = d2 [*] b & d2 [*] b [= c by A3;
hence thesis;
end;
("\/"X) [*] b = "\/"({d [*] b: d in X}, Q) by Def6;
then ("\/"X) [*] b [= c by A4,LATTICE3:def 21;
hence thesis by A1,LATTICES:7;
end;
theorem Th13:
for Q being Quantale, s,a,b being Element of Q st a [= b holds b
-r>s [= a-r>s & b-l>s [= a-l>s
proof
let Q be Quantale, s,a,b be Element of Q such that
A1: a [= b;
{d where d is Element of Q: d [*] b [= s} c= {c where c is Element of Q:
c [*] a [= s}
proof
let x be object;
assume x in {d where d is Element of Q: d [*] b [= s};
then consider d being Element of Q such that
A2: x = d and
A3: d [*] b [= s;
d [*] a [= d [*] b by A1,Th8;
then d [*] a [= s by A3,LATTICES:7;
hence thesis by A2;
end;
hence b-r>s [= a-r>s by LATTICE3:45;
{d where d is Element of Q: b [*] d [= s} c= {c where c is Element of Q:
a [*] c [= s}
proof
let x be object;
assume x in {d where d is Element of Q: b [*] d [= s};
then consider d being Element of Q such that
A4: x = d and
A5: b [*] d [= s;
a [*] d [= b [*] d by A1,Th8;
then a [*] d [= s by A5,LATTICES:7;
hence thesis by A4;
end;
hence thesis by LATTICE3:45;
end;
theorem
for Q being Quantale, s being Element of Q, j being UnOp of Q st for a
being Element of Q holds j.a = (a-r>s)-r>s holds j is monotone
proof
let Q be Quantale, s be Element of Q;
let j be UnOp of Q such that
A1: for a being Element of Q holds j.a = (a-r>s)-r>s;
thus j is monotone
proof
let a,b be Element of Q;
assume a [= b;
then b-r>s [= a-r>s by Th13;
then
A2: (a-r>s)-r>s [= (b-r>s)-r>s by Th13;
(a-r>s)-r>s = j.a by A1;
hence thesis by A1,A2;
end;
end;
definition
let Q be non empty QuantaleStr;
let IT be Element of Q;
attr IT is dualizing means
for a being Element of Q holds (a-r>IT) -l>IT = a & (a-l>IT)-r>IT = a;
attr IT is cyclic means
for a being Element of Q holds a -r> IT = a -l> IT;
end;
theorem Th15:
c is cyclic iff for a,b st a [*] b [= c holds b [*] a [= c
proof
thus c is cyclic implies for a,b st a [*] b [= c holds b [*] a [= c
proof
assume
A1: a -r> c = a -l> c;
let a,b;
assume a [*] b [= c;
then a [= b-r>c by Th12;
then a [= b-l>c by A1;
hence thesis by Th11;
end;
assume
A2: a [*] b [= c implies b [*] a [= c;
let a;
set X1 = {d1: d1 [*] a [= c}, X2 = {d2: a [*] d2 [= c};
X1 = X2
proof
thus X1 c= X2
proof
let x be object;
assume x in X1;
then consider d such that
A3: x = d and
A4: d [*] a [= c;
a [*] d [= c by A2,A4;
hence thesis by A3;
end;
let x be object;
assume x in X2;
then consider d such that
A5: x = d and
A6: a [*] d [= c;
d [*] a [= c by A2,A6;
hence thesis by A5;
end;
hence thesis;
end;
theorem Th16:
for Q being Quantale, s,a being Element of Q st s is cyclic
holds a [= (a-r>s)-r>s & a [= (a-l>s)-l>s
proof
let Q;
let s,a be Element of Q such that
A1: s is cyclic;
A2: {b: b [= a} c= {c: c[*](a-r>s) [= s}
proof
let x be object;
assume x in {b: b [= a};
then consider b such that
A3: x = b and
A4: b [= a;
(b-r>s)[*]b [= s by Th12;
then
A5: b[*](b-r>s) [= s by A1,Th15;
a-r>s [= b-r>s by A4,Th13;
then b[*](a-r>s) [= b[*](b-r>s) by Th8;
then b[*](a-r>s) [= s by A5,LATTICES:7;
hence thesis by A3;
end;
A6: {b: b [= a} c= {c: (a-l>s)[*]c [= s}
proof
let x be object;
assume x in {b: b [= a};
then consider b such that
A7: x = b and
A8: b [= a;
b[*](b-l>s) [= s by Th11;
then
A9: (b-l>s)[*]b [= s by A1,Th15;
a-l>s [= b-l>s by A8,Th13;
then (a-l>s)[*]b [= (b-l>s)[*]b by Th8;
then (a-l>s)[*]b [= s by A9,LATTICES:7;
hence thesis by A7;
end;
a = "\/"({d: d [= a},Q) by LATTICE3:44;
hence a [= (a-r>s)-r>s by A2,LATTICE3:45;
a = "\/"({d: d [= a},Q) by LATTICE3:44;
hence thesis by A6,LATTICE3:45;
end;
theorem
for Q being Quantale, s,a being Element of Q st s is cyclic holds a-r>
s = ((a-r>s)-r>s)-r>s & a-l>s = ((a-l>s)-l>s)-l>s
proof
let Q;
let s,a be Element of Q;
assume
A1: s is cyclic;
then a [= (a-r>s)-r>s by Th16;
then
A2: ((a-r>s)-r>s)-r>s [= a-r>s by Th13;
a [= (a-l>s)-l>s by A1,Th16;
then
A3: ((a-l>s)-l>s)-l>s [= a-l>s by Th13;
a-r>s [= ((a-r>s)-r>s)-r>s & a-l>s [= ((a-l>s)-l>s)-l>s by A1,Th16;
hence thesis by A2,A3,LATTICES:8;
end;
theorem
for Q being Quantale, s,a,b being Element of Q holds ((a-r>s)-r>s)[*](
(b-r>s)-r>s) [= ((a[*]b)-r>s)-r>s
proof
let Q;
let s,a,b be Element of Q;
deffunc NEG(Element of Q) = {c: c[*]($1-r>s) [= s};
A1: {a9[*]b9: a9 in NEG(a) & b9 in NEG(b)} c= NEG(a[*]b)
proof
defpred P[Element of Q] means $1[*](a[*]b) [= s;
deffunc G(Element of Q) = $1;
let x be object;
set A = {G(c): P[c]};
assume x in {a9[*]b9: a9 in NEG(a) & b9 in NEG(b)};
then consider a9, b9 such that
A2: x = a9[*]b9 and
A3: a9 in NEG(a) and
A4: b9 in NEG(b);
deffunc F(Element of Q) = a9[*]b9[*]$1;
set B = {F(G(c)): P[c]};
A5: ex c st b9 = c & c[*] (b-r>s) [= s by A4;
A6: ex c st a9 = c & c[*](a-r>s) [= s by A3;
A7: B is_less_than s
proof
let d;
assume d in B;
then consider c such that
A8: d = a9[*]b9[*]c and
A9: c[*](a[*]b) [= s;
A10: b-r>s [= b9-l>s by A5,Th11;
c[*]a[*]b [= s by A9,GROUP_1:def 3;
then c[*]a [= b-r>s by Th12;
then c[*]a [= b9-l>s by A10,LATTICES:7;
then b9[*](c[*]a) [= s by Th11;
then b9[*]c[*]a [= s by GROUP_1:def 3;
then
A11: b9[*]c [= a-r>s by Th12;
a-r>s [= a9-l>s by A6,Th11;
then b9[*]c [= a9-l>s by A11,LATTICES:7;
then a9[*](b9[*]c) [= s by Th11;
hence d [= s by A8,GROUP_1:def 3;
end;
{F(c): c in A} = B from DenestFraenkel;
then a9[*]b9[*]((a[*]b)-r>s) = "\/"(B, Q) by Def5;
then a9[*]b9[*]((a[*]b)-r>s) [= s by A7,LATTICE3:def 21;
hence thesis by A2;
end;
((a-r>s)-r>s)[*]((b-r>s)-r>s) = "\/"({a9[*] b9: a9 in NEG(a) & b9 in NEG
(b)}, Q) by Th5;
hence thesis by A1,LATTICE3:45;
end;
theorem Th19:
D is dualizing implies Q is unital & the_unity_wrt the multF of
Q = D -r> D & the_unity_wrt the multF of Q = D -l> D
proof
set I = D-l>D, J = D-r>D;
assume
A1: (a-r>D)-l>D = a & (a-l>D)-r>D = a;
A2: now
deffunc F(set) = $1;
let a;
defpred P1[Element of Q] means $1 [*] (a [*] I) [= D;
defpred P2[Element of Q] means $1 [*] a [= D;
defpred P3[Element of Q] means J [*] a [*] $1 [= D;
defpred P4[Element of Q] means a [*] $1 [= D;
A3: P1[b] iff P2[b]
proof
b [*] (a [*] I) = b [*] a [*] I & I-r>D=D by A1,GROUP_1:def 3;
hence thesis by Th12;
end;
A4: {F(b): P1[b]} = {F(c): P2[c]} from FRAENKEL:sch 3(A3);
thus a [*] I = ((a [*] I)-r>D)-l>D by A1
.= (a-r>D)-l>D by A4
.= a by A1;
A5: P3[b] iff P4[b]
proof
J [*] (a [*] b) = J [*] a [*] b & J-l>D=D by A1,GROUP_1:def 3;
hence thesis by Th11;
end;
A6: {F(b): P3[b]} = {F(c): P4[c]} from FRAENKEL:sch 3(A5);
thus J [*] a = ((J [*] a)-l>D)-r>D by A1
.= (a-l>D)-r>D by A6
.= a by A1;
end;
A7: I is_a_right_unity_wrt times(Q)
proof
let a;
thus times(Q).(a,I) = a [*] I .= a by A2;
end;
A8: I = J [*] I by A2;
I is_a_left_unity_wrt times(Q)
proof
let a;
thus times(Q).(I,a) = J [*] a by A2,A8
.= a by A2;
end;
then
A9: I is_a_unity_wrt times(Q) by A7;
hence times(Q) is having_a_unity;
J = J [*] I by A2;
hence thesis by A8,A9,BINOP_1:def 8;
end;
theorem
a is dualizing implies b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = (
(c -r> a) [*] b) -l> a
proof
deffunc F(set) = $1;
defpred P1[Element of Q] means $1 [*] b [= c;
defpred P2[Element of Q] means $1 [*] (b [*] (c -l> a)) [= a;
defpred P3[Element of Q] means b [*] $1 [= c;
defpred P4[Element of Q] means (c -r> a) [*] b [*] $1 [= a;
assume
A1: (d -r> a) -l> a = d & (d -l> a) -r> a = d;
then
A2: c = (c -l> a) -r> a;
A3: P1[d] iff P2[d]
proof
d [*] (b [*] (c -l> a)) = d [*] b [*] (c -l> a) by GROUP_1:def 3;
hence thesis by A2,Th12;
end;
{F(d1): P1[d1]} = {F(d2): P2[d2]} from FRAENKEL:sch 3(A3);
hence b -r> c = (b [*] (c -l> a)) -r> a;
A4: c = (c -r> a) -l> a by A1;
A5: P3[d] iff P4[d]
proof
(c -r> a) [*] b [*] d = (c -r> a) [*] (b [*] d) by GROUP_1:def 3;
hence thesis by A4,Th11;
end;
{F(d1): P3[d1]} = {F(d2): P4[d2]} from FRAENKEL:sch 3(A5);
hence thesis;
end;
definition
struct (QuasiNetStr) Girard-QuantaleStr (# carrier -> set, L_join, L_meet,
multF -> (BinOp of the carrier), OneF, absurd -> Element of the carrier #);
end;
registration
cluster non empty for Girard-QuantaleStr;
existence
proof
set A = the non empty set,b1 = the (BinOp of A),e1 = the Element of A;
take Girard-QuantaleStr(#A,b1,b1,b1,e1,e1#);
thus the carrier of Girard-QuantaleStr(#A,b1,b1,b1,e1,e1#) is non empty;
end;
end;
definition
let IT be non empty Girard-QuantaleStr;
attr IT is cyclic means
: Def19:
the absurd of IT is cyclic;
attr IT is dualized means
: Def20:
the absurd of IT is dualizing;
end;
theorem Th21:
for Q being non empty Girard-QuantaleStr st the LattStr of Q =
BooleLatt {} holds Q is cyclic dualized
proof
let Q be non empty Girard-QuantaleStr;
set c = the absurd of Q;
assume the LattStr of Q = BooleLatt {};
then
A1: carr(Q) = {{}} by LATTICE3:def 1,ZFMISC_1:1;
thus Q is cyclic
proof
let a be Element of Q;
a -r> c = {} by A1,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
let a be Element of Q;
(a-r>c)-l>c = {} & (a-l>c)-r>c = {} by A1,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
registration
let A be non empty set, b1,b2,b3 be (BinOp of A), e1,e2 be Element of A;
cluster Girard-QuantaleStr(#A,b1,b2,b3,e1,e2#) -> non empty;
coherence;
end;
registration
cluster associative commutative unital left-distributive right-distributive
complete Lattice-like cyclic dualized strict for
non empty Girard-QuantaleStr;
existence
proof
set B = BooleLatt {};
set b = the BinOp of B;
set e = the Element of B;
take Girard-QuantaleStr (#carr(B), join(B), met(B), b, e, e#);
thus thesis by Th4,Th21;
end;
end;
definition
mode Girard-Quantale is associative unital left-distributive
right-distributive complete Lattice-like cyclic dualized non empty
Girard-QuantaleStr;
end;
definition
let G be Girard-QuantaleStr;
func Bottom G -> Element of G equals
the absurd of G;
correctness;
end;
definition
let G be non empty Girard-QuantaleStr;
func Top G -> Element of G equals
(Bottom G) -r> Bottom G;
correctness;
let a be Element of G;
func Bottom a -> Element of G equals
a -r> Bottom G;
correctness;
end;
definition
let G be non empty Girard-QuantaleStr;
func Negation G -> UnOp of G means
for a being Element of G holds it.a = Bottom a;
existence
proof
deffunc F(Element of G) = Bottom $1;
consider f being Function of the carrier of G, the carrier of G such that
A1: for a being Element of G holds f.a = F(a) from FUNCT_2:sch 4;
reconsider f as UnOp of G;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be UnOp of G such that
A2: for a being Element of G holds f1.a = Bottom a and
A3: for a being Element of G holds f2.a = Bottom a;
now
let a be Element of G;
thus f1.a = Bottom a by A2
.= f2.a by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let G be non empty Girard-QuantaleStr, u be UnOp of G;
func Bottom u -> UnOp of G equals
Negation(G)*u;
correctness;
end;
definition
let G be non empty Girard-QuantaleStr, o be BinOp of G;
func Bottom o -> BinOp of G equals
Negation(G)*o;
correctness;
end;
reserve Q for Girard-Quantale,
a,a1,a2,b,b1,b2,c,d for Element of Q,
X for set;
theorem Th22:
Bottom Bottom a = a
proof
the absurd of Q is cyclic by Def19;
then
A1: a-l>the absurd of Q = a-r>the absurd of Q;
the absurd of Q is dualizing by Def20;
hence thesis by A1;
end;
theorem
a [= b implies Bottom b [= Bottom a by Th13;
theorem Th24:
Bottom "\/"(X,Q) = "/\"({Bottom a: a in X}, Q)
proof
{"/\"({Bottom a: a in X}, Q) [*] b: b in X} is_less_than Bottom Q
proof
let c;
assume c in {"/\"({Bottom a: a in X}, Q) [*] b: b in X};
then consider b such that
A1: c = "/\"({Bottom a: a in X}, Q) [*] b & b in X;
Bottom b in {Bottom a: a in X} by A1;
then "/\"({Bottom a: a in X}, Q) [= Bottom b by LATTICE3:38;
hence c [= Bottom Q by A1,Th12;
end;
then "\/"({"/\" ({Bottom a: a in X}, Q) [*] b: b in X}, Q) [= Bottom Q by
LATTICE3:def 21;
then "/\"({Bottom a: a in X}, Q) [*] "\/"(X,Q) [= Bottom Q by Def5;
then
A2: "/\"({Bottom a: a in X}, Q) [= Bottom "\/"(X,Q) by Th12;
Bottom "\/"(X,Q) is_less_than {Bottom a: a in X}
proof
let b;
assume b in {Bottom a: a in X};
then consider a such that
A3: b = Bottom a and
A4: a in X;
a [= "\/"(X,Q) by A4,LATTICE3:38;
hence thesis by A3,Th13;
end;
then Bottom "\/"(X,Q) [= "/\"({Bottom a: a in X}, Q) by LATTICE3:39;
hence thesis by A2,LATTICES:8;
end;
theorem Th25:
Bottom "/\"(X,Q) = "\/"({Bottom a: a in X}, Q)
proof
X is_greater_than "/\"({Bottom a: a in {Bottom b: b in X}}, Q)
proof
let c;
assume c in X;
then Bottom c in {Bottom b: b in X};
then
A1: Bottom Bottom c in {Bottom a: a in {Bottom b: b in X}};
Bottom Bottom c = c by Th22;
hence thesis by A1,LATTICE3:38;
end;
then
A2: "/\"({Bottom a: a in {Bottom b: b in X}}, Q) [= "/\"(X,Q) by LATTICE3:39;
{Bottom a: a in {Bottom b: b in X}} c= X
proof
let x be object;
assume x in {Bottom a: a in {Bottom b: b in X}};
then consider a such that
A3: x = Bottom a & a in {Bottom b: b in X};
ex b st a = Bottom b & b in X by A3;
hence thesis by A3,Th22;
end;
then "/\"(X,Q) [= "/\"({Bottom a: a in {Bottom b: b in X}}, Q) by LATTICE3:45
;
then "/\"(X,Q) = "/\"({Bottom a: a in {Bottom b: b in X}}, Q) by A2,
LATTICES:8;
hence Bottom "/\"(X,Q) = Bottom Bottom "\/"({Bottom a: a in X}, Q) by Th24
.= "\/"({Bottom a: a in X}, Q) by Th22;
end;
theorem Th26:
Bottom (a"\/"b) = Bottom a"/\"Bottom b & Bottom (a"/\"b) =
Bottom a"\/"Bottom b
proof
A1: {Bottom c: c in {a,b}} = {Bottom a,Bottom b}
proof
thus {Bottom c: c in {a,b}} c= {Bottom a,Bottom b}
proof
let x be object;
assume x in {Bottom c: c in {a,b}};
then consider c such that
A2: x = Bottom c and
A3: c in {a,b};
c = a or c = b by A3,TARSKI:def 2;
hence thesis by A2,TARSKI:def 2;
end;
let x be object;
assume x in {Bottom a,Bottom b};
then x = Bottom a & a in {a,b} or x = Bottom b & b in {a,b} by TARSKI:def 2
;
hence thesis;
end;
a"\/"b = "\/"{a,b} & Bottom a"/\"Bottom b = "/\"{Bottom a,Bottom b} by
LATTICE3:43;
hence Bottom (a"\/"b) = Bottom a"/\"Bottom b by A1,Th24;
Bottom a"\/"Bottom b = "\/"{Bottom a,Bottom b} & a"/\"b = "/\"{a,b} by
LATTICE3:43;
hence thesis by A1,Th25;
end;
definition
let Q,a,b;
func a delta b -> Element of Q equals
Bottom (Bottom a [*] Bottom b);
correctness;
end;
theorem
a [*] "\/"(X,Q) = "\/"({a [*] b: b in X}, Q) & a delta "/\"(X,Q) =
"/\"({a delta c: c in X}, Q)
proof
deffunc F(Element of Q) = Bottom a [*] $1;
deffunc G(Element of Q) = Bottom $1;
deffunc H(Element of Q) = Bottom a [*] Bottom $1;
defpred P[set] means $1 in X;
deffunc F1(Element of Q) = Bottom (Bottom a [*] Bottom $1);
deffunc F2(Element of Q) = a delta $1;
thus a [*] "\/"(X,Q) = "\/"({a [*] b: b in X}, Q) by Def5;
A1: {F(c): c in {G(d): P[d]}} = {F(G(b)): P[b]} from DenestFraenkel;
A2: {G(c): c in {H(d): P[d]}} = {G(H(b)): P[b]} from DenestFraenkel;
A3: F1(b) = F2(b);
A4: {F1(b): P[b]} = {F2(c): P[c]} from FRAENKEL:sch 5(A3);
thus a delta "/\"(X,Q) = Bottom (Bottom a [*] "\/"({Bottom b: b in X}, Q))
by Th25
.= Bottom "\/"({Bottom a [*] Bottom b: b in X}, Q) by A1,Def5
.= "/\"({a delta b: b in X}, Q) by A2,A4,Th24;
end;
theorem
"\/"(X,Q) [*] a = "\/"({b [*] a: b in X}, Q) & "/\"(X,Q) delta a =
"/\"({c delta a: c in X}, Q)
proof
deffunc F(Element of Q) = $1 [*] Bottom a;
deffunc G(Element of Q) = Bottom $1;
deffunc H(Element of Q) = Bottom $1 [*] Bottom a;
defpred P[set] means $1 in X;
deffunc F1(Element of Q) = Bottom (Bottom $1 [*] Bottom a);
deffunc F2(Element of Q) = $1 delta a;
thus "\/"(X,Q) [*] a = "\/"({b [*] a: b in X}, Q) by Def6;
A1: {F(c): c in {G(d): P[d]}} = {F(G(b)): P[b]} from DenestFraenkel;
A2: {G(c): c in {H(d): P[d]}} = {G(H(b)): P[b]} from DenestFraenkel;
A3: F1(b) = F2(b);
A4: {F1(b): P[b]} = {F2(c): P[c]} from FRAENKEL:sch 5(A3);
thus "/\"(X,Q) delta a = Bottom ("\/"({Bottom b: b in X}, Q) [*] Bottom a)
by Th25
.= Bottom "\/"({Bottom b [*] Bottom a: b in X}, Q) by A1,Def6
.= "/\"({b delta a: b in X}, Q) by A2,A4,Th24;
end;
theorem
a delta (b"/\"c) = (a delta b)"/\"(a delta c) & (b"/\"c) delta a = (b
delta a)"/\"(c delta a)
proof
thus a delta (b"/\"c) = Bottom (Bottom a [*] (Bottom b"\/"Bottom c)) by Th26
.= Bottom ((Bottom a [*] Bottom b)"\/"(Bottom a [*] Bottom c)) by Th6
.= (a delta b)"/\"(a delta c) by Th26;
thus (b"/\"c) delta a = Bottom ((Bottom b"\/"Bottom c) [*] Bottom a) by Th26
.= Bottom ((Bottom b [*] Bottom a)"\/"(Bottom c [*] Bottom a)) by Th6
.= (b delta a)"/\"(c delta a) by Th26;
end;
theorem
a1 [= b1 & a2 [= b2 implies a1 delta a2 [= b1 delta b2
proof
assume a1 [= b1 & a2 [= b2;
then Bottom b1 [= Bottom a1 & Bottom b2 [= Bottom a2 by Th13;
then Bottom b1 [*] Bottom b2 [= Bottom a1 [*] Bottom a2 by Th9;
hence thesis by Th13;
end;
theorem
a delta b delta c = a delta (b delta c)
proof
thus a delta b delta c = Bottom (Bottom a [*] Bottom b [*] Bottom c) by Th22
.= Bottom (Bottom a [*] (Bottom b [*] Bottom c)) by GROUP_1:def 3
.= a delta (b delta c) by Th22;
end;
theorem Th32:
a [*] Top Q = a & Top Q [*] a = a
proof
the absurd of Q is dualizing by Def20;
then
A1: Top Q = the_unity_wrt times(Q) by Th19;
times(Q) is having_a_unity by MONOID_0:def 10;
hence thesis by A1,SETWISEO:15;
end;
theorem
a delta Bottom Q = a & (Bottom Q) delta a = a
proof
Bottom a [*] Top Q = Bottom a & Top Q [*] Bottom a = Bottom a by Th32;
hence thesis by Th22;
end;
theorem
for Q being Quantale for j being UnOp of Q st j is monotone idempotent
\/-distributive ex L being complete Lattice st the carrier of L = rng j & for X
being Subset of L holds "\/"X = j."\/"(X,Q)
proof
let Q be Quantale, j be UnOp of Q;
assume
A1: j is monotone idempotent \/-distributive;
reconsider D = rng j as non empty Subset of Q;
dom j = carr(Q) by FUNCT_2:def 1;
then reconsider j9 = j as Function of carr(Q), D by RELSET_1:4;
deffunc F(Subset of D) = j9."\/"($1,Q);
consider f being Function of bool D, D such that
A2: for X being Subset of D holds f.X = F(X) from FUNCT_2:sch 4;
A3: dom f = bool D by FUNCT_2:def 1;
A4: for X being Subset-Family of D holds f.(f.:X) = f.(union X)
proof
let X be Subset-Family of D;
set A = {j.a where a is Element of Q: a in f.:X};
set B = {j.b where b is Element of Q: b in union X};
reconsider Y = f.:X, X9 = union X as Subset of Q by XBOOLE_1:1;
now
let a be Element of Q;
assume a in B;
then consider b9 being Element of Q such that
A5: a = j.b9 and
A6: b9 in union X;
consider Y being set such that
A7: b9 in Y and
A8: Y in X by A6,TARSKI:def 4;
reconsider Y as Subset of D by A8;
A9: b9 [= "\/"(Y,Q) by A7,LATTICE3:38;
take b = j."\/"(Y,Q);
b = f.Y by A2;
then
A10: b in f.:X by A3,A8,FUNCT_1:def 6;
j.b = b by A1,Lm1;
hence a [= b & b in A by A1,A5,A10,A9;
end;
then
A11: "\/"(B, Q) [= "\/"(A, Q) by LATTICE3:47;
A is_less_than "\/"(B, Q)
proof
let a be Element of Q;
assume a in A;
then consider a9 being Element of Q such that
A12: a = j.a9 and
A13: a9 in f.:X;
consider x being object such that
A14: x in dom f and
A15: x in X and
A16: a9 = f.x by A13,FUNCT_1:def 6;
reconsider x as Subset of D by A14;
reconsider Y = x as Subset of Q by XBOOLE_1:1;
A17: {j.b where b is Element of Q: b in Y} c= B
proof
let z be object;
assume z in {j.b where b is Element of Q: b in Y};
then consider b being Element of Q such that
A18: z = j.b and
A19: b in Y;
b in union X by A15,A19,TARSKI:def 4;
hence thesis by A18;
end;
a9 = j."\/"Y by A2,A16;
then a9 = "\/" ({j.b where b is Element of Q: b in Y}, Q) by A1,Th10;
then a9 [= "\/"(B, Q) by A17,LATTICE3:45;
then a [= j."\/"(B, Q) by A1,A12;
then a [= j.(j."\/"X9) by A1,Th10;
then a [= j."\/"X9 by A1,Lm1;
hence thesis by A1,Th10;
end;
then
A20: "\/"(A, Q) [= "\/"(B, Q) by LATTICE3:def 21;
thus f.(f.:X) = j."\/"Y by A2
.= "\/"(A, Q) by A1,Th10
.= "\/"(B, Q) by A20,A11,LATTICES:8
.= j."\/"X9 by A1,Th10
.= f.union X by A2;
end;
for a being Element of D holds f.{a} = a
proof
let a be Element of D;
consider a9 being object such that
A21: a9 in dom j and
A22: a = j.a9 by FUNCT_1:def 3;
reconsider x = a as Element of Q;
reconsider x9 = {x} as Subset of Q;
reconsider a9 as Element of Q by A21;
thus f.{a} = j."\/"x9 by A2
.= j.(j.a9) by A22,LATTICE3:42
.= a by A1,A22,Lm1;
end;
then consider L being complete strict Lattice such that
A23: carr(L) = D and
A24: for X being Subset of L holds "\/" X = f.X by A4,LATTICE3:55;
take L;
thus carr(L) = rng j by A23;
let X be Subset of L;
thus "\/"X = f.X by A24
.= j."\/"(X,Q) by A2,A23;
end;