Enumerated Sets

Andrzej Trybulec

Warsaw University, Bialystok

Supported by RPBP.III-24.C1.

Summary.

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

Contents (PDF format)

Bibliography

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