Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Semigroup Operations on Finite Subsets

**by****Czeslaw Bylinski**- Received May 4, 1990
- MML identifier: SETWOP_2

- [ Mizar article, MML identifier index ]

environ vocabulary FINSUB_1, BINOP_1, FUNCT_1, FINSEQ_1, FINSEQ_2, SETWISEO, BOOLE, RELAT_1, TARSKI, FINSEQOP, FUNCOP_1, SUBSET_1, FUNCT_4, FINSOP_1; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, RELSET_1, FUNCT_1, FINSEQ_1, FINSUB_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, SETWISEO, FINSEQ_2, FINSEQOP, FINSOP_1; constructors NAT_1, BINOP_1, WELLORD2, SETWISEO, FINSEQOP, FINSOP_1, XREAL_0, MEMBERED, PARTFUN1, XBOOLE_0; clusters SUBSET_1, FUNCT_1, RELSET_1, FINSEQ_2, FINSUB_1, FINSEQ_1, ARYTM_3, MEMBERED, ZFMISC_1, FUNCT_2, XBOOLE_0, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve x,y for set; reserve C,C',D,E for non empty set; reserve c,c',c1,c2,c3 for Element of C; reserve B,B',B1,B2 for Element of Fin C; reserve A for Element of Fin C'; reserve d,d1,d2,d3,d4,e for Element of D; reserve F,G for BinOp of D; reserve u for UnOp of D; reserve f,f' for Function of C,D; reserve g for Function of C',D; reserve H for BinOp of E; reserve h for Function of D,E; reserve i,j for Nat; reserve s for Function; reserve p,q for FinSequence of D; reserve T1,T2 for Element of i-tuples_on D; canceled 2; theorem :: SETWOP_2:3 F is commutative associative & c1 <> c2 implies F $$ ({c1,c2},f) = F.(f.c1, f.c2); theorem :: SETWOP_2:4 F is commutative associative & (B <> {} or F has_a_unity) & not c in B implies F $$(B \/ {c}, f) = F.(F $$(B,f),f.c); theorem :: SETWOP_2:5 F is commutative associative & c1 <> c2 & c1 <> c3 & c2 <> c3 implies F $$ ({c1,c2,c3},f) = F.(F.(f.c1, f.c2),f.c3); theorem :: SETWOP_2:6 F is commutative associative & (B1 <> {} & B2 <> {} or F has_a_unity) & B1 misses B2 implies F $$(B1 \/ B2, f) = F.(F $$(B1,f),F $$(B2,f)); theorem :: SETWOP_2:7 F is commutative associative & (A <> {} or F has_a_unity) & (ex s st dom s = A & rng s = B & s is one-to-one & g|A = f*s) implies F $$(A,g) = F $$(B,f); theorem :: SETWOP_2:8 H is commutative associative & (B <> {} or H has_a_unity) & f is one-to-one implies H $$(f.:B,h) = H $$(B,h*f); theorem :: SETWOP_2:9 F is commutative associative & (B <> {} or F has_a_unity) & f|B = f'|B implies F $$(B,f) = F $$(B,f'); theorem :: SETWOP_2:10 F is commutative associative & F has_a_unity & e = the_unity_wrt F & f.:B = {e} implies F$$(B,f) = e; theorem :: SETWOP_2:11 F is commutative associative & F has_a_unity & e = the_unity_wrt F & G.(e,e) = e & (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))) implies G.(F$$(B,f),F$$(B,f')) = F $$(B,G.:(f,f')); theorem :: SETWOP_2:12 F is commutative associative & F has_a_unity implies F.(F$$(B,f),F$$(B,f')) = F $$(B,F.:(f,f')); theorem :: SETWOP_2:13 F is commutative associative & F has_a_unity & F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies G.(F$$(B,f),F$$(B,f')) = F $$(B,G.:(f,f')); theorem :: SETWOP_2:14 F is commutative associative & F has_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(d,e) = e implies G.(d,F$$(B,f)) = F $$(B,G[;](d,f)); theorem :: SETWOP_2:15 F is commutative associative & F has_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(e,d) = e implies G.(F$$(B,f),d) = F $$(B,G[:](f,d)); theorem :: SETWOP_2:16 F is commutative associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G.(d,F$$(B,f)) = F $$(B,G[;](d,f)); theorem :: SETWOP_2:17 F is commutative associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G.(F$$(B,f),d) = F $$(B,G[:](f,d)); theorem :: SETWOP_2:18 F is commutative associative & F has_a_unity & H is commutative associative & H has_a_unity & h.the_unity_wrt F = the_unity_wrt H & (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h.(F$$(B,f)) = H $$(B,h*f); theorem :: SETWOP_2:19 F is commutative associative & F has_a_unity & u.the_unity_wrt F = the_unity_wrt F & u is_distributive_wrt F implies u.(F$$(B,f)) = F $$(B,u*f); theorem :: SETWOP_2:20 F is commutative associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G[;](d,id D).(F$$(B,f)) = F $$(B,G[;](d,id D)*f); theorem :: SETWOP_2:21 F is commutative associative & F has_a_unity & F has_an_inverseOp implies (the_inverseOp_wrt F).(F$$(B,f)) = F $$(B,(the_inverseOp_wrt F)*f); definition let D,p,d; func [#](p,d) -> Function of NAT,D equals :: SETWOP_2:def 1 (NAT --> d) +* p; end; theorem :: SETWOP_2:22 (i in dom p implies [#](p,d).i = p.i) & (not i in dom p implies [#](p,d).i = d); theorem :: SETWOP_2:23 [#](p,d)|(dom p) = p; theorem :: SETWOP_2:24 [#](p^q,d)|(dom p) = p; theorem :: SETWOP_2:25 rng [#](p,d) = rng p \/ {d}; theorem :: SETWOP_2:26 h*[#](p,d) = [#](h*p,h.d); definition let i; redefine func Seg i -> Element of Fin NAT; end; definition let f be FinSequence; redefine func dom f -> Element of Fin NAT; end; definition let D,p,F; assume (F has_a_unity or len p >= 1) & F is associative commutative; redefine func F "**" p equals :: SETWOP_2:def 2 F $$(dom p,[#](p,the_unity_wrt F)); synonym F $$ p; end; canceled 8; theorem :: SETWOP_2:35 F has_a_unity implies F"**"(i|->the_unity_wrt F) = the_unity_wrt F; canceled; theorem :: SETWOP_2:37 F is associative & (i>=1 & j>=1 or F has_a_unity) implies F"**"((i+j)|->d) = F.(F"**"(i|->d),F"**"(j|->d)); theorem :: SETWOP_2:38 F is commutative associative & (i>=1 & j>=1 or F has_a_unity) implies F"**"((i*j)|->d) = F"**"(j|->(F"**"(i|->d))); theorem :: SETWOP_2:39 F has_a_unity & H has_a_unity & h.the_unity_wrt F = the_unity_wrt H & (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h.(F"**"p) = H "**"(h*p); theorem :: SETWOP_2:40 F has_a_unity & u.the_unity_wrt F = the_unity_wrt F & u is_distributive_wrt F implies u.(F"**"p) = F "**"(u*p); theorem :: SETWOP_2:41 F is associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G[;](d,id D).(F"**"p) = F "**"(G[;](d,id D)*p); theorem :: SETWOP_2:42 F is commutative associative & F has_a_unity & F has_an_inverseOp implies (the_inverseOp_wrt F).(F"**"p) = F "**"((the_inverseOp_wrt F)*p); theorem :: SETWOP_2:43 F is commutative associative & F has_a_unity & e = the_unity_wrt F & G.(e,e) = e & (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))) & len p = len q implies G.(F"**"p,F"**"q) = F "**"(G.:(p,q)); theorem :: SETWOP_2:44 F is commutative associative & F has_a_unity & e = the_unity_wrt F & G.(e,e) = e & (for d1,d2,d3,d4 holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))) implies G.(F"**"T1,F"**"T2) = F "**"(G.:(T1,T2)); theorem :: SETWOP_2:45 F is commutative associative & F has_a_unity & len p = len q implies F.(F"**"p,F"**"q) = F "**"(F.:(p,q)); theorem :: SETWOP_2:46 F is commutative associative & F has_a_unity implies F.(F"**"T1,F"**"T2) = F "**"(F.:(T1,T2)); theorem :: SETWOP_2:47 F is commutative associative & F has_a_unity implies F"**"(i|->(F.(d1,d2))) = F.(F"**"(i|->d1),F"**"(i|->d2)); theorem :: SETWOP_2:48 F is commutative associative & F has_a_unity & F has_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies G.(F"**"T1,F"**"T2) = F "**"(G.:(T1,T2)); theorem :: SETWOP_2:49 F is commutative associative & F has_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(d,e) = e implies G.(d,F"**"p) = F "**"(G[;](d,p)); theorem :: SETWOP_2:50 F is commutative associative & F has_a_unity & e = the_unity_wrt F & G is_distributive_wrt F & G.(e,d) = e implies G.(F"**"p,d) = F "**"(G[:](p,d)); theorem :: SETWOP_2:51 F is commutative associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G.(d,F"**"p) = F "**"(G[;](d,p)); theorem :: SETWOP_2:52 F is commutative associative & F has_a_unity & F has_an_inverseOp & G is_distributive_wrt F implies G.(F"**"p,d) = F "**"(G[:](p,d));

Back to top