:: QUANTAL1 semantic presentation
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
thus { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } c= { F3(F4(a)) where a is Element of F1() : P1[a] } :: according to XBOOLE_0:def_10 ::_thesis: { F3(F4(a)) where a is Element of F1() : P1[a] } c= { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } or x in { F3(F4(a)) where a is Element of F1() : P1[a] } )
assume x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } ; ::_thesis: x in { F3(F4(a)) where a is Element of F1() : P1[a] }
then consider a being Element of F2() such that
A1: x = F3(a) and
A2: a in { F4(b) where b is Element of F1() : P1[b] } ;
ex b being Element of F1() st
( a = F4(b) & P1[b] ) by A2;
hence x in { F3(F4(a)) where a is Element of F1() : P1[a] } by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(F4(a)) where a is Element of F1() : P1[a] } or x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } )
assume x in { F3(F4(a)) where a is Element of F1() : P1[a] } ; ::_thesis: x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } }
then consider a being Element of F1() such that
A3: x = F3(F4(a)) and
A4: P1[a] ;
F4(a) in { F4(b) where b is Element of F1() : P1[b] } by A4;
hence x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } by A3; ::_thesis: verum
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
assume not { F2(a) where a is Element of F1() : P1[a] } = {} ; ::_thesis: contradiction
then reconsider X = { F2(a) where a is Element of F1() : P1[a] } as non empty set ;
set x = the Element of X;
the Element of X in X ;
then ex a being Element of F1() st
( the Element of X = F2(a) & P1[a] ) ;
hence contradiction by A1; ::_thesis: verum
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
let L1, L2 be non empty LattStr ; ::_thesis: ( 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 #) implies 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 ) ) )
assume A1: 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 #) ; ::_thesis: 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 ) )
let a1, b1 be Element of L1; ::_thesis: 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 ) )
let a2, b2 be Element of L2; ::_thesis: ( a1 = a2 & b1 = b2 implies ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) )
assume A2: ( a1 = a2 & b1 = b2 ) ; ::_thesis: ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
thus a1 "\/" b1 = a2 "\/" b2 by A1, A2; ::_thesis: ( a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
thus a1 "/\" b1 = a2 "/\" b2 by A1, A2; ::_thesis: ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
A3: ( a2 "\/" b2 = b2 iff a2 [= b2 ) by LATTICES:def_3;
( a1 [= b1 iff a1 "\/" b1 = b1 ) by LATTICES:def_3;
hence ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) by A1, A2, A3; ::_thesis: verum
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
let L1, L2 be non empty LattStr ; ::_thesis: ( 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 #) implies 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 ) ) )
assume A1: 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 #) ; ::_thesis: 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 ) )
let a be Element of L1; ::_thesis: 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 ) )
let b be Element of L2; ::_thesis: 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 ) )
let X be set ; ::_thesis: ( a = b implies ( ( 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 ) ) )
assume A2: a = b ; ::_thesis: ( ( 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 ) )
thus ( a is_less_than X implies b is_less_than X ) ::_thesis: ( ( 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
assume A3: for c being Element of L1 st c in X holds
a [= c ; :: according to LATTICE3:def_16 ::_thesis: b is_less_than X
let c be Element of L2; :: according to LATTICE3:def_16 ::_thesis: ( not c in X or b [= c )
reconsider d = c as Element of L1 by A1;
assume c in X ; ::_thesis: b [= c
then a [= d by A3;
hence b [= c by A1, A2, Th1; ::_thesis: verum
end;
thus ( b is_less_than X implies a is_less_than X ) ::_thesis: ( a is_greater_than X iff b is_greater_than X )
proof
assume A4: for c being Element of L2 st c in X holds
b [= c ; :: according to LATTICE3:def_16 ::_thesis: a is_less_than X
let c be Element of L1; :: according to LATTICE3:def_16 ::_thesis: ( not c in X or a [= c )
reconsider d = c as Element of L2 by A1;
assume c in X ; ::_thesis: a [= c
then b [= d by A4;
hence a [= c by A1, A2, Th1; ::_thesis: verum
end;
thus ( a is_greater_than X implies b is_greater_than X ) ::_thesis: ( b is_greater_than X implies a is_greater_than X )
proof
assume A5: for c being Element of L1 st c in X holds
c [= a ; :: according to LATTICE3:def_17 ::_thesis: b is_greater_than X
let c be Element of L2; :: according to LATTICE3:def_17 ::_thesis: ( not c in X or c [= b )
reconsider d = c as Element of L1 by A1;
assume c in X ; ::_thesis: c [= b
then d [= a by A5;
hence c [= b by A1, A2, Th1; ::_thesis: verum
end;
assume A6: for c being Element of L2 st c in X holds
c [= b ; :: according to LATTICE3:def_17 ::_thesis: a is_greater_than X
let c be Element of L1; :: according to LATTICE3:def_17 ::_thesis: ( not c in X or c [= a )
reconsider d = c as Element of L2 by A1;
assume c in X ; ::_thesis: c [= a
then d [= b by A6;
hence c [= a by A1, A2, Th1; ::_thesis: verum
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;
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
proof
let L be non empty LattStr ; ::_thesis: for X being Subset of L st X is directed holds
not X is empty
let X be Subset of L; ::_thesis: ( X is directed implies not X is empty )
assume for Y being finite Subset of X ex x being Element of L st
( "\/" (Y,L) [= x & x in X ) ; :: according to QUANTAL1:def_1 ::_thesis: not X is empty
then ex x being Element of L st
( "\/" (({} X),L) [= x & x in X ) ;
hence not X is empty ; ::_thesis: verum
end;
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
proof
set A = the non empty set ;
set b1 = the BinOp of the non empty set ;
take QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) ; ::_thesis: not QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) is empty
thus not the carrier of QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
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
proof
set A = the non empty set ;
set b1 = the BinOp of the non empty set ;
set e = the Element of the non empty set ;
take QuasiNetStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) ; ::_thesis: not QuasiNetStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty
thus not the carrier of QuasiNetStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
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
proof
set x = the set ;
set f = the BinOp of { the set };
take G = multMagma(# { the set }, the BinOp of { the set } #); ::_thesis: G is with_zero
reconsider x = the set as Element of G by TARSKI:def_1;
thus G is with_left-zero :: according to QUANTAL1:def_4 ::_thesis: G is with_right-zero
proof
take x ; :: according to QUANTAL1:def_2 ::_thesis: for b being Element of G holds x * b = x
thus for b being Element of G holds x * b = x by TARSKI:def_1; ::_thesis: verum
end;
take x ; :: according to QUANTAL1:def_3 ::_thesis: for a being Element of G holds a * x = x
thus for a being Element of G holds a * x = x by TARSKI:def_1; ::_thesis: verum
end;
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 )
proof
set B = BooleLatt {};
let Q be non empty QuantaleStr ; ::_thesis: ( LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} implies ( 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 ) )
set a = the Element of Q;
assume A1: LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} ; ::_thesis: ( 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 )
A2: now__::_thesis:_for_x,_y_being_Element_of_Q_holds_x_=_y
let x, y be Element of Q; ::_thesis: x = y
A3: H1( BooleLatt {}) = {{}} by LATTICE3:def_1, ZFMISC_1:1;
then x = {} by A1, TARSKI:def_1;
hence x = y by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
thus H4(Q) is associative :: according to MONOID_0:def_12 ::_thesis: ( 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
let a, b, c be Element of Q; :: according to BINOP_1:def_3 ::_thesis: H4(Q) . (a,(H4(Q) . (b,c))) = H4(Q) . ((H4(Q) . (a,b)),c)
thus H4(Q) . (a,(H4(Q) . (b,c))) = H4(Q) . ((H4(Q) . (a,b)),c) by A2; ::_thesis: verum
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 H4(Q) is commutative :: according to MONOID_0:def_11 ::_thesis: ( Q is unital & Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
proof
let a, b be Element of Q; :: according to BINOP_1:def_2 ::_thesis: H4(Q) . (a,b) = H4(Q) . (b,a)
thus H4(Q) . (a,b) = H4(Q) . (b,a) by A2; ::_thesis: verum
end;
thus H4(Q) is having_a_unity :: according to MONOID_0:def_10 ::_thesis: ( Q is with_zero & Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
proof
take the Element of Q ; :: according to SETWISEO:def_2 ::_thesis: the Element of Q is_a_unity_wrt H4(Q)
thus the Element of Q is_a_left_unity_wrt H4(Q) :: according to BINOP_1:def_7 ::_thesis: the Element of Q is_a_right_unity_wrt H4(Q)
proof
let b be Element of Q; :: according to BINOP_1:def_16 ::_thesis: H4(Q) . ( the Element of Q,b) = b
thus H4(Q) . ( the Element of Q,b) = b by A2; ::_thesis: verum
end;
let b be Element of Q; :: according to BINOP_1:def_17 ::_thesis: H4(Q) . (b, the Element of Q) = b
thus H4(Q) . (b, the Element of Q) = b by A2; ::_thesis: verum
end;
thus Q is with_zero ::_thesis: ( Q is complete & Q is right-distributive & Q is left-distributive & Q is Lattice-like )
proof
thus Q is with_left-zero :: according to QUANTAL1:def_4 ::_thesis: Q is with_right-zero
proof
take the Element of Q ; :: according to QUANTAL1:def_2 ::_thesis: for b being Element of Q holds the Element of Q * b = the Element of Q
thus for b being Element of Q holds the Element of Q * b = the Element of Q by A2; ::_thesis: verum
end;
take the Element of Q ; :: according to QUANTAL1:def_3 ::_thesis: for a being Element of Q holds a * the Element of Q = the Element of Q
thus for a being Element of Q holds a * the Element of Q = the Element of Q by A2; ::_thesis: verum
end;
now__::_thesis:_for_X_being_set_ex_p9_being_Element_of_Q_st_
(_X_is_less_than_p9_&_(_for_r9_being_Element_of_Q_st_X_is_less_than_r9_holds_
p9_[=_r9_)_)
let X be set ; ::_thesis: ex p9 being Element of Q st
( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds
p9 [= r9 ) )
consider p being Element of (BooleLatt {}) such that
A5: X is_less_than p and
A6: for r being Element of (BooleLatt {}) st X is_less_than r holds
p [= r by LATTICE3:def_18;
reconsider p9 = p as Element of Q by A1;
take p9 = p9; ::_thesis: ( X is_less_than p9 & ( for r9 being Element of Q st X is_less_than r9 holds
p9 [= r9 ) )
thus X is_less_than p9 by A1, A5, Th2; ::_thesis: for r9 being Element of Q st X is_less_than r9 holds
p9 [= r9
let r9 be Element of Q; ::_thesis: ( X is_less_than r9 implies p9 [= r9 )
reconsider r = r9 as Element of (BooleLatt {}) by A1;
assume X is_less_than r9 ; ::_thesis: p9 [= r9
then X is_less_than r by A1, Th2;
then p [= r by A6;
hence p9 [= r9 by A1, Th1; ::_thesis: verum
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 ) ) ; :: according to LATTICE3:def_18 ::_thesis: ( Q is right-distributive & Q is left-distributive & Q is Lattice-like )
thus Q is right-distributive ::_thesis: ( Q is left-distributive & Q is Lattice-like )
proof
let a be Element of Q; :: according to QUANTAL1:def_5 ::_thesis: for X being set holds a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q)
let X be set ; ::_thesis: a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q)
thus a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) by A2; ::_thesis: verum
end;
thus Q is left-distributive ::_thesis: Q is Lattice-like
proof
let a be Element of Q; :: according to QUANTAL1:def_6 ::_thesis: for X being set holds ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q)
let X be set ; ::_thesis: ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q)
thus ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) by A2; ::_thesis: verum
end;
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 & Q is join-associative & Q is meet-absorbing & Q is meet-commutative & Q is meet-associative & Q is join-absorbing ) by A7, A4, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence Q is Lattice-like ; ::_thesis: verum
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
set B = BooleLatt {};
set b = the BinOp of (BooleLatt {});
take QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) ; ::_thesis: ( QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is associative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is commutative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is unital & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is with_zero & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is left-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is right-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is complete & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is Lattice-like )
thus ( QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is associative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is commutative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is unital & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is with_zero & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is left-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is right-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is complete & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is Lattice-like ) by Th4; ::_thesis: verum
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
set Q = F1();
set X = F3();
set Y = F4();
set Z = { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ;
set W = { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ;
set S = { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ;
A1: { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } = { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
proof
thus { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } c= { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } c= { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } or x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } )
assume x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ; ::_thesis: x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
then consider V being Subset of F1() such that
A2: x = "\/" V and
A3: V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ;
ex a being Element of F1() st
( V = { F2(a,b) where b is Element of F1() : b in F4() } & a in F3() ) by A3;
hence x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } or x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } )
assume x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ; ::_thesis: x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } }
then consider a being Element of F1() such that
A4: x = "\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1()) and
A5: a in F3() ;
A6: { F2(a,b) where b is Element of F1() : b in F4() } c= H1(F1())
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { F2(a,b) where b is Element of F1() : b in F4() } or y in H1(F1()) )
assume y in { F2(a,b) where b is Element of F1() : b in F4() } ; ::_thesis: y in H1(F1())
then ex b being Element of F1() st
( y = F2(a,b) & b in F4() ) ;
hence y in H1(F1()) ; ::_thesis: verum
end;
{ F2(a,c) where c is Element of F1() : c in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by A5;
hence x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } by A4, A6; ::_thesis: verum
end;
A7: { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } = union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
proof
thus { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } c= union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } :: according to XBOOLE_0:def_10 ::_thesis: union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } or x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } )
assume x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ; ::_thesis: x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
then consider a, b being Element of F1() such that
A8: ( x = F2(a,b) & a in F3() & b in F4() ) ;
( x in { F2(a,c) where c is Element of F1() : c in F4() } & { F2(a,d) where d is Element of F1() : d in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ) by A8;
hence x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } or x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } )
assume x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; ::_thesis: x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) }
then consider V being set such that
A9: x in V and
A10: V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } by TARSKI:def_4;
consider a being Element of F1() such that
A11: V = { F2(a,b) where b is Element of F1() : b in F4() } and
A12: a in F3() by A10;
ex b being Element of F1() st
( x = F2(a,b) & b in F4() ) by A9, A11;
hence x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } by A12; ::_thesis: verum
end;
{ { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= bool H1(F1())
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } or x in bool H1(F1()) )
assume x in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ; ::_thesis: x in bool H1(F1())
then consider a being Element of F1() such that
A13: x = { F2(a,b) where b is Element of F1() : b in F4() } and
a in F3() ;
x c= H1(F1())
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in H1(F1()) )
assume y in x ; ::_thesis: y in H1(F1())
then ex b being Element of F1() st
( y = F2(a,b) & b in F4() ) by A13;
hence y in H1(F1()) ; ::_thesis: verum
end;
hence x in bool H1(F1()) ; ::_thesis: verum
end;
hence "\/" ( { ("\/" ( { 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()) by A1, A7, LATTICE3:48; ::_thesis: verum
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
let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; ::_thesis: 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)
let X, Y be set ; ::_thesis: ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q)
deffunc H5( Element of Q) -> Element of the carrier of Q = $1 [*] ("\/" (Y,Q));
deffunc H6( Element of Q) -> Element of the carrier of Q = "\/" ( { ($1 [*] b) where b is Element of Q : b in Y } ,Q);
defpred S1[ set ] means $1 in X;
deffunc H7( Element of Q, Element of Q) -> Element of the carrier of Q = $1 [*] $2;
A1: for a being Element of Q holds H5(a) = H6(a) by Def5;
{ H5(c) where c is Element of Q : S1[c] } = { H6(a) where a is Element of Q : S1[a] } from FRAENKEL:sch_5(A1);
hence ("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { ("\/" ( { H7(a,b) where b is Element of Q : b in Y } ,Q)) where a is Element of Q : a in X } ,Q) by Def6
.= "\/" ( { H7(c,d) where c, d is Element of Q : ( c in X & d in Y ) } ,Q) from QUANTAL1:sch_3() ;
::_thesis: verum
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
let Q be non empty Lattice-like complete right-distributive left-distributive QuantaleStr ; ::_thesis: for a, b, c being Element of Q holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )
let a, b, c be Element of Q; ::_thesis: ( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) )
set X1 = { (d [*] c) where d is Element of Q : d in {a,b} } ;
set X2 = { (c [*] d) where d is Element of Q : d in {a,b} } ;
now__::_thesis:_for_x_being_set_holds_
(_(_(_x_=_a_[*]_c_or_x_=_b_[*]_c_)_implies_x_in__{__(d_[*]_c)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__)_&_(_not_x_in__{__(d_[*]_c)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__or_x_=_a_[*]_c_or_x_=_b_[*]_c_)_)
let x be set ; ::_thesis: ( ( ( x = a [*] c or x = b [*] c ) implies x in { (d [*] c) where d is Element of Q : d in {a,b} } ) & ( not x in { (d [*] c) where d is Element of Q : d in {a,b} } or x = a [*] c or x = b [*] c ) )
( a in {a,b} & b in {a,b} ) by TARSKI:def_2;
hence ( ( x = a [*] c or x = b [*] c ) implies x in { (d [*] c) where d is Element of Q : d in {a,b} } ) ; ::_thesis: ( not x in { (d [*] c) where d is Element of Q : d in {a,b} } or x = a [*] c or x = b [*] c )
assume x in { (d [*] c) where d is Element of Q : d in {a,b} } ; ::_thesis: ( x = a [*] c or x = b [*] c )
then ex d being Element of Q st
( x = d [*] c & d in {a,b} ) ;
hence ( x = a [*] c or x = b [*] c ) by TARSKI:def_2; ::_thesis: verum
end;
then A1: { (d [*] c) where d is Element of Q : d in {a,b} } = {(a [*] c),(b [*] c)} by TARSKI:def_2;
now__::_thesis:_for_x_being_set_holds_
(_(_(_x_=_c_[*]_a_or_x_=_c_[*]_b_)_implies_x_in__{__(c_[*]_d)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__)_&_(_not_x_in__{__(c_[*]_d)_where_d_is_Element_of_Q_:_d_in_{a,b}__}__or_x_=_c_[*]_a_or_x_=_c_[*]_b_)_)
let x be set ; ::_thesis: ( ( ( x = c [*] a or x = c [*] b ) implies x in { (c [*] d) where d is Element of Q : d in {a,b} } ) & ( not x in { (c [*] d) where d is Element of Q : d in {a,b} } or x = c [*] a or x = c [*] b ) )
( a in {a,b} & b in {a,b} ) by TARSKI:def_2;
hence ( ( x = c [*] a or x = c [*] b ) implies x in { (c [*] d) where d is Element of Q : d in {a,b} } ) ; ::_thesis: ( not x in { (c [*] d) where d is Element of Q : d in {a,b} } or x = c [*] a or x = c [*] b )
assume x in { (c [*] d) where d is Element of Q : d in {a,b} } ; ::_thesis: ( x = c [*] a or x = c [*] b )
then ex d being Element of Q st
( x = c [*] d & d in {a,b} ) ;
hence ( x = c [*] a or x = c [*] b ) by TARSKI:def_2; ::_thesis: verum
end;
then A2: { (c [*] d) where d is Element of Q : d in {a,b} } = {(c [*] a),(c [*] b)} by TARSKI:def_2;
A3: a "\/" b = "\/" {a,b} by LATTICE3:43;
then (a "\/" b) [*] c = "\/" ( { (d [*] c) where d is Element of Q : d in {a,b} } ,Q) by Def6;
hence (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) by A1, LATTICE3:43; ::_thesis: c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b)
c [*] (a "\/" b) = "\/" ( { (c [*] d) where d is Element of Q : d in {a,b} } ,Q) by A3, Def5;
hence c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) by A2, LATTICE3:43; ::_thesis: verum
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
set B = BooleLatt {};
set e = the Element of (BooleLatt {});
set b = the BinOp of (BooleLatt {});
take QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) ; ::_thesis: ( QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like )
thus ( QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like ) by Th4; ::_thesis: verum
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
let Q be non empty Lattice-like complete QuasiNetStr ; ::_thesis: ( Q is left-distributive & Q is right-distributive implies ( Q is times-continuous & Q is times-additive ) )
assume ( Q is left-distributive & Q is right-distributive ) ; ::_thesis: ( Q is times-continuous & Q is times-additive )
hence ( ( for X, Y being Subset of Q st X is directed & Y is directed holds
("\/" (X,Q)) [*] ("\/" (Y,Q)) = "\/" ( { (a [*] b) where a, b is Element of Q : ( a in X & b in Y ) } ,Q) ) & ( for a, b, c being Element of Q holds
( (a "\/" b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a "\/" b) = (c [*] a) "\/" (c [*] b) ) ) ) by Th5, Th6; :: according to QUANTAL1:def_7,QUANTAL1:def_8 ::_thesis: verum
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
set B = BooleLatt {};
set e = the Element of (BooleLatt {});
set b = the BinOp of (BooleLatt {});
take Q = QuasiNetStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #); ::_thesis: ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is with_left-zero & Q is left-distributive & Q is right-distributive & Q is complete & Q is Lattice-like )
( Q is with_zero & Q is unital ) by Th4;
hence ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is with_left-zero & Q is left-distributive & Q is right-distributive & Q is complete & Q is Lattice-like ) by Th4; ::_thesis: verum
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
defpred S1[ set ] means $1 in {} ;
let Q be non empty unital QuasiNetStr ; ::_thesis: ( Q is Quantale implies Q is BlikleNet )
assume Q is Quantale ; ::_thesis: Q is BlikleNet
then reconsider Q9 = Q as Quantale ;
A1: Bottom Q9 = "\/" ({},Q9) by LATTICE3:49;
A2: for c being Element of Q9 holds not S1[c] ;
Q9 is with_zero
proof
hereby :: according to QUANTAL1:def_2,QUANTAL1:def_4 ::_thesis: Q9 is with_right-zero
reconsider a = Bottom Q9 as Element of Q9 ;
take a = a; ::_thesis: for b being Element of Q9 holds a [*] b = a
let b be Element of Q9; ::_thesis: a [*] b = a
deffunc H5( Element of Q9) -> Element of the carrier of Q9 = $1 [*] b;
{ H5(c) where c is Element of Q9 : S1[c] } = {} from QUANTAL1:sch_2(A2);
hence a [*] b = a by A1, Def6; ::_thesis: verum
end;
take Bottom Q9 ; :: according to QUANTAL1:def_3 ::_thesis: for a being Element of Q9 holds a * (Bottom Q9) = Bottom Q9
let a be Element of Q9; ::_thesis: a * (Bottom Q9) = Bottom Q9
deffunc H5( Element of Q9) -> Element of the carrier of Q9 = a [*] $1;
{ H5(c) where c is Element of Q9 : S1[c] } = {} from QUANTAL1:sch_2(A2);
hence a * (Bottom Q9) = Bottom Q9 by A1, Def5; ::_thesis: verum
end;
hence Q is BlikleNet ; ::_thesis: verum
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
let Q be Quantale; ::_thesis: for a, b, c being Element of Q st a [= b holds
( a [*] c [= b [*] c & c [*] a [= c [*] b )
let a, b, c be Element of Q; ::_thesis: ( a [= b implies ( a [*] c [= b [*] c & c [*] a [= c [*] b ) )
assume A1: a [= b ; ::_thesis: ( a [*] c [= b [*] c & c [*] a [= c [*] b )
thus (a [*] c) "\/" (b [*] c) = (a "\/" b) [*] c by Th6
.= b [*] c by A1, LATTICES:def_3 ; :: according to LATTICES:def_3 ::_thesis: c [*] a [= c [*] b
thus (c [*] a) "\/" (c [*] b) = c [*] (a "\/" b) by Th6
.= c [*] b by A1, LATTICES:def_3 ; :: according to LATTICES:def_3 ::_thesis: verum
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
let Q be Quantale; ::_thesis: for a, b, c, d being Element of Q st a [= b & c [= d holds
a [*] c [= b [*] d
let a, b, c, d be Element of Q; ::_thesis: ( a [= b & c [= d implies a [*] c [= b [*] d )
assume ( a [= b & c [= d ) ; ::_thesis: a [*] c [= b [*] d
then ( a [*] c [= b [*] c & b [*] c [= b [*] d ) by Th8;
hence a [*] c [= b [*] d by LATTICES:7; ::_thesis: verum
end;
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
proof
let A be non empty set ; ::_thesis: for f being UnOp of A st f is idempotent holds
for a being Element of A holds f . (f . a) = f . a
let f be UnOp of A; ::_thesis: ( f is idempotent implies for a being Element of A holds f . (f . a) = f . a )
assume f * f = f ; :: according to QUANTAL1:def_9 ::_thesis: for a being Element of A holds f . (f . a) = f . a
hence for a being Element of A holds f . (f . a) = f . a by FUNCT_2:15; ::_thesis: verum
end;
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 )
proof
reconsider f = id the carrier of L as UnOp of L ;
take f ; ::_thesis: ( f is inflationary & f is deflationary & f is monotone )
thus f is inflationary ::_thesis: ( f is deflationary & f is monotone )
proof
let p be Element of L; :: according to QUANTAL1:def_10 ::_thesis: p [= f . p
p [= p ;
hence p [= f . p by FUNCT_1:17; ::_thesis: verum
end;
thus f is deflationary ::_thesis: f is monotone
proof
let p be Element of L; :: according to QUANTAL1:def_11 ::_thesis: f . p [= p
p [= p ;
hence f . p [= p by FUNCT_1:17; ::_thesis: verum
end;
let p, q be Element of L; :: according to QUANTAL1:def_12 ::_thesis: ( p [= q implies f . p [= f . q )
f . p = p by FUNCT_1:17;
hence ( p [= q implies f . p [= f . q ) by FUNCT_1:17; ::_thesis: verum
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
let L be complete Lattice; ::_thesis: 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) )
let j be UnOp of L; ::_thesis: ( j is monotone implies ( 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) ) )
assume A1: j is monotone ; ::_thesis: ( 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) )
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) ) ::_thesis: ( ( for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ) implies j is \/-distributive )
proof
assume A2: for X being Subset of L holds j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) ; :: according to QUANTAL1:def_13 ::_thesis: 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; ::_thesis: j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L)
{ (j . a) where a is Element of L : a in X } is_less_than j . ("\/" X)
proof
let x be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not x in { (j . a) where a is Element of L : a in X } or x [= j . ("\/" X) )
assume x in { (j . a) where a is Element of L : a in X } ; ::_thesis: x [= j . ("\/" 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 x [= j . ("\/" X) by A1, A3, Def12; ::_thesis: verum
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 j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A5, LATTICES:8; ::_thesis: verum
end;
assume A6: for X being Subset of L holds j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) ; ::_thesis: j is \/-distributive
let X be Subset of L; :: according to QUANTAL1:def_13 ::_thesis: j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L)
j . ("\/" X) [= j . ("\/" X) ;
hence j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A6; ::_thesis: verum
end;
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 )
proof
let Q be Quantale; ::_thesis: for a, b, c being Element of Q holds
( a [*] b [= c iff b [= a -l> c )
let a, b, c be Element of Q; ::_thesis: ( a [*] b [= c iff b [= a -l> c )
set X = { d where d is Element of Q : a [*] d [= c } ;
{ d where d is Element of Q : a [*] d [= c } c= H1(Q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : a [*] d [= c } or x in H1(Q) )
assume x in { d where d is Element of Q : a [*] d [= c } ; ::_thesis: x in H1(Q)
then ex d being Element of Q st
( x = d & a [*] d [= c ) ;
hence x in H1(Q) ; ::_thesis: verum
end;
then reconsider X = { d where d is Element of Q : a [*] d [= c } as Subset of Q ;
thus ( a [*] b [= c implies b [= a -l> c ) ::_thesis: ( b [= a -l> c implies a [*] b [= c )
proof
assume a [*] b [= c ; ::_thesis: b [= a -l> c
then b in X ;
hence b [= a -l> c by LATTICE3:38; ::_thesis: verum
end;
deffunc H5( Element of Q) -> Element of the carrier of Q = a [*] $1;
defpred S1[ set ] means $1 in X;
defpred S2[ Element of Q] means a [*] $1 [= c;
assume b [= a -l> c ; ::_thesis: a [*] b [= c
then A1: a [*] b [= a [*] ("\/" X) by Th8;
now__::_thesis:_for_d_being_Element_of_Q_st_d_in_X_holds_
a_[*]_d_[=_c
let d be Element of Q; ::_thesis: ( d in X implies a [*] d [= c )
assume d in X ; ::_thesis: a [*] d [= c
then ex d1 being Element of Q st
( d = d1 & a [*] d1 [= c ) ;
hence a [*] d [= c ; ::_thesis: verum
end;
then A2: for d being Element of Q holds
( S1[d] iff S2[d] ) ;
A3: { H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from FRAENKEL:sch_3(A2);
A4: { (a [*] d) where d is Element of Q : d in X } is_less_than c
proof
let d1 be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not d1 in { (a [*] d) where d is Element of Q : d in X } or d1 [= c )
assume d1 in { (a [*] d) where d is Element of Q : d in X } ; ::_thesis: d1 [= c
then ex d2 being Element of Q st
( d1 = a [*] d2 & a [*] d2 [= c ) by A3;
hence d1 [= c ; ::_thesis: verum
end;
a [*] ("\/" X) = "\/" ( { (a [*] d) where d is Element of Q : d in X } ,Q) by Def5;
then a [*] ("\/" X) [= c by A4, LATTICE3:def_21;
hence a [*] b [= c by A1, LATTICES:7; ::_thesis: verum
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
let Q be Quantale; ::_thesis: for a, b, c being Element of Q holds
( a [*] b [= c iff a [= b -r> c )
let a, b, c be Element of Q; ::_thesis: ( a [*] b [= c iff a [= b -r> c )
set X = { d where d is Element of Q : d [*] b [= c } ;
{ d where d is Element of Q : d [*] b [= c } c= H1(Q)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : d [*] b [= c } or x in H1(Q) )
assume x in { d where d is Element of Q : d [*] b [= c } ; ::_thesis: x in H1(Q)
then ex d being Element of Q st
( x = d & d [*] b [= c ) ;
hence x in H1(Q) ; ::_thesis: verum
end;
then reconsider X = { d where d is Element of Q : d [*] b [= c } as Subset of Q ;
thus ( a [*] b [= c implies a [= b -r> c ) ::_thesis: ( a [= b -r> c implies a [*] b [= c )
proof
assume a [*] b [= c ; ::_thesis: a [= b -r> c
then a in X ;
hence a [= b -r> c by LATTICE3:38; ::_thesis: verum
end;
deffunc H5( Element of Q) -> Element of the carrier of Q = $1 [*] b;
defpred S1[ set ] means $1 in X;
defpred S2[ Element of Q] means $1 [*] b [= c;
assume a [= b -r> c ; ::_thesis: a [*] b [= c
then A1: a [*] b [= ("\/" X) [*] b by Th8;
now__::_thesis:_for_d_being_Element_of_Q_st_d_in_X_holds_
d_[*]_b_[=_c
let d be Element of Q; ::_thesis: ( d in X implies d [*] b [= c )
assume d in X ; ::_thesis: d [*] b [= c
then ex d1 being Element of Q st
( d = d1 & d1 [*] b [= c ) ;
hence d [*] b [= c ; ::_thesis: verum
end;
then A2: for d being Element of Q holds
( S1[d] iff S2[d] ) ;
A3: { H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from FRAENKEL:sch_3(A2);
A4: { (d [*] b) where d is Element of Q : d in X } is_less_than c
proof
let d1 be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not d1 in { (d [*] b) where d is Element of Q : d in X } or d1 [= c )
assume d1 in { (d [*] b) where d is Element of Q : d in X } ; ::_thesis: d1 [= c
then ex d2 being Element of Q st
( d1 = d2 [*] b & d2 [*] b [= c ) by A3;
hence d1 [= c ; ::_thesis: verum
end;
("\/" X) [*] b = "\/" ( { (d [*] b) where d is Element of Q : d in X } ,Q) by Def6;
then ("\/" X) [*] b [= c by A4, LATTICE3:def_21;
hence a [*] b [= c by A1, LATTICES:7; ::_thesis: verum
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
let Q be Quantale; ::_thesis: for s, a, b being Element of Q st a [= b holds
( b -r> s [= a -r> s & b -l> s [= a -l> s )
let s, a, b be Element of Q; ::_thesis: ( a [= b implies ( b -r> s [= a -r> s & b -l> s [= a -l> s ) )
assume A1: a [= b ; ::_thesis: ( b -r> s [= a -r> s & b -l> s [= a -l> s )
{ 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : d [*] b [= s } or x in { c where c is Element of Q : c [*] a [= s } )
assume x in { d where d is Element of Q : d [*] b [= s } ; ::_thesis: x in { c where c is Element of Q : c [*] a [= 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 x in { c where c is Element of Q : c [*] a [= s } by A2; ::_thesis: verum
end;
hence b -r> s [= a -r> s by LATTICE3:45; ::_thesis: b -l> s [= a -l> s
{ 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d where d is Element of Q : b [*] d [= s } or x in { c where c is Element of Q : a [*] c [= s } )
assume x in { d where d is Element of Q : b [*] d [= s } ; ::_thesis: x in { c where c is Element of Q : a [*] c [= 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 x in { c where c is Element of Q : a [*] c [= s } by A4; ::_thesis: verum
end;
hence b -l> s [= a -l> s by LATTICE3:45; ::_thesis: verum
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
let Q be Quantale; ::_thesis: 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
let s be Element of Q; ::_thesis: 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
let j be UnOp of Q; ::_thesis: ( ( for a being Element of Q holds j . a = (a -r> s) -r> s ) implies j is monotone )
assume A1: for a being Element of Q holds j . a = (a -r> s) -r> s ; ::_thesis: j is monotone
thus j is monotone ::_thesis: verum
proof
let a, b be Element of Q; :: according to QUANTAL1:def_12 ::_thesis: ( a [= b implies j . a [= j . b )
assume a [= b ; ::_thesis: j . a [= j . 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 j . a [= j . b by A1, A2; ::_thesis: verum
end;
end;
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 )
proof
let Q be Quantale; ::_thesis: 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 )
let c be Element of Q; ::_thesis: ( c is cyclic iff for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c )
thus ( c is cyclic implies for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c ) ::_thesis: ( ( for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c ) implies c is cyclic )
proof
assume A1: for a being Element of Q holds a -r> c = a -l> c ; :: according to QUANTAL1:def_18 ::_thesis: for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c
let a, b be Element of Q; ::_thesis: ( a [*] b [= c implies b [*] a [= c )
assume a [*] b [= c ; ::_thesis: b [*] a [= c
then a [= b -r> c by Th12;
then a [= b -l> c by A1;
hence b [*] a [= c by Th11; ::_thesis: verum
end;
assume A2: for a, b being Element of Q st a [*] b [= c holds
b [*] a [= c ; ::_thesis: c is cyclic
let a be Element of Q; :: according to QUANTAL1:def_18 ::_thesis: a -r> c = a -l> c
set X1 = { d1 where d1 is Element of Q : d1 [*] a [= c } ;
set X2 = { d2 where d2 is Element of Q : a [*] d2 [= c } ;
{ d1 where d1 is Element of Q : d1 [*] a [= c } = { d2 where d2 is Element of Q : a [*] d2 [= c }
proof
thus { d1 where d1 is Element of Q : d1 [*] a [= c } c= { d2 where d2 is Element of Q : a [*] d2 [= c } :: according to XBOOLE_0:def_10 ::_thesis: { d2 where d2 is Element of Q : a [*] d2 [= c } c= { d1 where d1 is Element of Q : d1 [*] a [= c }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d1 where d1 is Element of Q : d1 [*] a [= c } or x in { d2 where d2 is Element of Q : a [*] d2 [= c } )
assume x in { d1 where d1 is Element of Q : d1 [*] a [= c } ; ::_thesis: x in { d2 where d2 is Element of Q : a [*] d2 [= c }
then consider d being Element of Q such that
A3: x = d and
A4: d [*] a [= c ;
a [*] d [= c by A2, A4;
hence x in { d2 where d2 is Element of Q : a [*] d2 [= c } by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { d2 where d2 is Element of Q : a [*] d2 [= c } or x in { d1 where d1 is Element of Q : d1 [*] a [= c } )
assume x in { d2 where d2 is Element of Q : a [*] d2 [= c } ; ::_thesis: x in { d1 where d1 is Element of Q : d1 [*] a [= c }
then consider d being Element of Q such that
A5: x = d and
A6: a [*] d [= c ;
d [*] a [= c by A2, A6;
hence x in { d1 where d1 is Element of Q : d1 [*] a [= c } by A5; ::_thesis: verum
end;
hence a -r> c = a -l> c ; ::_thesis: verum
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
let Q be Quantale; ::_thesis: for s, a being Element of Q st s is cyclic holds
( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )
let s, a be Element of Q; ::_thesis: ( s is cyclic implies ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s ) )
assume A1: s is cyclic ; ::_thesis: ( a [= (a -r> s) -r> s & a [= (a -l> s) -l> s )
A2: { b where b is Element of Q : b [= a } c= { c where c is Element of Q : c [*] (a -r> s) [= s }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Element of Q : b [= a } or x in { c where c is Element of Q : c [*] (a -r> s) [= s } )
assume x in { b where b is Element of Q : b [= a } ; ::_thesis: x in { c where c is Element of Q : c [*] (a -r> s) [= s }
then consider b being Element of Q 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 x in { c where c is Element of Q : c [*] (a -r> s) [= s } by A3; ::_thesis: verum
end;
A6: { b where b is Element of Q : b [= a } c= { c where c is Element of Q : (a -l> s) [*] c [= s }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { b where b is Element of Q : b [= a } or x in { c where c is Element of Q : (a -l> s) [*] c [= s } )
assume x in { b where b is Element of Q : b [= a } ; ::_thesis: x in { c where c is Element of Q : (a -l> s) [*] c [= s }
then consider b being Element of Q 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 x in { c where c is Element of Q : (a -l> s) [*] c [= s } by A7; ::_thesis: verum
end;
a = "\/" ( { d where d is Element of Q : d [= a } ,Q) by LATTICE3:44;
hence a [= (a -r> s) -r> s by A2, LATTICE3:45; ::_thesis: a [= (a -l> s) -l> s
a = "\/" ( { d where d is Element of Q : d [= a } ,Q) by LATTICE3:44;
hence a [= (a -l> s) -l> s by A6, LATTICE3:45; ::_thesis: verum
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
let Q be Quantale; ::_thesis: 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 )
let s, a be Element of Q; ::_thesis: ( s is cyclic implies ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) )
assume A1: s is cyclic ; ::_thesis: ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s )
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 ( a -r> s = ((a -r> s) -r> s) -r> s & a -l> s = ((a -l> s) -l> s) -l> s ) by A2, A3, LATTICES:8; ::_thesis: verum
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
let Q be Quantale; ::_thesis: 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
let s, a, b be Element of Q; ::_thesis: ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s
deffunc H5( Element of Q) -> set = { c where c is Element of Q : c [*] ($1 -r> s) [= s } ;
A1: { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } c= H5(a [*] b)
proof
defpred S1[ Element of Q] means $1 [*] (a [*] b) [= s;
deffunc H6( Element of Q) -> Element of Q = $1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } or x in H5(a [*] b) )
set A = { H6(c) where c is Element of Q : S1[c] } ;
assume x in { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } ; ::_thesis: x in H5(a [*] b)
then consider a9, b9 being Element of Q such that
A2: x = a9 [*] b9 and
A3: a9 in H5(a) and
A4: b9 in H5(b) ;
deffunc H7( Element of Q) -> Element of the carrier of Q = (a9 [*] b9) [*] $1;
set B = { H7(H6(c)) where c is Element of Q : S1[c] } ;
A5: ex c being Element of Q st
( b9 = c & c [*] (b -r> s) [= s ) by A4;
A6: ex c being Element of Q st
( a9 = c & c [*] (a -r> s) [= s ) by A3;
A7: { H7(H6(c)) where c is Element of Q : S1[c] } is_less_than s
proof
let d be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not d in { H7(H6(c)) where c is Element of Q : S1[c] } or d [= s )
assume d in { H7(H6(c)) where c is Element of Q : S1[c] } ; ::_thesis: d [= s
then consider c being Element of Q 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; ::_thesis: verum
end;
{ H7(c) where c is Element of Q : c in { H6(c) where c is Element of Q : S1[c] } } = { H7(H6(c)) where c is Element of Q : S1[c] } from QUANTAL1:sch_1();
then (a9 [*] b9) [*] ((a [*] b) -r> s) = "\/" ( { H7(H6(c)) where c is Element of Q : S1[c] } ,Q) by Def5;
then (a9 [*] b9) [*] ((a [*] b) -r> s) [= s by A7, LATTICE3:def_21;
hence x in H5(a [*] b) by A2; ::_thesis: verum
end;
((a -r> s) -r> s) [*] ((b -r> s) -r> s) = "\/" ( { (a9 [*] b9) where a9, b9 is Element of Q : ( a9 in H5(a) & b9 in H5(b) ) } ,Q) by Th5;
hence ((a -r> s) -r> s) [*] ((b -r> s) -r> s) [= ((a [*] b) -r> s) -r> s by A1, LATTICE3:45; ::_thesis: verum
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
let Q be Quantale; ::_thesis: 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 )
let D be Element of Q; ::_thesis: ( 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 ) )
set I = D -l> D;
set J = D -r> D;
assume A1: for a being Element of Q holds
( (a -r> D) -l> D = a & (a -l> D) -r> D = a ) ; :: according to QUANTAL1:def_17 ::_thesis: ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
A2: now__::_thesis:_for_a_being_Element_of_Q_holds_
(_a_[*]_(D_-l>_D)_=_a_&_(D_-r>_D)_[*]_a_=_a_)
deffunc H5( set ) -> set = $1;
let a be Element of Q; ::_thesis: ( a [*] (D -l> D) = a & (D -r> D) [*] a = a )
defpred S1[ Element of Q] means $1 [*] (a [*] (D -l> D)) [= D;
defpred S2[ Element of Q] means $1 [*] a [= D;
defpred S3[ Element of Q] means ((D -r> D) [*] a) [*] $1 [= D;
defpred S4[ Element of Q] means a [*] $1 [= D;
A3: for b being Element of Q holds
( S1[b] iff S2[b] )
proof
let b be Element of Q; ::_thesis: ( S1[b] iff S2[b] )
( b [*] (a [*] (D -l> D)) = (b [*] a) [*] (D -l> D) & (D -l> D) -r> D = D ) by A1, GROUP_1:def_3;
hence ( S1[b] iff S2[b] ) by Th12; ::_thesis: verum
end;
A4: { H5(b) where b is Element of Q : S1[b] } = { H5(c) where c is Element of Q : S2[c] } from FRAENKEL:sch_3(A3);
thus a [*] (D -l> D) = ((a [*] (D -l> D)) -r> D) -l> D by A1
.= (a -r> D) -l> D by A4
.= a by A1 ; ::_thesis: (D -r> D) [*] a = a
A5: for b being Element of Q holds
( S3[b] iff S4[b] )
proof
let b be Element of Q; ::_thesis: ( S3[b] iff S4[b] )
( (D -r> D) [*] (a [*] b) = ((D -r> D) [*] a) [*] b & (D -r> D) -l> D = D ) by A1, GROUP_1:def_3;
hence ( S3[b] iff S4[b] ) by Th11; ::_thesis: verum
end;
A6: { H5(b) where b is Element of Q : S3[b] } = { H5(c) where c is Element of Q : S4[c] } from FRAENKEL:sch_3(A5);
thus (D -r> D) [*] a = (((D -r> D) [*] a) -l> D) -r> D by A1
.= (a -l> D) -r> D by A6
.= a by A1 ; ::_thesis: verum
end;
A7: D -l> D is_a_right_unity_wrt H4(Q)
proof
let a be Element of Q; :: according to BINOP_1:def_17 ::_thesis: H4(Q) . (a,(D -l> D)) = a
thus H4(Q) . (a,(D -l> D)) = a [*] (D -l> D)
.= a by A2 ; ::_thesis: verum
end;
A8: D -l> D = (D -r> D) [*] (D -l> D) by A2;
D -l> D is_a_left_unity_wrt H4(Q)
proof
let a be Element of Q; :: according to BINOP_1:def_16 ::_thesis: H4(Q) . ((D -l> D),a) = a
thus H4(Q) . ((D -l> D),a) = (D -r> D) [*] a by A2, A8
.= a by A2 ; ::_thesis: verum
end;
then A9: D -l> D is_a_unity_wrt H4(Q) by A7, BINOP_1:def_7;
hence H4(Q) is having_a_unity by SETWISEO:def_2; :: according to MONOID_0:def_10 ::_thesis: ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
D -r> D = (D -r> D) [*] (D -l> D) by A2;
hence ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) by A8, A9, BINOP_1:def_8; ::_thesis: verum
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
let Q be Quantale; ::_thesis: 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 )
let a, b, c be Element of Q; ::_thesis: ( a is dualizing implies ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a ) )
deffunc H5( set ) -> set = $1;
defpred S1[ Element of Q] means $1 [*] b [= c;
defpred S2[ Element of Q] means $1 [*] (b [*] (c -l> a)) [= a;
defpred S3[ Element of Q] means b [*] $1 [= c;
defpred S4[ Element of Q] means ((c -r> a) [*] b) [*] $1 [= a;
assume A1: for d being Element of Q holds
( (d -r> a) -l> a = d & (d -l> a) -r> a = d ) ; :: according to QUANTAL1:def_17 ::_thesis: ( b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a )
then A2: c = (c -l> a) -r> a ;
A3: for d being Element of Q holds
( S1[d] iff S2[d] )
proof
let d be Element of Q; ::_thesis: ( S1[d] iff S2[d] )
d [*] (b [*] (c -l> a)) = (d [*] b) [*] (c -l> a) by GROUP_1:def_3;
hence ( S1[d] iff S2[d] ) by A2, Th12; ::_thesis: verum
end;
{ H5(d1) where d1 is Element of Q : S1[d1] } = { H5(d2) where d2 is Element of Q : S2[d2] } from FRAENKEL:sch_3(A3);
hence b -r> c = (b [*] (c -l> a)) -r> a ; ::_thesis: b -l> c = ((c -r> a) [*] b) -l> a
A4: c = (c -r> a) -l> a by A1;
A5: for d being Element of Q holds
( S3[d] iff S4[d] )
proof
let d be Element of Q; ::_thesis: ( S3[d] iff S4[d] )
((c -r> a) [*] b) [*] d = (c -r> a) [*] (b [*] d) by GROUP_1:def_3;
hence ( S3[d] iff S4[d] ) by A4, Th11; ::_thesis: verum
end;
{ H5(d1) where d1 is Element of Q : S3[d1] } = { H5(d2) where d2 is Element of Q : S4[d2] } from FRAENKEL:sch_3(A5);
hence b -l> c = ((c -r> a) [*] b) -l> a ; ::_thesis: verum
end;
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
proof
set A = the non empty set ;
set b1 = the BinOp of the non empty set ;
set e1 = the Element of the non empty set ;
take Girard-QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Element of the non empty set #) ; ::_thesis: not Girard-QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty
thus not the carrier of Girard-QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
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 )
proof
let Q be non empty Girard-QuantaleStr ; ::_thesis: ( LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} implies ( Q is cyclic & Q is dualized ) )
set c = the absurd of Q;
assume LattStr(# the carrier of Q, the L_join of Q, the L_meet of Q #) = BooleLatt {} ; ::_thesis: ( Q is cyclic & Q is dualized )
then A1: H1(Q) = {{}} by LATTICE3:def_1, ZFMISC_1:1;
thus Q is cyclic ::_thesis: Q is dualized
proof
let a be Element of Q; :: according to QUANTAL1:def_18,QUANTAL1:def_19 ::_thesis: a -r> the absurd of Q = a -l> the absurd of Q
a -r> the absurd of Q = {} by A1, TARSKI:def_1;
hence a -r> the absurd of Q = a -l> the absurd of Q by A1, TARSKI:def_1; ::_thesis: verum
end;
let a be Element of Q; :: according to QUANTAL1:def_17,QUANTAL1:def_20 ::_thesis: ( (a -r> the absurd of Q) -l> the absurd of Q = a & (a -l> the absurd of Q) -r> the absurd of Q = a )
( (a -r> the absurd of Q) -l> the absurd of Q = {} & (a -l> the absurd of Q) -r> the absurd of Q = {} ) by A1, TARSKI:def_1;
hence ( (a -r> the absurd of Q) -l> the absurd of Q = a & (a -l> the absurd of Q) -r> the absurd of Q = a ) by A1, TARSKI:def_1; ::_thesis: verum
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
set B = BooleLatt {};
set b = the BinOp of (BooleLatt {});
set e = the Element of (BooleLatt {});
take Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) ; ::_thesis: ( Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is associative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is commutative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is unital & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is left-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is right-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is cyclic & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is dualized & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is strict )
thus ( Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is associative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is commutative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is unital & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is left-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is right-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is complete & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is Lattice-like & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is cyclic & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is dualized & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}), the Element of (BooleLatt {}) #) is strict ) by Th4, Th21; ::_thesis: verum
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
deffunc H5( Element of G) -> 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 = H5(a) from FUNCT_2:sch_4();
reconsider f = f as UnOp of G ;
take f ; ::_thesis: for a being Element of G holds f . a = Bottom a
thus for a being Element of G holds f . a = Bottom a by A1; ::_thesis: verum
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
let f1, f2 be UnOp of G; ::_thesis: ( ( for a being Element of G holds f1 . a = Bottom a ) & ( for a being Element of G holds f2 . a = Bottom a ) implies f1 = f2 )
assume 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 ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_Element_of_G_holds_f1_._a_=_f2_._a
let a be Element of G; ::_thesis: f1 . a = f2 . a
thus f1 . a = Bottom a by A2
.= f2 . a by A3 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for a being Element of Q holds Bottom (Bottom a) = a
let a be Element of Q; ::_thesis: Bottom (Bottom a) = a
the absurd of Q is cyclic by Def19;
then A1: a -l> the absurd of Q = a -r> the absurd of Q by Def18;
the absurd of Q is dualizing by Def20;
hence Bottom (Bottom a) = a by A1, Def17; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for X being set holds Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
let X be set ; ::_thesis: Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
{ (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } is_less_than Bottom Q
proof
let c be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not c in { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } or c [= Bottom Q )
assume c in { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } ; ::_thesis: c [= Bottom Q
then consider b being Element of Q such that
A1: ( c = ("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b & b in X ) ;
Bottom b in { (Bottom a) where a is Element of Q : a in X } by A1;
then "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) [= Bottom b by LATTICE3:38;
hence c [= Bottom Q by A1, Th12; ::_thesis: verum
end;
then "\/" ( { (("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] b) where b is Element of Q : b in X } ,Q) [= Bottom Q by LATTICE3:def_21;
then ("/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q)) [*] ("\/" (X,Q)) [= Bottom Q by Def5;
then A2: "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) [= Bottom ("\/" (X,Q)) by Th12;
Bottom ("\/" (X,Q)) is_less_than { (Bottom a) where a is Element of Q : a in X }
proof
let b be Element of Q; :: according to LATTICE3:def_16 ::_thesis: ( not b in { (Bottom a) where a is Element of Q : a in X } or Bottom ("\/" (X,Q)) [= b )
assume b in { (Bottom a) where a is Element of Q : a in X } ; ::_thesis: Bottom ("\/" (X,Q)) [= b
then consider a being Element of Q such that
A3: b = Bottom a and
A4: a in X ;
a [= "\/" (X,Q) by A4, LATTICE3:38;
hence Bottom ("\/" (X,Q)) [= b by A3, Th13; ::_thesis: verum
end;
then Bottom ("\/" (X,Q)) [= "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by LATTICE3:39;
hence Bottom ("\/" (X,Q)) = "/\" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by A2, LATTICES:8; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for X being set holds Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
let X be set ; ::_thesis: Bottom ("/\" (X,Q)) = "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q)
X is_greater_than "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q)
proof
let c be Element of Q; :: according to LATTICE3:def_16 ::_thesis: ( not c in X or "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c )
assume c in X ; ::_thesis: "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c
then Bottom c in { (Bottom b) where b is Element of Q : b in X } ;
then A1: Bottom (Bottom c) in { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ;
Bottom (Bottom c) = c by Th22;
hence "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= c by A1, LATTICE3:38; ::_thesis: verum
end;
then A2: "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) [= "/\" (X,Q) by LATTICE3:39;
{ (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } or x in X )
assume x in { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ; ::_thesis: x in X
then consider a being Element of Q such that
A3: ( x = Bottom a & a in { (Bottom b) where b is Element of Q : b in X } ) ;
ex b being Element of Q st
( a = Bottom b & b in X ) by A3;
hence x in X by A3, Th22; ::_thesis: verum
end;
then "/\" (X,Q) [= "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) by LATTICE3:45;
then "/\" (X,Q) = "/\" ( { (Bottom a) where a is Element of Q : a in { (Bottom b) where b is Element of Q : b in X } } ,Q) by A2, LATTICES:8;
hence Bottom ("/\" (X,Q)) = Bottom (Bottom ("\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q))) by Th24
.= "\/" ( { (Bottom a) where a is Element of Q : a in X } ,Q) by Th22 ;
::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for a, b being Element of Q holds
( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )
let a, b be Element of Q; ::_thesis: ( Bottom (a "\/" b) = (Bottom a) "/\" (Bottom b) & Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) )
A1: { (Bottom c) where c is Element of Q : c in {a,b} } = {(Bottom a),(Bottom b)}
proof
thus { (Bottom c) where c is Element of Q : c in {a,b} } c= {(Bottom a),(Bottom b)} :: according to XBOOLE_0:def_10 ::_thesis: {(Bottom a),(Bottom b)} c= { (Bottom c) where c is Element of Q : c in {a,b} }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Bottom c) where c is Element of Q : c in {a,b} } or x in {(Bottom a),(Bottom b)} )
assume x in { (Bottom c) where c is Element of Q : c in {a,b} } ; ::_thesis: x in {(Bottom a),(Bottom b)}
then consider c being Element of Q such that
A2: x = Bottom c and
A3: c in {a,b} ;
( c = a or c = b ) by A3, TARSKI:def_2;
hence x in {(Bottom a),(Bottom b)} by A2, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Bottom a),(Bottom b)} or x in { (Bottom c) where c is Element of Q : c in {a,b} } )
assume x in {(Bottom a),(Bottom b)} ; ::_thesis: x in { (Bottom c) where c is Element of Q : c in {a,b} }
then ( ( x = Bottom a & a in {a,b} ) or ( x = Bottom b & b in {a,b} ) ) by TARSKI:def_2;
hence x in { (Bottom c) where c is Element of Q : c in {a,b} } ; ::_thesis: verum
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; ::_thesis: Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b)
( (Bottom a) "\/" (Bottom b) = "\/" {(Bottom a),(Bottom b)} & a "/\" b = "/\" {a,b} ) by LATTICE3:43;
hence Bottom (a "/\" b) = (Bottom a) "\/" (Bottom b) by A1, Th25; ::_thesis: verum
end;
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) )
proof
let Q be Girard-Quantale; ::_thesis: 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) )
let a be Element of Q; ::_thesis: 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) )
let X be set ; ::_thesis: ( 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) )
deffunc H5( Element of Q) -> Element of the carrier of Q = (Bottom a) [*] $1;
deffunc H6( Element of Q) -> Element of Q = Bottom $1;
deffunc H7( Element of Q) -> Element of the carrier of Q = (Bottom a) [*] (Bottom $1);
defpred S1[ set ] means $1 in X;
deffunc H8( Element of Q) -> Element of Q = Bottom ((Bottom a) [*] (Bottom $1));
deffunc H9( Element of Q) -> Element of Q = a delta $1;
thus a [*] ("\/" (X,Q)) = "\/" ( { (a [*] b) where b is Element of Q : b in X } ,Q) by Def5; ::_thesis: a delta ("/\" (X,Q)) = "/\" ( { (a delta c) where c is Element of Q : c in X } ,Q)
A1: { H5(c) where c is Element of Q : c in { H6(d) where d is Element of Q : S1[d] } } = { H5(H6(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1();
A2: { H6(c) where c is Element of Q : c in { H7(d) where d is Element of Q : S1[d] } } = { H6(H7(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1();
A3: for b being Element of Q holds H8(b) = H9(b) ;
A4: { H8(b) where b is Element of Q : S1[b] } = { H9(c) where c is Element of Q : S1[c] } from FRAENKEL:sch_5(A3);
thus a delta ("/\" (X,Q)) = Bottom ((Bottom a) [*] ("\/" ( { (Bottom b) where b is Element of Q : b in X } ,Q))) by Th25
.= Bottom ("\/" ( { ((Bottom a) [*] (Bottom b)) where b is Element of Q : b in X } ,Q)) by A1, Def5
.= "/\" ( { (a delta b) where b is Element of Q : b in X } ,Q) by A2, A4, Th24 ; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: 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) )
let a be Element of Q; ::_thesis: 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) )
let X be set ; ::_thesis: ( ("\/" (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) )
deffunc H5( Element of Q) -> Element of the carrier of Q = $1 [*] (Bottom a);
deffunc H6( Element of Q) -> Element of Q = Bottom $1;
deffunc H7( Element of Q) -> Element of the carrier of Q = (Bottom $1) [*] (Bottom a);
defpred S1[ set ] means $1 in X;
deffunc H8( Element of Q) -> Element of Q = Bottom ((Bottom $1) [*] (Bottom a));
deffunc H9( Element of Q) -> Element of Q = $1 delta a;
thus ("\/" (X,Q)) [*] a = "\/" ( { (b [*] a) where b is Element of Q : b in X } ,Q) by Def6; ::_thesis: ("/\" (X,Q)) delta a = "/\" ( { (c delta a) where c is Element of Q : c in X } ,Q)
A1: { H5(c) where c is Element of Q : c in { H6(d) where d is Element of Q : S1[d] } } = { H5(H6(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1();
A2: { H6(c) where c is Element of Q : c in { H7(d) where d is Element of Q : S1[d] } } = { H6(H7(b)) where b is Element of Q : S1[b] } from QUANTAL1:sch_1();
A3: for b being Element of Q holds H8(b) = H9(b) ;
A4: { H8(b) where b is Element of Q : S1[b] } = { H9(c) where c is Element of Q : S1[c] } from FRAENKEL:sch_5(A3);
thus ("/\" (X,Q)) delta a = Bottom (("\/" ( { (Bottom b) where b is Element of Q : b in X } ,Q)) [*] (Bottom a)) by Th25
.= Bottom ("\/" ( { ((Bottom b) [*] (Bottom a)) where b is Element of Q : b in X } ,Q)) by A1, Def6
.= "/\" ( { (b delta a) where b is Element of Q : b in X } ,Q) by A2, A4, Th24 ; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: 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) )
let a, b, c be Element of Q; ::_thesis: ( a delta (b "/\" c) = (a delta b) "/\" (a delta c) & (b "/\" c) delta a = (b delta a) "/\" (c delta a) )
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 ; ::_thesis: (b "/\" c) delta a = (b delta a) "/\" (c delta a)
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 ; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for a1, b1, a2, b2 being Element of Q st a1 [= b1 & a2 [= b2 holds
a1 delta a2 [= b1 delta b2
let a1, b1, a2, b2 be Element of Q; ::_thesis: ( a1 [= b1 & a2 [= b2 implies a1 delta a2 [= b1 delta b2 )
assume ( a1 [= b1 & a2 [= b2 ) ; ::_thesis: a1 delta a2 [= b1 delta b2
then ( Bottom b1 [= Bottom a1 & Bottom b2 [= Bottom a2 ) by Th13;
then (Bottom b1) [*] (Bottom b2) [= (Bottom a1) [*] (Bottom a2) by Th9;
hence a1 delta a2 [= b1 delta b2 by Th13; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for a, b, c being Element of Q holds (a delta b) delta c = a delta (b delta c)
let a, b, c be Element of Q; ::_thesis: (a delta b) delta c = a delta (b delta c)
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 ; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for a being Element of Q holds
( a [*] (Top Q) = a & (Top Q) [*] a = a )
let a be Element of Q; ::_thesis: ( a [*] (Top Q) = a & (Top Q) [*] a = a )
the absurd of Q is dualizing by Def20;
then A1: Top Q = the_unity_wrt H4(Q) by Th19;
H4(Q) is having_a_unity by MONOID_0:def_10;
hence ( a [*] (Top Q) = a & (Top Q) [*] a = a ) by A1, SETWISEO:15; ::_thesis: verum
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
let Q be Girard-Quantale; ::_thesis: for a being Element of Q holds
( a delta (Bottom Q) = a & (Bottom Q) delta a = a )
let a be Element of Q; ::_thesis: ( a delta (Bottom Q) = a & (Bottom Q) delta a = a )
( (Bottom a) [*] (Top Q) = Bottom a & (Top Q) [*] (Bottom a) = Bottom a ) by Th32;
hence ( a delta (Bottom Q) = a & (Bottom Q) delta a = a ) by Th22; ::_thesis: verum
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
let Q be Quantale; ::_thesis: 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)) ) )
let j be UnOp of Q; ::_thesis: ( j is monotone & j is idempotent & j is \/-distributive implies ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) ) )
assume A1: ( j is monotone & j is idempotent & j is \/-distributive ) ; ::_thesis: ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )
reconsider D = rng j as non empty Subset of Q ;
dom j = H1(Q) by FUNCT_2:def_1;
then reconsider j9 = j as Function of H1(Q),D by RELSET_1:4;
deffunc H5( Subset of D) -> Element 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 = H5(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; ::_thesis: f . (f .: X) = f . (union X)
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__::_thesis:_for_a_being_Element_of_Q_st_a_in__{__(j_._b)_where_b_is_Element_of_Q_:_b_in_union_X__}__holds_
ex_b_being_Element_of_the_carrier_of_Q_st_
(_a_[=_b_&_b_in__{__(j_._a)_where_a_is_Element_of_Q_:_a_in_f_.:_X__}__)
let a be Element of Q; ::_thesis: ( a in { (j . b) where b is Element of Q : b in union X } implies ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) )
assume a in { (j . b) where b is Element of Q : b in union X } ; ::_thesis: ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )
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 = Y as Subset of D by A8;
A9: b9 [= "\/" (Y,Q) by A7, LATTICE3:38;
take b = j . ("\/" (Y,Q)); ::_thesis: ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )
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 { (j . a) where a is Element of Q : a in f .: X } ) by A1, A5, A10, A9, Def12; ::_thesis: verum
end;
then A11: "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) [= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) by LATTICE3:47;
{ (j . a) where a is Element of Q : a in f .: X } is_less_than "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)
proof
let a be Element of Q; :: according to LATTICE3:def_17 ::_thesis: ( not a in { (j . a) where a is Element of Q : a in f .: X } or a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) )
assume a in { (j . a) where a is Element of Q : a in f .: X } ; ::_thesis: a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)
then consider a9 being Element of Q such that
A12: a = j . a9 and
A13: a9 in f .: X ;
consider x being set 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 = 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= { (j . b) where b is Element of Q : b in union X }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (j . b) where b is Element of Q : b in Y } or z in { (j . b) where b is Element of Q : b in union X } )
assume z in { (j . b) where b is Element of Q : b in Y } ; ::_thesis: z in { (j . b) where b is Element of Q : b in union X }
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 z in { (j . b) where b is Element of Q : b in union X } by A18; ::_thesis: verum
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 [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A17, LATTICE3:45;
then a [= j . ("\/" ( { (j . b) where b is Element of Q : b in union X } ,Q)) by A1, A12, Def12;
then a [= j . (j . ("\/" X9)) by A1, Th10;
then a [= j . ("\/" X9) by A1, Lm1;
hence a [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A1, Th10; ::_thesis: verum
end;
then A20: "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by LATTICE3:def_21;
thus f . (f .: X) = j . ("\/" Y) by A2
.= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) by A1, Th10
.= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A20, A11, LATTICES:8
.= j . ("\/" X9) by A1, Th10
.= f . (union X) by A2 ; ::_thesis: verum
end;
for a being Element of D holds f . {a} = a
proof
let a be Element of D; ::_thesis: f . {a} = a
consider a9 being set 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 = 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 ; ::_thesis: verum
end;
then consider L being strict complete Lattice such that
A23: H1(L) = D and
A24: for X being Subset of L holds "\/" X = f . X by A4, LATTICE3:55;
take L ; ::_thesis: ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )
thus H1(L) = rng j by A23; ::_thesis: for X being Subset of L holds "\/" X = j . ("\/" (X,Q))
let X be Subset of L; ::_thesis: "\/" X = j . ("\/" (X,Q))
thus "\/" X = f . X by A24
.= j . ("\/" (X,Q)) by A2, A23 ; ::_thesis: verum
end;