Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### 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);
```