:: Semilattice Operations on Finite Subsets :: by Andrzej Trybulec :: :: Received September 18, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TARSKI, XBOOLE_0, FUNCT_1, RELAT_1, ZFMISC_1, SUBSET_1, FINSUB_1, BINOP_1, FINSET_1, FUNCOP_1, SETWISEO; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, FINSUB_1, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1; constructors ENUMSET1, PARTFUN1, BINOP_1, FUNCOP_1, FINSET_1, FINSUB_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, FINSUB_1, RELAT_1, FUNCT_3, ZFMISC_1; requirements BOOLE, SUBSET; begin :: Auxiliary Theorems reserve x,y,z,X,Y for set; theorem :: SETWISEO:1 {x} c= {x,y,z}; theorem :: SETWISEO:2 {x,y} c= {x,y,z}; ::\$CT 3 theorem :: SETWISEO:6 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:7 for x being Element of X holds x in f"{f.x}; theorem :: SETWISEO:8 for x being Element of X holds Im(f,x) = {f.x}; :: Theorems related to Fin ... theorem :: SETWISEO:9 for B being Element of Fin X for x st x in B holds x is Element of X; theorem :: SETWISEO:10 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:11 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; theorem :: SETWISEO:12 for B being Element of Fin X st B <> {} ex x being Element of X st x in B; theorem :: SETWISEO:13 for A being Element of Fin X holds f.:A = {} implies A = {}; registration let X be set; cluster empty for Element of Fin X; end; definition let X be set; func {}.X -> empty Element of Fin X equals :: SETWISEO:def 1 {}; end; scheme :: SETWISEO:sch 1 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; end; theorem :: SETWISEO:14 for X being non empty set, F being BinOp of X holds F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F; theorem :: SETWISEO:15 for X being non empty set, F being BinOp of X st F is having_a_unity for x being Element of X holds F.(the_unity_wrt F, x) = x & F.(x , the_unity_wrt F) = x; :: Main part registration let X be non empty set; cluster non empty for Element of Fin X; end; notation let X be non empty set, x be Element of X; synonym {.x.} for {x}; let y be Element of X; synonym {.x,y.} for {x,y}; let z be Element of X; synonym {.x,y,z.} for {x,y,z}; 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; redefine func {.x,y.} -> Element of Fin X; let z be Element of X; redefine 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 :: SETWISEO:sch 2 FinSubInd1{ X() -> non empty set, P[set] } : for B being Element of Fin X() holds P[B] provided P[{}.X()] and for B9 being (Element of Fin X()), b being Element of X() holds P[B9 ] & not b in B9 implies P[B9 \/ {b}]; scheme :: SETWISEO:sch 3 FinSubInd2{ X() -> non empty set, P[Element of Fin X()] } : for B being non empty Element of Fin X() holds P[B] provided for x being Element of X() holds P[{.x.}] and for B1,B2 being non empty Element of Fin X() st P[B1] & P[B2] holds P[B1 \/ B2]; scheme :: SETWISEO:sch 4 FinSubInd3{ X() -> non empty set, P[set] } : for B being Element of Fin X() holds P[B] provided P[{}.X()] and for B9 being (Element of Fin X()), b being Element of X() holds P[B9 ] implies P[B9 \/ {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 is having_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 B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B \ B9 holds G.(B9 \/ {x}) = F.(G.B9,f.x); end; theorem :: SETWISEO:16 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 is having_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 B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B holds G.(B9 \/ {x}) = F.(G.B9,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:17 F is commutative & F is associative implies for b being Element of X holds F \$\$ ({.b.},f) = f.b; theorem :: SETWISEO:18 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:19 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) ; :: If B is non empty theorem :: SETWISEO:20 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:21 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:22 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:23 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:24 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:25 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:26 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:27 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:28 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:29 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:30 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); :: If F has a unity theorem :: SETWISEO:31 F is commutative & F is associative & F is having_a_unity implies for f holds F\$\$({}.X,f) = the_unity_wrt F; theorem :: SETWISEO:32 F is idempotent & F is commutative & F is associative & F is having_a_unity implies for x being Element of X holds F \$\$(B \/ {.x.}, f) = F.( F \$\$(B,f),f.x); theorem :: SETWISEO:33 F is idempotent & F is commutative & F is associative & F is having_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:34 F is commutative & F is associative & F is idempotent & F is having_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:35 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 is having_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:36 F is commutative & F is associative & F is idempotent & F is having_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 is having_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); 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; theorem :: SETWISEO:37 FinUnion A is idempotent; theorem :: SETWISEO:38 FinUnion A is commutative; theorem :: SETWISEO:39 FinUnion A is associative; theorem :: SETWISEO:40 {}.A is_a_unity_wrt FinUnion A; theorem :: SETWISEO:41 FinUnion A is having_a_unity; theorem :: SETWISEO:42 the_unity_wrt FinUnion A is_a_unity_wrt FinUnion A; theorem :: SETWISEO:43 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:44 FinUnion({.i.},f) = f.i; theorem :: SETWISEO:45 FinUnion({.i,j.},f) = f.i \/ f.j; theorem :: SETWISEO:46 FinUnion({.i,j,k.},f) = f.i \/ f.j \/ f.k; theorem :: SETWISEO:47 FinUnion({}.X,f) = {}; theorem :: SETWISEO:48 for B being Element of Fin X holds FinUnion(B \/ {.i.}, f) = FinUnion(B,f) \/ f.i; theorem :: SETWISEO:49 for B being Element of Fin X holds FinUnion(B,f) = union (f.:B); theorem :: SETWISEO:50 for B1,B2 being Element of Fin X holds FinUnion(B1 \/ B2, f) = FinUnion(B1,f) \/ FinUnion(B2,f); theorem :: SETWISEO:51 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:52 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:53 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 is having_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 object st x in A holds it.x = {x}; end; theorem :: SETWISEO:54 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:55 for x being set, y being Element of X holds x in singleton X.y iff x = y; theorem :: SETWISEO:56 for x,y,z being Element of X st x in singleton X.z & y in singleton X. z holds x = y; theorem :: SETWISEO:57 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:58 for B being Element of Fin X holds FinUnion(B, singleton X) = B; theorem :: SETWISEO:59 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);