begin
:: deftheorem defines . BINOP_1:def 1 :
theorem Th1:
for
X,
Y,
Z being
set for
f1,
f2 being
Function of
[:X,Y:],
Z st ( for
x,
y being
set st
x in X &
y in Y holds
f1 . x,
y = f2 . x,
y ) holds
f1 = f2
theorem
scheme
FuncEx2{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
P1[
set ,
set ,
set ] } :
ex
f being
Function of
[:F1(),F2():],
F3() st
for
x,
y being
set st
x in F1() &
y in F2() holds
P1[
x,
y,
f . x,
y]
provided
A1:
for
x,
y being
set st
x in F1() &
y in F2() holds
ex
z being
set st
(
z in F3() &
P1[
x,
y,
z] )
scheme
Lambda2{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4(
set ,
set )
-> set } :
ex
f being
Function of
[:F1(),F2():],
F3() st
for
x,
y being
set st
x in F1() &
y in F2() holds
f . x,
y = F4(
x,
y)
provided
A1:
for
x,
y being
set st
x in F1() &
y in F2() holds
F4(
x,
y)
in F3()
definition
let A be
set ;
let o be
BinOp of
A;
attr o is
commutative means :
Def2:
for
a,
b being
Element of
A holds
o . a,
b = o . b,
a;
attr o is
associative means :
Def3:
for
a,
b,
c being
Element of
A holds
o . a,
(o . b,c) = o . (o . a,b),
c;
attr o is
idempotent means :
Def4:
for
a being
Element of
A holds
o . a,
a = a;
end;
:: deftheorem Def2 defines commutative BINOP_1:def 2 :
:: deftheorem Def3 defines associative BINOP_1:def 3 :
:: deftheorem Def4 defines idempotent BINOP_1:def 4 :
:: deftheorem Def5 defines is_a_left_unity_wrt BINOP_1:def 5 :
:: deftheorem Def6 defines is_a_right_unity_wrt BINOP_1:def 6 :
:: deftheorem defines is_a_unity_wrt BINOP_1:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
:: deftheorem defines the_unity_wrt BINOP_1:def 8 :
definition
let A be
set ;
let o',
o be
BinOp of
A;
pred o' is_left_distributive_wrt o means :
Def9:
for
a,
b,
c being
Element of
A holds
o' . a,
(o . b,c) = o . (o' . a,b),
(o' . a,c);
pred o' is_right_distributive_wrt o means :
Def10:
for
a,
b,
c being
Element of
A holds
o' . (o . a,b),
c = o . (o' . a,c),
(o' . b,c);
end;
:: deftheorem Def9 defines is_left_distributive_wrt BINOP_1:def 9 :
:: deftheorem Def10 defines is_right_distributive_wrt BINOP_1:def 10 :
:: deftheorem defines is_distributive_wrt BINOP_1:def 11 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th23:
for
A being
set for
o',
o being
BinOp of
A holds
(
o' is_distributive_wrt o iff for
a,
b,
c being
Element of
A holds
(
o' . a,
(o . b,c) = o . (o' . a,b),
(o' . a,c) &
o' . (o . a,b),
c = o . (o' . a,c),
(o' . b,c) ) )
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
:: deftheorem Def12 defines is_distributive_wrt BINOP_1:def 12 :
definition
let A be non
empty set ;
let o be
BinOp of
A;
redefine attr o is
commutative means
for
a,
b being
Element of
A holds
o . a,
b = o . b,
a;
correctness
compatibility
( o is commutative iff for a, b being Element of A holds o . a,b = o . b,a );
by Def2;
redefine attr o is
associative means
for
a,
b,
c being
Element of
A holds
o . a,
(o . b,c) = o . (o . a,b),
c;
correctness
compatibility
( o is associative iff for a, b, c being Element of A holds o . a,(o . b,c) = o . (o . a,b),c );
by Def3;
redefine attr o is
idempotent means
for
a being
Element of
A holds
o . a,
a = a;
correctness
compatibility
( o is idempotent iff for a being Element of A holds o . a,a = a );
by Def4;
end;
:: deftheorem defines commutative BINOP_1:def 13 :
:: deftheorem defines associative BINOP_1:def 14 :
:: deftheorem defines idempotent BINOP_1:def 15 :
:: deftheorem defines is_a_left_unity_wrt BINOP_1:def 16 :
:: deftheorem defines is_a_right_unity_wrt BINOP_1:def 17 :
definition
let A be non
empty set ;
let o',
o be
BinOp of
A;
redefine pred o' is_left_distributive_wrt o means
for
a,
b,
c being
Element of
A holds
o' . a,
(o . b,c) = o . (o' . a,b),
(o' . a,c);
correctness
compatibility
( o' is_left_distributive_wrt o iff for a, b, c being Element of A holds o' . a,(o . b,c) = o . (o' . a,b),(o' . a,c) );
by Def9;
redefine pred o' is_right_distributive_wrt o means
for
a,
b,
c being
Element of
A holds
o' . (o . a,b),
c = o . (o' . a,c),
(o' . b,c);
correctness
compatibility
( o' is_right_distributive_wrt o iff for a, b, c being Element of A holds o' . (o . a,b),c = o . (o' . a,c),(o' . b,c) );
by Def10;
end;
:: deftheorem defines is_left_distributive_wrt BINOP_1:def 18 :
:: deftheorem defines is_right_distributive_wrt BINOP_1:def 19 :
:: deftheorem defines is_distributive_wrt BINOP_1:def 20 :
theorem
theorem
theorem
theorem
scheme
PartFuncEx2{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
P1[
set ,
set ,
set ] } :
ex
f being
PartFunc of , st
( ( for
x,
y being
set holds
(
[x,y] in dom f iff (
x in F1() &
y in F2() & ex
z being
set st
P1[
x,
y,
z] ) ) ) & ( for
x,
y being
set st
[x,y] in dom f holds
P1[
x,
y,
f . x,
y] ) )
provided
A1:
for
x,
y,
z being
set st
x in F1() &
y in F2() &
P1[
x,
y,
z] holds
z in F3()
and A2:
for
x,
y,
z1,
z2 being
set st
x in F1() &
y in F2() &
P1[
x,
y,
z1] &
P1[
x,
y,
z2] holds
z1 = z2
scheme
LambdaR2{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4(
set ,
set )
-> set ,
P1[
set ,
set ] } :
ex
f being
PartFunc of , st
( ( for
x,
y being
set holds
(
[x,y] in dom f iff (
x in F1() &
y in F2() &
P1[
x,
y] ) ) ) & ( for
x,
y being
set st
[x,y] in dom f holds
f . x,
y = F4(
x,
y) ) )
provided
A1:
for
x,
y being
set st
P1[
x,
y] holds
F4(
x,
y)
in F3()
scheme
PartLambda2{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4(
set ,
set )
-> set ,
P1[
set ,
set ] } :
ex
f being
PartFunc of , st
( ( for
x,
y being
set holds
(
[x,y] in dom f iff (
x in F1() &
y in F2() &
P1[
x,
y] ) ) ) & ( for
x,
y being
set st
[x,y] in dom f holds
f . x,
y = F4(
x,
y) ) )
provided
A1:
for
x,
y being
set st
x in F1() &
y in F2() &
P1[
x,
y] holds
F4(
x,
y)
in F3()