:: Quantales
:: by Grzegorz Bancerek
::
:: Received May 9, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

scheme :: QUANTAL1:sch 1
DenestFraenkel{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> set , F4( set ) -> Element of F2(), P1[ set ] } :
{ F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } = { F3(F4(a)) where a is Element of F1() : P1[a] }
proof end;

scheme :: QUANTAL1:sch 2
EmptyFraenkel{ F1() -> non empty set , F2( set ) -> set , P1[ set ] } :
{ F2(a) where a is Element of F1() : P1[a] } = {}
provided
A1: for a being Element of F1() holds P1[a]
proof end;

deffunc H1( non empty LattStr ) -> set = the carrier of $1;

deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;

deffunc H3( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;

deffunc H4( multMagma ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the multF of $1;

theorem Th1: :: QUANTAL1:1
for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
proof end;

theorem Th2: :: QUANTAL1:2
for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a being Element of L1
for b being Element of L2
for X being set st a = b holds
( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )
proof end;

definition
let L be 1-sorted ;
mode UnOp of L is Function of L,L;
end;

definition
let L be non empty LattStr ;
let X be Subset of L;
attr X is directed means :: QUANTAL1:def 1
 for Y being finite Subset of X ex x being Element of L st
( "\/" (Y,L) [= x & x in X );
end;

:: deftheorem defines directed QUANTAL1:def 1 :
for L being non empty LattStr
for X being Subset of L holds
( X is directed iff for Y being finite Subset of X ex x being Element of L st
( "\/" (Y,L) [= x & x in X ) );

theorem :: QUANTAL1:3
for L being non empty LattStr
for X being Subset of L st X is directed holds
not X is empty
proof end;

definition
attr c1 is strict ;
struct QuantaleStr -> LattStr , multMagma ;
aggr QuantaleStr(# carrier, L_join, L_meet, multF #) -> QuantaleStr ;
end;

registration
cluster non empty for QuantaleStr ;
existence
not for b1 being QuantaleStr holds b1 is empty
proof end;
end;

definition
attr c1 is strict ;
struct QuasiNetStr -> QuantaleStr , multLoopStr ;
aggr QuasiNetStr(# carrier, L_join, L_meet, multF, OneF #) -> QuasiNetStr ;
end;

registration
cluster non empty for QuasiNetStr ;
existence
not for b1 being QuasiNetStr holds b1 is empty
proof end;
end;

definition
let IT be non empty multMagma ;
attr IT is with_left-zero means :: QUANTAL1:def 2
 ex a being Element of IT st
for b being Element of IT holds a * b = a;
attr IT is with_right-zero means :: QUANTAL1:def 3
 ex b being Element of IT st
for a being Element of IT holds a * b = b;
end;

:: deftheorem defines with_left-zero QUANTAL1:def 2 :
for IT being non empty multMagma holds
( IT is with_left-zero iff ex a being Element of IT st
for b being Element of IT holds a * b = a );

:: deftheorem defines with_right-zero QUANTAL1:def 3 :
for IT being non empty multMagma holds
( IT is with_right-zero iff ex b being Element of IT st
for a being Element of IT holds a * b = b );

definition
let IT be non empty multMagma ;
attr IT is with_zero means :Def4: :: QUANTAL1:def 4
( IT is with_left-zero & IT is with_right-zero );
end;

:: deftheorem Def4 defines with_zero QUANTAL1:def 4 :
for IT being non empty multMagma holds
( IT is with_zero iff ( IT is with_left-zero & IT is with_right-zero ) );

registration
cluster non empty with_zero -> non empty with_left-zero with_right-zero for multMagma ;
coherence
for b1 being non empty multMagma st b1 is with_zero holds
( b1 is with_left-zero & b1 is with_right-zero ) by Def4;
cluster non empty with_left-zero with_right-zero -> non empty with_zero for multMagma ;
coherence
for b1 being non empty multMagma st b1 is with_left-zero & b1 is with_right-zero holds
b1 is with_zero by Def4;
end;

registration
cluster non empty with_zero for multMagma ;
existence
ex b1 being non empty multMagma st b1 is with_zero
proof end;
end;

definition
let IT be non empty QuantaleStr ;
attr IT is right-distributive means :Def5: :: QUANTAL1:def 5
 for a being Element of IT
for 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: :: QUANTAL1:def 6
 for a being Element of IT
for 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 :: QUANTAL1:def 7
 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 :: QUANTAL1:def 8
 for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds
("\/" X1) [*] ("\/" X2) = "\/" ( { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT);
end;

:: deftheorem Def5 defines right-distributive QUANTAL1:def 5 :
for IT being non empty QuantaleStr holds
( IT is right-distributive iff for a being Element of IT
for X being set holds a [*] ("\/" (X,IT)) = "\/" ( { (a [*] b) where b is Element of IT : b in X } ,IT) );

:: deftheorem Def6 defines left-distributive QUANTAL1:def 6 :
for IT being non empty QuantaleStr holds
( IT is left-distributive iff for a being Element of IT
for X being set holds ("\/" (X,IT)) [*] a = "\/" ( { (b [*] a) where b is Element of IT : b in X } ,IT) );

:: deftheorem defines times-additive QUANTAL1:def 7 :
for IT being non empty QuantaleStr holds
( IT is times-additive iff for a, b, c being Element of IT holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) );

:: deftheorem defines times-continuous QUANTAL1:def 8 :
for IT being non empty QuantaleStr holds
( IT is times-continuous iff for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds
("\/" X1) [*] ("\/" X2) = "\/" ( { (a [*] b) where a, b is Element of IT : ( a in X1 & b in X2 ) } ,IT) );

theorem Th4: :: QUANTAL1:4
for Q being non empty QuantaleStr st LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} holds
( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
proof end;

registration
let A be non empty set ;
let b1, b2, b3 be BinOp of A;
cluster QuantaleStr(# A,b1,b2,b3 #) -> non empty ;
coherence
not QuantaleStr(# A,b1,b2,b3 #) is empty ;
end;

registration
cluster non empty unital associative commutative Lattice-like complete with_zero right-distributive left-distributive for QuantaleStr ;
existence
ex b1 being non empty QuantaleStr st
( b1 is associative & b1 is commutative & b1 is unital & b1 is with_zero & b1 is left-distributive & b1 is right-distributive & b1 is complete & b1 is Lattice-like )
proof end;
end;

scheme :: QUANTAL1:sch 3
LUBFraenkelDistr{ F1() -> non empty Lattice-like complete QuantaleStr , F2( set , set ) -> Element of F1(), F3() -> set , F4() -> set } :
"\/" ( { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ,F1()) = "\/" ( { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ,F1())
proof end;

theorem Th5: :: QUANTAL1:5
for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr
for X, Y being set holds ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q)
proof end;

theorem Th6: :: QUANTAL1:6
for Q being non empty Lattice-like complete right-distributive left-distributive QuantaleStr
for a, b, c being Element of Q holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )
proof end;

registration
let A be non empty set ;
let b1, b2, b3 be BinOp of A;
let e be Element of A;
cluster QuasiNetStr(# A,b1,b2,b3,e #) -> non empty ;
coherence
not QuasiNetStr(# A,b1,b2,b3,e #) is empty ;
end;

registration
cluster non empty Lattice-like complete for QuasiNetStr ;
existence
ex b1 being non empty QuasiNetStr st
( b1 is complete & b1 is Lattice-like )
proof end;
end;

registration
cluster non empty Lattice-like complete right-distributive left-distributive -> non empty Lattice-like complete times-additive times-continuous for QuasiNetStr ;
coherence
for b1 being non empty Lattice-like complete QuasiNetStr st b1 is left-distributive & b1 is right-distributive holds
( b1 is times-continuous & b1 is times-additive )
proof end;
end;

registration
cluster non empty unital associative commutative Lattice-like complete with_left-zero with_zero right-distributive left-distributive for QuasiNetStr ;
existence
ex b1 being non empty QuasiNetStr st
( b1 is associative & b1 is commutative & b1 is unital & b1 is with_zero & b1 is with_left-zero & b1 is left-distributive & b1 is right-distributive & b1 is complete & b1 is Lattice-like )
proof end;
end;

definition
mode Quantale is non empty associative Lattice-like complete right-distributive left-distributive QuantaleStr ;
mode QuasiNet is non empty unital associative Lattice-like complete with_left-zero times-additive times-continuous QuasiNetStr ;
end;

definition
mode BlikleNet is with_zero QuasiNet;
end;

theorem :: QUANTAL1:7
for Q being non empty unital QuasiNetStr st Q is Quantale holds
Q is BlikleNet
proof end;

theorem Th8: :: QUANTAL1:8
for Q being Quantale
for a, b, c being Element of Q st a [= b holds
( a [*] c [= b [*] c & c [*] a [= c [*] b )
proof end;

theorem Th9: :: QUANTAL1:9
for Q being Quantale
for a, b, c, d being Element of Q st a [= b & c [= d holds
a [*] c [= b [*] d
proof end;

definition
let f be Function;
attr f is idempotent means :: QUANTAL1:def 9
f * f = f;
end;

:: deftheorem defines idempotent QUANTAL1:def 9 :
for f being Function holds
( f is idempotent iff f * f = f );

Lm1: for A being non empty set
for f being UnOp of A st f is idempotent holds
for a being Element of A holds f . (f . a) = f . a
proof end;

definition
let L be non empty LattStr ;
let IT be UnOp of L;
attr IT is inflationary means :: QUANTAL1:def 10
 for p being Element of L holds p [= IT . p;
attr IT is deflationary means :: QUANTAL1:def 11
 for p being Element of L holds IT . p [= p;
attr IT is monotone means :Def12: :: QUANTAL1:def 12
 for p, q being Element of L st p [= q holds
IT . p [= IT . q;
attr IT is \/-distributive means :: QUANTAL1:def 13
 for X being Subset of L holds IT . ("\/" X) [= "\/" ( { (IT . a) where a is Element of L : a in X } ,L);
end;

:: deftheorem defines inflationary QUANTAL1:def 10 :
for L being non empty LattStr
for IT being UnOp of L holds
( IT is inflationary iff for p being Element of L holds p [= IT . p );

:: deftheorem defines deflationary QUANTAL1:def 11 :
for L being non empty LattStr
for IT being UnOp of L holds
( IT is deflationary iff for p being Element of L holds IT . p [= p );

:: deftheorem Def12 defines monotone QUANTAL1:def 12 :
for L being non empty LattStr
for IT being UnOp of L holds
( IT is monotone iff for p, q being Element of L st p [= q holds
IT . p [= IT . q );

:: deftheorem defines \/-distributive QUANTAL1:def 13 :
for L being non empty LattStr
for IT being UnOp of L holds
( IT is \/-distributive iff for X being Subset of L holds IT . ("\/" X) [= "\/" ( { (IT . a) where a is Element of L : a in X } ,L) );

registration
let L be Lattice;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V17( the carrier of L) V21( the carrier of L, the carrier of L) inflationary deflationary monotone for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being UnOp of L st
( b1 is inflationary & b1 is deflationary & b1 is monotone )
proof end;
end;

theorem Th10: :: QUANTAL1:10
for L being complete Lattice
for 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 end;

definition
let Q be non empty QuantaleStr ;
let IT be UnOp of Q;
attr IT is times-monotone means :: QUANTAL1:def 14
 for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b);
end;

:: deftheorem defines times-monotone QUANTAL1:def 14 :
for Q being non empty QuantaleStr
for IT being UnOp of Q holds
( IT is times-monotone iff for a, b being Element of Q holds (IT . a) [*] (IT . b) [= IT . (a [*] b) );

definition
let Q be non empty QuantaleStr ;
let a, b be Element of Q;
func a -r> b -> Element of Q equals :: QUANTAL1:def 15
 "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q);
correctness
coherence
"\/" ( { c where c is Element of Q : c [*] a [= b } ,Q) is Element of Q;
;
func a -l> b -> Element of Q equals :: QUANTAL1:def 16
 "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q);
correctness
coherence
"\/" ( { c where c is Element of Q : a [*] c [= b } ,Q) is Element of Q;
;
end;

:: deftheorem defines -r> QUANTAL1:def 15 :
for Q being non empty QuantaleStr
for a, b being Element of Q holds a -r> b = "\/" ( { c where c is Element of Q : c [*] a [= b } ,Q);

:: deftheorem defines -l> QUANTAL1:def 16 :
for Q being non empty QuantaleStr
for a, b being Element of Q holds a -l> b = "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q);

theorem Th11: :: QUANTAL1:11
for Q being Quantale
for a, b, c being Element of Q holds
( a [*] b [= c iff b [= a -l> c )
proof end;

theorem Th12: :: QUANTAL1:12
for Q being Quantale
for a, b, c being Element of Q holds
( a [*] b [= c iff a [= b -r> c )
proof end;

theorem Th13: :: QUANTAL1:13
for Q being Quantale
for s, a, b being Element of Q st a [= b holds
( b -r> s [= a -r> s & b -l> s [= a -l> s )
proof end;

theorem :: QUANTAL1:14
for Q being Quantale
for s being Element of Q
for 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 end;

definition
let Q be non empty QuantaleStr ;
let IT be Element of Q;
attr IT is dualizing means :Def17: :: QUANTAL1:def 17
 for a being Element of Q holds
( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a );
attr IT is cyclic means :Def18: :: QUANTAL1:def 18
 for a being Element of Q holds a -r> IT = a -l> IT;
end;

:: deftheorem Def17 defines dualizing QUANTAL1:def 17 :
for Q being non empty QuantaleStr
for IT being Element of Q holds
( IT is dualizing iff for a being Element of Q holds
( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a ) );

:: deftheorem Def18 defines cyclic QUANTAL1:def 18 :
for Q being non empty QuantaleStr
for IT being Element of Q holds
( IT is cyclic iff for a being Element of Q holds a -r> IT = a -l> IT );

theorem Th15: :: QUANTAL1:15
for Q being Quantale
for c being Element of Q holds
( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c )
proof end;

theorem Th16: :: QUANTAL1:16
for Q being Quantale
for s, a being Element of Q st s is cyclic holds
( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )
proof end;

theorem :: QUANTAL1:17
for Q being Quantale
for 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 end;

theorem :: QUANTAL1:18
for Q being Quantale
for 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 end;

theorem Th19: :: QUANTAL1:19
for Q being Quantale
for D being Element of Q st D is dualizing holds
( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
proof end;

theorem :: QUANTAL1:20
for Q being Quantale
for a, b, c being Element of Q st a is dualizing holds
( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a )
proof end;

definition
attr c1 is strict ;
struct Girard-QuantaleStr -> QuasiNetStr ;
aggr Girard-QuantaleStr(# carrier, L_join, L_meet, multF, OneF, absurd #) -> Girard-QuantaleStr ;
sel absurd c1 -> Element of the carrier of c1;
end;

registration
cluster non empty for Girard-QuantaleStr ;
existence
not for b1 being Girard-QuantaleStr holds b1 is empty
proof end;
end;

definition
let IT be non empty Girard-QuantaleStr ;
attr IT is cyclic means :Def19: :: QUANTAL1:def 19
 the absurd of IT is cyclic ;
attr IT is dualized means :Def20: :: QUANTAL1:def 20
 the absurd of IT is dualizing ;
end;

:: deftheorem Def19 defines cyclic QUANTAL1:def 19 :
for IT being non empty Girard-QuantaleStr holds
( IT is cyclic iff the absurd of IT is cyclic );

:: deftheorem Def20 defines dualized QUANTAL1:def 20 :
for IT being non empty Girard-QuantaleStr holds
( IT is dualized iff the absurd of IT is dualizing );

theorem Th21: :: QUANTAL1:21
for Q being non empty Girard-QuantaleStr st LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} holds
( Q is cyclic & Q is dualized )
proof end;

registration
let A be non empty set ;
let b1, b2, b3 be BinOp of A;
let e1, e2 be Element of A;
cluster Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) -> non empty ;
coherence
not Girard-QuantaleStr(# A,b1,b2,b3,e1,e2 #) is empty ;
end;

registration
cluster non empty unital associative commutative Lattice-like complete right-distributive left-distributive strict cyclic dualized for Girard-QuantaleStr ;
existence
ex b1 being non empty Girard-QuantaleStr st
( b1 is associative & b1 is commutative & b1 is unital & b1 is left-distributive & b1 is right-distributive & b1 is complete & b1 is Lattice-like & b1 is cyclic & b1 is dualized & b1 is strict )
proof end;
end;

definition
mode Girard-Quantale is non empty unital associative Lattice-like complete right-distributive left-distributive cyclic dualized Girard-QuantaleStr ;
end;

definition
let G be Girard-QuantaleStr ;
func Bottom G -> Element of G equals :: QUANTAL1:def 21
 the absurd of G;
correctness
coherence
the absurd of G is Element of G;
;
end;

:: deftheorem defines Bottom QUANTAL1:def 21 :
for G being Girard-QuantaleStr holds Bottom G = the absurd of G;

definition
let G be non empty Girard-QuantaleStr ;
func Top G -> Element of G equals :: QUANTAL1:def 22
(Bottom G) -r> (Bottom G);
correctness
coherence
(Bottom G) -r> (Bottom G) is Element of G;
;
let a be Element of G;
func Bottom a -> Element of G equals :: QUANTAL1:def 23
a -r> (Bottom G);
correctness
coherence
a -r> (Bottom G) is Element of G;
;
end;

:: deftheorem defines Top QUANTAL1:def 22 :
for G being non empty Girard-QuantaleStr holds Top G = (Bottom G) -r> (Bottom G);

:: deftheorem defines Bottom QUANTAL1:def 23 :
for G being non empty Girard-QuantaleStr
for a being Element of G holds Bottom a = a -r> (Bottom G);

definition
let G be non empty Girard-QuantaleStr ;
func Negation G -> UnOp of G means :: QUANTAL1:def 24
 for a being Element of G holds it . a = Bottom a;
existence
ex b1 being UnOp of G st
for a being Element of G holds b1 . a = Bottom a
proof end;
uniqueness
for b1, b2 being UnOp of G st ( for a being Element of G holds b1 . a = Bottom a ) & ( for a being Element of G holds b2 . a = Bottom a ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Negation QUANTAL1:def 24 :
for G being non empty Girard-QuantaleStr
for b2 being UnOp of G holds
( b2 = Negation G iff for a being Element of G holds b2 . a = Bottom a );

definition
let G be non empty Girard-QuantaleStr ;
let u be UnOp of G;
func Bottom u -> UnOp of G equals :: QUANTAL1:def 25
(Negation G) * u;
correctness
coherence
(Negation G) * u is UnOp of G;
;
end;

:: deftheorem defines Bottom QUANTAL1:def 25 :
for G being non empty Girard-QuantaleStr
for u being UnOp of G holds Bottom u = (Negation G) * u;

definition
let G be non empty Girard-QuantaleStr ;
let o be BinOp of G;
func Bottom o -> BinOp of G equals :: QUANTAL1:def 26
(Negation G) * o;
correctness
coherence
(Negation G) * o is BinOp of G;
;
end;

:: deftheorem defines Bottom QUANTAL1:def 26 :
for G being non empty Girard-QuantaleStr
for o being BinOp of G holds Bottom o = (Negation G) * o;

theorem Th22: :: QUANTAL1:22
for Q being Girard-Quantale
for a being Element of Q holds Bottom (Bottom a) = a
proof end;

theorem :: QUANTAL1:23
for Q being Girard-Quantale
for a, b being Element of Q st a [= b holds
Bottom b [= Bottom a by Th13;

theorem Th24: :: QUANTAL1:24
for Q being Girard-Quantale
for X being set holds Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
proof end;

theorem Th25: :: QUANTAL1:25
for Q being Girard-Quantale
for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
proof end;

theorem Th26: :: QUANTAL1:26
for Q being Girard-Quantale
for a, b being Element of Q holds
( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )
proof end;

definition
let Q be Girard-Quantale;
let a, b be Element of Q;
func a delta b -> Element of Q equals :: QUANTAL1:def 27
 Bottom ((Bottom a) [*] (Bottom b));
correctness
coherence
Bottom ((Bottom a) [*] (Bottom b)) is Element of Q;
;
end;

:: deftheorem defines delta QUANTAL1:def 27 :
for Q being Girard-Quantale
for a, b being Element of Q holds a delta b = Bottom ((Bottom a) [*] (Bottom b));

theorem :: QUANTAL1:27
for Q being Girard-Quantale
for a being Element of Q
for X being set holds
( a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) & a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q) )
proof end;

theorem :: QUANTAL1:28
for Q being Girard-Quantale
for a being Element of Q
for X being set holds
( ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) & ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q) )
proof end;

theorem :: QUANTAL1:29
for Q being Girard-Quantale
for a, b, c being Element of Q holds
( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) )
proof end;

theorem :: QUANTAL1:30
for Q being Girard-Quantale
for a1, b1, a2, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds
a1 delta a2 [= b1 delta b2
proof end;

theorem :: QUANTAL1:31
for Q being Girard-Quantale
for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c)
proof end;

theorem Th32: :: QUANTAL1:32
for Q being Girard-Quantale
for a being Element of Q holds
( a [*] (Top Q) = a & (Top Q) [*] a = a )
proof end;

theorem :: QUANTAL1:33
for Q being Girard-Quantale
for a being Element of Q holds
( a delta (Bottom Q) = a & (Bottom Q) delta a = a )
proof end;

theorem :: QUANTAL1:34
for Q being Quantale
for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds
ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )
proof end;