:: 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);