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

Enumerated Sets

Andrzej Trybulec
Warsaw University, Bialystok
Supported by RPBP.III-24.C1.


We prove basic facts about enumerated sets: definitional theorems and their immediate consequences, some theorems related to the decomposition of an enumerated set into union of two sets, facts about removing elements that occur more than once, and facts about permutations of enumerated sets (with the length $\le$ 4). The article includes also schemes enabling instantiation of up to nine universal quantifiers.

MML Identifier: ENUMSET1

The terminology and notation used in this paper have been introduced in the following articles [1]

Contents (PDF format)


[1] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

Received January 8, 1989

[ Download a postscript version, MML identifier index, Mizar home page]