Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Semilattice Operations on Finite Subsets

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III24.C1.
Summary.

In the article we deal with a binary operation that is associative,
commutative.
We define for such an operation a functor that
depends on two more arguments: a finite set of indices and a function indexing
elements of the domain of the operation and yields the result of applying
the operation to all indexed elements. The definition has a restriction
that requires that either the set of indices is non empty or the operation
has the unity.
We prove theorems describing
some properties of the functor introduced. Most of them we prove in two
versions depending on which requirement is fulfilled.
In the second part we deal with the union of finite sets that enjoys
mentioned above properties. We prove analogs of the theorems proved in the
first part.
We precede the main part of the article with auxiliary theorems related to
boolean properties of sets, enumerated sets, finite subsets, and functions.
We define a casting function that yields to a set the empty set typed as
a finite subset of the set.
We prove also two schemes of the induction on finite sets.
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[5]
[8]
[9]
[2]
[7]
[3]
[1]
[4]
Contents (PDF format)
Bibliography
 [1]
Czeslaw Bylinski.
Binary operations.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Andrzej Trybulec.
Binary operations applied to functions.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Andrzej Trybulec.
Enumerated sets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Andrzej Trybulec and Agata Darmochwal.
Boolean domains.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received September 18, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]