Semilattice Operations on Finite Subsets

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III-24.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.

MML Identifier: SETWISEO

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.