Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Binary Operations

**by****Czeslaw Bylinski**- Received April 14, 1989
- MML identifier: BINOP_1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, BOOLE, RELAT_1, BINOP_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2; constructors TARSKI, FUNCT_2, XBOOLE_0; clusters RELSET_1, SUBSET_1, XBOOLE_0, ZFMISC_1; requirements SUBSET, BOOLE; begin definition let f be Function; let a,b be set; func f.(a,b) -> set equals :: BINOP_1:def 1 f.[a,b]; end; reserve A for set; definition let A,B be non empty set, C be set, f be Function of [:A,B:],C; let a be Element of A; let b be Element of B; redefine func f.(a,b) -> Element of C; end; canceled; theorem :: BINOP_1:2 for A,B,C be non empty set for f1,f2 being Function of [:A,B:],C st for a being Element of A for b being Element of B holds f1.(a,b) = f2.(a,b) holds f1 = f2; definition let A be set; mode UnOp of A is Function of A,A; mode BinOp of A is Function of [:A,A:],A; end; reserve u for UnOp of A, o,o' for BinOp of A, a,b,c,e,e1,e2 for Element of A; scheme BinOpEx{A()->non empty set, P[Element of A(),Element of A(),Element of A()]}: ex o being BinOp of A() st for a,b being Element of A() holds P[a,b,o.(a,b)] provided for x,y being Element of A() ex z being Element of A() st P[x,y,z]; scheme BinOpLambda{A()->non empty set, O(Element of A(),Element of A())->Element of A()}: ex o being BinOp of A() st for a,b being Element of A() holds o.(a,b) = O(a,b); definition let A,o; attr o is commutative means :: BINOP_1:def 2 for a,b holds o.(a,b) = o.(b,a); attr o is associative means :: BINOP_1:def 3 for a,b,c holds o.(a,o.(b,c)) = o.(o.(a,b),c); attr o is idempotent means :: BINOP_1:def 4 for a holds o.(a,a) = a; end; definition cluster -> empty associative commutative BinOp of {}; end; definition let A,e,o; pred e is_a_left_unity_wrt o means :: BINOP_1:def 5 for a holds o.(e,a) = a; pred e is_a_right_unity_wrt o means :: BINOP_1:def 6 for a holds o.(a,e) = a; end; definition let A,e,o; pred e is_a_unity_wrt o means :: BINOP_1:def 7 e is_a_left_unity_wrt o & e is_a_right_unity_wrt o; end; canceled 8; theorem :: BINOP_1:11 e is_a_unity_wrt o iff for a holds o.(e,a) = a & o.(a,e) = a; theorem :: BINOP_1:12 o is commutative implies (e is_a_unity_wrt o iff for a holds o.(e,a) = a); theorem :: BINOP_1:13 o is commutative implies (e is_a_unity_wrt o iff for a holds o.(a,e) = a); theorem :: BINOP_1:14 o is commutative implies (e is_a_unity_wrt o iff e is_a_left_unity_wrt o); theorem :: BINOP_1:15 o is commutative implies (e is_a_unity_wrt o iff e is_a_right_unity_wrt o); theorem :: BINOP_1:16 o is commutative implies (e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o); theorem :: BINOP_1:17 e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o implies e1 = e2; theorem :: BINOP_1:18 e1 is_a_unity_wrt o & e2 is_a_unity_wrt o implies e1 = e2; definition let A,o; assume ex e st e is_a_unity_wrt o; func the_unity_wrt o -> Element of A means :: BINOP_1:def 8 it is_a_unity_wrt o; end; definition let A,o',o; pred o' is_left_distributive_wrt o means :: BINOP_1:def 9 for a,b,c holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)); pred o' is_right_distributive_wrt o means :: BINOP_1:def 10 for a,b,c holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)); end; definition let A,o',o; pred o' is_distributive_wrt o means :: BINOP_1:def 11 o' is_left_distributive_wrt o & o' is_right_distributive_wrt o; end; canceled 4; theorem :: BINOP_1:23 o' is_distributive_wrt o iff for a,b,c 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 :: BINOP_1:24 for A being non empty set, o,o' being BinOp of A holds o' is commutative implies (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))) ; theorem :: BINOP_1:25 for A being non empty set, o,o' being BinOp of A holds o' is commutative implies (o' is_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))) ; theorem :: BINOP_1:26 for A being non empty set, o,o' being BinOp of A holds o' is commutative implies (o' is_distributive_wrt o iff o' is_left_distributive_wrt o); theorem :: BINOP_1:27 for A being non empty set, o,o' being BinOp of A holds o' is commutative implies (o' is_distributive_wrt o iff o' is_right_distributive_wrt o); theorem :: BINOP_1:28 for A being non empty set, o,o' being BinOp of A holds o' is commutative implies (o' is_right_distributive_wrt o iff o' is_left_distributive_wrt o); definition let A,u,o; pred u is_distributive_wrt o means :: BINOP_1:def 12 for a,b holds u.(o.(a,b)) = o.((u.a),(u.b)); end; definition let A be non empty set, o be BinOp of A; redefine attr o is commutative means :: BINOP_1:def 13 for a,b being Element of A holds o.(a,b) = o.(b,a); attr o is associative means :: BINOP_1:def 14 for a,b,c being Element of A holds o.(a,o.(b,c)) = o.(o.(a,b),c); attr o is idempotent means :: BINOP_1:def 15 for a being Element of A holds o.(a,a) = a; end; definition let A be non empty set, e be Element of A, o be BinOp of A; redefine pred e is_a_left_unity_wrt o means :: BINOP_1:def 16 for a being Element of A holds o.(e,a) = a; pred e is_a_right_unity_wrt o means :: BINOP_1:def 17 for a being Element of A holds o.(a,e) = a; end; definition let A be non empty set, o',o be BinOp of A; redefine pred o' is_left_distributive_wrt o means :: BINOP_1:def 18 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 :: BINOP_1:def 19 for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)) ; end; definition let A be non empty set, u be UnOp of A, o be BinOp of A; redefine pred u is_distributive_wrt o means :: BINOP_1:def 20 for a,b being Element of A holds u.(o.(a,b)) = o.((u.a),(u.b)); end;

Back to top