## 3.3.4 Sets

### 3.3.4.1 Set comprehensions

 {ids.P|E} Set comprehension {E|P} Set comprehension (short form)
Description

ids is a comma-separated list of one ore more identifiers whose type must be inferable by the predicate . The predicate and can contain references to the identifiers ids.

The set comprehension contains all values of for the values of where is true.

is a short form for where denotes the list of free identifiers occurring in (see Section 3.3.1.3)).

Definition

Types

With and :

WD

Example

The following set comprehensions contain all the first 10 squares numbers:

### 3.3.4.2 Basic sets

 {} Empty set {exprs} Set extension
Description

is a comma-separated list of one or more expressions of the same type.

The empty set contains no elements. The set extension is the set that contains exactly the elements .

Definition

Types

, where is an arbitrary type.
with

WD

### 3.3.4.3 Subsets

 <: subset /<: not a subset <<: strict subset /<<: not a strict subset
Description

checks if is a subset of , i.e. if all elements of occur in . checks if is a subset of and does not equal . and are the respective negated variants.

Definition

Types

is a predicate with , for each operator of , , , .

WD

for each operator of , , , .

### 3.3.4.4 Operations on sets

 \/ Union /\ Intersection \ Set subtraction
Description

The union denotes the set that contains all elements that are in or . The intersection denotes the set that contains all elements that are in both and . The set subtraction or set difference denotes all elements that are in but not in .

Definition

Types

with and for each operator of , ,

WD

for each operator of , ,

### 3.3.4.5 Power sets

 POW Power set POW1 Set of non-empty subsets
Description

denotes the set of all subsets of the set . denotes the set of all non-empty subsets of the set .

Definition

Types

and with .

WD

### 3.3.4.6 Finite sets

 finite Finite set card Cardinality of a finite set
Description

is a predicate that states that is a finite set. denotes the cardinality of . The cardinality is only defined for finite sets.

Definition

Types

is a predicate and with , i.e. must be a set.

WD

### 3.3.4.7 Partition

 partition Partitions of a set
Description

is a predicate that states that the sets constitute a partition of . The union of all elements of a partition is and all elements are disjoint.

is equivalent to and to .

Definition

Types

is a predicate with and for

WD

### 3.3.4.8 Generalized union and intersection

 union Generalized union inter Generalized intersection
Description

is the union of all elements of . is the intersection of all elements of . The intersection is only defined for non-empty .

Definition

Types

and with .

WD

### 3.3.4.9 Quantified union and intersection

 UNION Quantified union INTER Quantified intersection
Description

is the union of all values of for valuations of the identifiers that fulfill the predicate . The types of must be inferable by .

Analogously is the intersection of all values of for valuations of the identifiers that fulfill the predicate .

Like set comprehensions (3.3.4.1), the quantified union and intersection have a short form where the free variables of the expression are quantified implicitly: and .

Definition

Types

With and being a predicate:

WD