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

scheme :: QUANTAL1:sch 1
DenestFraenkel{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> set , F₄( set ) -> Element of F₂(), P₁[ set ] } :

{ F₃(a) where a is Element of F₂() : a in { F₄(b) where b is Element of F₁() : P₁[b] } } = { F₃(F₄(a)) where a is Element of F₁() : P₁[a] }

proof end;

scheme :: QUANTAL1:sch 2
EmptyFraenkel{ F₁() -> non empty set , F₂( set ) -> set , P₁[ set ] } :

{ F₂(a) where a is Element of F₁() : P₁[a] } = {}

provided

A1: for a being Element of F₁() holds P₁[a]

proof end;

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

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

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

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

theorem :: 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 ) ) ;

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 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 c₁ 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 b₁ being QuantaleStr holds b₁ is empty

proof end;

end;

definition

attr c₁ 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 b₁ being QuasiNetStr holds b₁ 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 :: QUANTAL1:def 4
( IT is with_left-zero & IT is with_right-zero );

end;

:: deftheorem 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 b₁ being non empty multMagma st b₁ is with_zero holds
( b₁ is with_left-zero & b₁ is with_right-zero ) ;

cluster non empty with_left-zero with_right-zero -> non empty with_zero for multMagma ;

coherence
for b₁ being non empty multMagma st b₁ is with_left-zero & b₁ is with_right-zero holds
b₁ is with_zero ;

end;

registration

cluster non empty with_zero for multMagma ;

existence
ex b₁ being non empty multMagma st b₁ 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 Lattice-like complete unital associative commutative with_zero right-distributive left-distributive for QuantaleStr ;

existence
ex b₁ being non empty QuantaleStr st
( b₁ is associative & b₁ is commutative & b₁ is unital & b₁ is with_zero & b₁ is left-distributive & b₁ is right-distributive & b₁ is complete & b₁ is Lattice-like )

proof end;

end;

scheme :: QUANTAL1:sch 3
LUBFraenkelDistr{ F₁() -> non empty Lattice-like complete QuantaleStr , F₂( set , set ) -> Element of F₁(), F₃() -> set , F₄() -> set } :

"\/" ( { ("\/" ( { F₂(a,b) where b is Element of F₁() : b in F₄() } ,F₁())) where a is Element of F₁() : a in F₃() } ,F₁()) = "\/" ( { F₂(a,b) where a, b is Element of F₁() : ( a in F₃() & b in F₄() ) } ,F₁())

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 b₁ being non empty QuasiNetStr st
( b₁ is complete & b₁ 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 b₁ being non empty Lattice-like complete QuasiNetStr st b₁ is left-distributive & b₁ is right-distributive holds
( b₁ is times-continuous & b₁ is times-additive ) by Th5, Th6;

end;

registration

cluster non empty Lattice-like complete unital associative commutative with_left-zero with_zero right-distributive left-distributive for QuasiNetStr ;

existence
ex b₁ being non empty QuasiNetStr st
( b₁ is associative & b₁ is commutative & b₁ is unital & b₁ is with_zero & b₁ is with_left-zero & b₁ is left-distributive & b₁ is right-distributive & b₁ is complete & b₁ is Lattice-like )

proof end;

end;

definition

mode Quantale is non empty Lattice-like complete associative right-distributive left-distributive QuantaleStr ;
mode QuasiNet is non empty Lattice-like complete unital associative 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 ) by Th6;

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
by FUNCT_2:15;

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 :: 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 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 b₁ being UnOp of L st
( b₁ is inflationary & b₁ is deflationary & b₁ 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 :: 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 :: QUANTAL1:def 18
for a being Element of Q holds a -r> IT = a -l> IT;

end;

:: deftheorem 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 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 c₁ is strict ;
struct Girard-QuantaleStr -> QuasiNetStr ;
aggr Girard-QuantaleStr(# carrier, L_join, L_meet, multF, OneF, absurd #) -> Girard-QuantaleStr ;
sel absurd c₁ -> Element of the carrier of c₁;

end;

registration

cluster non empty for Girard-QuantaleStr ;

existence
not for b₁ being Girard-QuantaleStr holds b₁ 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 Lattice-like complete unital associative commutative right-distributive left-distributive strict cyclic dualized for Girard-QuantaleStr ;

existence
ex b₁ being non empty Girard-QuantaleStr st
( b₁ is associative & b₁ is commutative & b₁ is unital & b₁ is left-distributive & b₁ is right-distributive & b₁ is complete & b₁ is Lattice-like & b₁ is cyclic & b₁ is dualized & b₁ is strict )

proof end;

end;

definition

mode Girard-Quantale is non empty Lattice-like complete unital associative 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 b₁ being UnOp of G st
for a being Element of G holds b₁ . a = Bottom a

proof end;

uniqueness
for b₁, b₂ being UnOp of G st ( for a being Element of G holds b₁ . a = Bottom a ) & ( for a being Element of G holds b₂ . a = Bottom a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Negation QUANTAL1:def 24 :
for G being non empty Girard-QuantaleStr
for b₂ being UnOp of G holds
( b₂ = Negation G iff for a being Element of G holds b₂ . 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, a2, b1, 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;