Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Semilattice Operations on Finite Subsets

**by****Andrzej Trybulec**- Received September 18, 1989
- MML identifier: SETWISEO

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, FUNCT_1, RELAT_1, FINSUB_1, FINSET_1, BINOP_1, FUNCOP_1, TARSKI, SETWISEO; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FINSUB_1, FINSET_1, FUNCT_2, BINOP_1, FUNCOP_1; constructors TARSKI, ENUMSET1, FINSUB_1, FINSET_1, BINOP_1, FUNCOP_1, XBOOLE_0; clusters FINSET_1, FINSUB_1, RELSET_1, XBOOLE_0, ZFMISC_1; requirements BOOLE, SUBSET; begin :: A u x i l i a r y T h e o r e m s reserve x,y,z,X,Y for set; canceled 2; theorem :: SETWISEO:3 {x} c= {x,y,z} ; theorem :: SETWISEO:4 {x,y} c= {x,y,z} ; theorem :: SETWISEO:5 X c= Y \/ {x} implies x in X or X c= Y; theorem :: SETWISEO:6 x in X \/ {y} iff x in X or x = y; canceled; theorem :: SETWISEO:8 X \/ {x} c= Y iff x in Y & X c= Y; canceled 2; theorem :: SETWISEO:11 for X,Y for f being Function holds f.:(Y \ f"X) = f.:Y \ X; reserve X,Y for non empty set, f for Function of X,Y; theorem :: SETWISEO:12 for x being Element of X holds x in f"{f.x}; theorem :: SETWISEO:13 for x being Element of X holds f.:{x} = {f.x}; scheme SubsetEx { A() -> non empty set, P[set] } : ex B being Subset of A() st for x being Element of A() holds x in B iff P[x]; :: Theorems related to Fin ... theorem :: SETWISEO:14 for B being Element of Fin X for x st x in B holds x is Element of X; theorem :: SETWISEO:15 for A being (Element of Fin X), B being set for f being Function of X,Y st for x being Element of X holds x in A implies f.x in B holds f.:A c= B; theorem :: SETWISEO:16 for X being set for B being Element of Fin X for A being set st A c= B holds A is Element of Fin X; canceled; theorem :: SETWISEO:18 for B being Element of Fin X st B <> {} ex x being Element of X st x in B; theorem :: SETWISEO:19 for A being Element of Fin X holds f.:A = {} implies A = {}; definition let X be set; cluster empty Element of Fin X; end; definition let X be set; func {}.X -> empty Element of Fin X equals :: SETWISEO:def 1 {}; end; scheme FinSubFuncEx{ A()->non empty set , B()->(Element of Fin A()), P[set,set] } : ex f being Function of A(), Fin A() st for b,a being Element of A() holds a in f.b iff a in B() & P[a,b]; :: theorems related to BinOp of ... definition let X be non empty set, F be BinOp of X; attr F is having_a_unity means :: SETWISEO:def 2 ex x being Element of X st x is_a_unity_wrt F; synonym F has_a_unity; end; canceled 2; theorem :: SETWISEO:22 for X being non empty set, F being BinOp of X holds F has_a_unity iff the_unity_wrt F is_a_unity_wrt F; theorem :: SETWISEO:23 for X being non empty set, F being BinOp of X st F has_a_unity for x being Element of X holds F.(the_unity_wrt F, x) = x & F.(x, the_unity_wrt F) = x; :: M a i n p a r t definition let X be non empty set; cluster non empty Element of Fin X; end; definition let X be non empty set, x be Element of X; redefine func {x} -> Element of Fin X; let y be Element of X; func {x,y} -> Element of Fin X; let z be Element of X; func {x,y,z} -> Element of Fin X; end; definition let X be set; let A,B be Element of Fin X; redefine func A \/ B -> Element of Fin X; end; definition let X be set; let A,B be Element of Fin X; redefine func A \ B -> Element of Fin X; end; scheme FinSubInd1{ X() -> non empty set, P[set] } : for B being Element of Fin X() holds P[B] provided P[{}.X()] and for B' being (Element of Fin X()), b being Element of X() holds P[B'] & not b in B' implies P[B' \/ {b}]; scheme FinSubInd2{ X() -> non empty set, P[Element of Fin X()] } : for B being Element of Fin X() st B <> {} holds P[B] provided for x being Element of X() holds P[{x}] and for B1,B2 being Element of Fin X() st B1 <> {} & B2 <> {} holds P[B1] & P[B2] implies P[B1 \/ B2]; scheme FinSubInd3{ X() -> non empty set, P[set] } : for B being Element of Fin X() holds P[B] provided P[{}.X()] and for B' being (Element of Fin X()), b being Element of X() holds P[B'] implies P[B' \/ {b}]; definition let X, Y be non empty set; let F be BinOp of Y; let B be Element of Fin X; let f be Function of X,Y; assume that B <> {} or F has_a_unity and F is commutative and F is associative; func F $$ (B,f) -> Element of Y means :: SETWISEO:def 3 ex G being Function of Fin X, Y st it = G.B & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G.(B' \/ {x}) = F.(G.B',f.x); end; canceled; theorem :: SETWISEO:25 for X, Y being non empty set for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st (B <> {} or F has_a_unity) & F is idempotent & F is commutative & F is associative for IT being Element of Y holds IT = F $$ (B,f) iff ex G being Function of Fin X, Y st IT = G.B & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B holds G.(B' \/ {x}) = F.(G.B',f.x); reserve X, Y for non empty set, F for (BinOp of Y), B for (Element of Fin X), f for Function of X,Y; theorem :: SETWISEO:26 F is commutative & F is associative implies for b being Element of X holds F $$ ({b},f) = f.b; theorem :: SETWISEO:27 F is idempotent & F is commutative & F is associative implies for a,b being Element of X holds F $$ ({a,b},f) = F.(f.a, f.b); theorem :: SETWISEO:28 F is idempotent & F is commutative & F is associative implies for a,b,c being Element of X holds F $$ ({a,b,c},f) = F.(F.(f.a, f.b), f.c); :: I f B i s n o n e m p t y theorem :: SETWISEO:29 F is idempotent & F is commutative & F is associative & B <> {} implies for x being Element of X holds F $$(B \/ {x}, f) = F.(F $$(B,f),f.x); theorem :: SETWISEO:30 F is idempotent & F is commutative & F is associative implies for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F $$ (B1 \/ B2,f) = F.(F $$ (B1,f),F $$ (B2,f)); theorem :: SETWISEO:31 F is commutative & F is associative & F is idempotent implies for x being Element of X st x in B holds F.(f.x,F$$(B,f)) = F$$(B,f); theorem :: SETWISEO:32 F is commutative & F is associative & F is idempotent implies for B,C being Element of Fin X st B <> {} & B c= C holds F.(F$$(B,f),F$$(C,f)) = F$$(C,f); theorem :: SETWISEO:33 B <> {} & F is commutative & F is associative & F is idempotent implies for a being Element of Y st for b being Element of X st b in B holds f.b = a holds F$$(B,f) = a; theorem :: SETWISEO:34 F is commutative & F is associative & F is idempotent implies for a being Element of Y st f.:B = {a} holds F$$(B,f) = a; theorem :: SETWISEO:35 F is commutative & F is associative & F is idempotent implies for f,g being Function of X,Y for A,B being Element of Fin X st A <> {} & f.:A = g.:B holds F$$(A,f) = F$$(B,g); theorem :: SETWISEO:36 for F,G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F for B being Element of Fin X st B <> {} for f being Function of X,Y for a being Element of Y holds G.(a,F$$(B,f)) = F$$(B,G[;](a,f)); theorem :: SETWISEO:37 for F,G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F for B being Element of Fin X st B <> {} for f being Function of X,Y for a being Element of Y holds G.(F$$(B,f),a) = F$$(B,G[:](f,a)); definition let X, Y be non empty set; let f be Function of X,Y; let A be Element of Fin X; redefine func f.:A -> Element of Fin Y; end; theorem :: SETWISEO:38 for A, X, Y being non empty set for F being BinOp of A st F is idempotent & F is commutative & F is associative for B being Element of Fin X st B <> {} for f being Function of X,Y holds for g being Function of Y,A holds F$$(f.:B,g) = F$$(B,g*f); theorem :: SETWISEO:39 F is commutative & F is associative & F is idempotent implies for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent for f being Function of X, Y for g being Function of Y,Z st for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y) for B being Element of Fin X st B <> {} holds g.(F$$(B,f)) = G$$(B,g*f); :: I f F h a s a u n i t y theorem :: SETWISEO:40 F is commutative & F is associative & F has_a_unity implies for f holds F$$({}.X,f) = the_unity_wrt F; theorem :: SETWISEO:41 F is idempotent & F is commutative & F is associative & F has_a_unity implies for x being Element of X holds F $$(B \/ {x}, f) = F.(F $$(B,f),f.x); theorem :: SETWISEO:42 F is idempotent & F is commutative & F is associative & F has_a_unity implies for B1,B2 being Element of Fin X holds F $$ (B1 \/ B2,f) = F.(F $$ (B1,f),F $$ (B2,f)); theorem :: SETWISEO:43 F is commutative & F is associative & F is idempotent & F has_a_unity implies for f,g being Function of X,Y for A,B being Element of Fin X st f.:A = g.:B holds F$$(A,f) = F$$(B,g); theorem :: SETWISEO:44 for A, X, Y being non empty set for F being BinOp of A st F is idempotent & F is commutative & F is associative & F has_a_unity for B being Element of Fin X for f being Function of X,Y holds for g being Function of Y,A holds F$$(f.:B,g) = F$$(B,g*f); theorem :: SETWISEO:45 F is commutative & F is associative & F is idempotent & F has_a_unity implies for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G has_a_unity for f being Function of X, Y for g being Function of Y,Z st g.the_unity_wrt F = the_unity_wrt G & for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y) for B being Element of Fin X holds g.(F$$(B,f)) = G$$(B,g*f); :: Funkcja wprowadzona powyzej konieczna jest do zakastowania :: wyniku operacji unii. Jest to Element of DOMAIN , :: co nie rozszerza sie do Element of DOMAIN definition let A be set; func FinUnion A -> BinOp of Fin A means :: SETWISEO:def 4 for x,y being Element of Fin A holds it.(x,y) = (x \/ y); end; reserve A for set, x,y,z for Element of Fin A; canceled 3; theorem :: SETWISEO:49 FinUnion A is idempotent; theorem :: SETWISEO:50 FinUnion A is commutative; theorem :: SETWISEO:51 FinUnion A is associative; theorem :: SETWISEO:52 {}.A is_a_unity_wrt FinUnion A; theorem :: SETWISEO:53 FinUnion A has_a_unity; theorem :: SETWISEO:54 the_unity_wrt FinUnion A is_a_unity_wrt FinUnion A; theorem :: SETWISEO:55 the_unity_wrt FinUnion A = {}; reserve X,Y for non empty set, A for set, f for (Function of X, Fin A), i,j,k for (Element of X); definition let X be non empty set, A be set; let B be Element of Fin X; let f be Function of X, Fin A; func FinUnion(B,f) -> Element of Fin A equals :: SETWISEO:def 5 FinUnion A $$(B,f); end; theorem :: SETWISEO:56 FinUnion({i},f) = f.i; theorem :: SETWISEO:57 FinUnion({i,j},f) = f.i \/ f.j; theorem :: SETWISEO:58 FinUnion({i,j,k},f) = f.i \/ f.j \/ f.k; theorem :: SETWISEO:59 FinUnion({}.X,f) = {}; theorem :: SETWISEO:60 for B being Element of Fin X holds FinUnion(B \/ {i}, f) = FinUnion(B,f) \/ f.i; theorem :: SETWISEO:61 for B being Element of Fin X holds FinUnion(B,f) = union (f.:B); theorem :: SETWISEO:62 for B1,B2 being Element of Fin X holds FinUnion(B1 \/ B2, f) = FinUnion(B1,f) \/ FinUnion(B2,f); theorem :: SETWISEO:63 for B being Element of Fin X for f being Function of X,Y holds for g being Function of Y,Fin A holds FinUnion(f.:B,g) = FinUnion(B,g*f); theorem :: SETWISEO:64 for A,X being non empty set, Y being set for G being BinOp of A st G is commutative & G is associative & G is idempotent for B being Element of Fin X st B <> {} for f being (Function of X,Fin Y), g being Function of Fin Y,A st for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y) holds g.(FinUnion(B,f)) = G$$(B,g*f); theorem :: SETWISEO:65 for Z being non empty set, Y being set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G has_a_unity for f being Function of X, Fin Y for g being Function of Fin Y,Z st g.{}.Y = the_unity_wrt G & for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y) for B being Element of Fin X holds g.(FinUnion(B,f)) = G$$(B,g*f); definition let A be set; func singleton A -> Function of A, Fin A means :: SETWISEO:def 6 for x being set st x in A holds it.x = {x}; end; canceled; theorem :: SETWISEO:67 for A being non empty set for f being Function of A, Fin A holds f = singleton A iff for x being Element of A holds f.x = {x}; theorem :: SETWISEO:68 for x being set, y being Element of X holds x in singleton X.y iff x = y; theorem :: SETWISEO:69 for x,y,z being Element of X st x in singleton X.z & y in singleton X.z holds x = y; theorem :: SETWISEO:70 for B being Element of Fin X, x being set holds x in FinUnion(B, f) iff ex i being Element of X st i in B & x in f.i; theorem :: SETWISEO:71 for B being Element of Fin X holds FinUnion(B, singleton X) = B; theorem :: SETWISEO:72 for Y,Z being set for f being Function of X, Fin Y for g being Function of Fin Y, Fin Z st g.{}.Y = {}.Z & for x,y being Element of Fin Y holds g.(x \/ y) = g.x \/ g.y for B being Element of Fin X holds g.(FinUnion(B,f)) = FinUnion(B,g*f);

Back to top