:: 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]  }
proofend;

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]
proofend;

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 ) )
proofend;

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 ) )
proofend;

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;
attrX 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
proofend;

definition
attrc1 is strict ;
struct QuantaleStr  ->  LattStr , multMagma ;
aggrQuantaleStr(# carrier, L_join, L_meet, multF #) ->  QuantaleStr ;
end;

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

definition
attrc1 is strict ;
struct QuasiNetStr  ->  QuantaleStr , multLoopStr ;
aggrQuasiNetStr(# 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
proofend;
end;

definition
let IT be non empty multMagma ;
attrIT 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;
attrIT 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 ;
attrIT 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
proofend;
end;

definition
let IT be non empty QuantaleStr ;
attrIT 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);
attrIT 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);
attrIT 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) );
attrIT 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 )
proofend;

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 )
proofend;
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())
proofend;

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)
proofend;

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) )
proofend;

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 )
proofend;
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 )
proofend;
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 )
proofend;
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
proofend;

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 )
proofend;

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
proofend;

definition
let f be Function;
attrf 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
proofend;

definition
let L be non empty LattStr ;
let IT be UnOp of L;
attrIT is inflationary  means :: QUANTAL1:def 10
 for p being Element of L holds p [= IT . p;
attrIT is deflationary  means :: QUANTAL1:def 11
 for p being Element of L holds IT . p [= p;
attrIT is monotone  means :Def12: :: QUANTAL1:def 12
 for p, q being Element of L st p [= q holds
IT . p [= IT . q;
attrIT 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 )
proofend;
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) )
proofend;

definition
let Q be non empty QuantaleStr ;
let IT be UnOp of Q;
attrIT 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;
funca -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;
;
funca -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 )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;

definition
let Q be non empty QuantaleStr ;
let IT be Element of Q;
attrIT 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 );
attrIT 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 )
proofend;

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 )
proofend;

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 )
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

definition
attrc1 is strict ;
struct Girard-QuantaleStr  ->  QuasiNetStr ;
aggrGirard-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
proofend;
end;

definition
let IT be non empty Girard-QuantaleStr ;
attrIT is cyclic  means :Def19: :: QUANTAL1:def 19
 the absurd of IT is cyclic ;
attrIT 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 )
proofend;

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 )
proofend;
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
proofend;
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
proofend;
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
proofend;

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)
proofend;

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)
proofend;

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) )
proofend;

definition
let Q be Girard-Quantale;
let a, b be Element of Q;
funca 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) )
proofend;

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) )
proofend;

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) )
proofend;

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
proofend;

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)
proofend;

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

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 )
proofend;

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)) ) )
proofend;