Rodin User’s Handbook v.2.8: Sets

3.3.4 Sets

3.3.4.1 Set comprehensions

$\{ ~ \textit{ids}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ \|~ \textsf{E}~ \}$	`{ids.P\|E}`	Set comprehension
$\{ ~ \textsf{E}~ \|~ \textsf{P}~ \}$	`{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 $\textsf{P}$ . The predicate $\textsf{P}$ and $\textsf{E}$ can contain references to the identifiers ids.

The set comprehension $\{ ~ x_1,\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ \}$ contains all values of $\textsf{E}$ for the values of $x_1,\ldots ,x_ n$ where $\textsf{P}$ is true.

$\{ ~ \textsf{E}~ |~ \textsf{P}~ \}$ is a short form for $\{ ~ \textsl{Free}(\textsf{E})~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ \}$ where $\textsl{Free}(\textsf{E})$ denotes the list of free identifiers occurring in $\textsf{E}$ (see Section 3.3.1.3)).

Definition

$\{ ~ \textsf{E}~ |~ \textsf{P}~ \} \mathrel {\widehat=}\{ ~ \textsl{Free}(\textsf{E})~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ \}$

Types

With $x_1\in \alpha _1, \ldots , x_ n\in \alpha _ n$ and $\textsf{E}\in \beta$ :
$\{ ~ x_1,\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ \} \in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$
$\{ ~ \textsf{E}~ |~ \textsf{P}~ \} \in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$

WD

$\mathcal{L}(\{ ~ x_1,\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}~ \} ) \quad \mathrel {\widehat=}\quad \forall x_1,\ldots ,x_ n \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{E}))$
$\mathcal{L}(\{ ~ \textsf{E}~ |~ \textsf{P}~ \} ) \quad \mathrel {\widehat=}\quad \forall \textsl{Free}(\textsf{E}) \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{E}))$

Example

The following set comprehensions contain all the first 10 squares numbers:
$\{ 1,4,9,16,25,36,49,64,81,100\}$
$= \{ ~ x~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\in 1\mathbin {.\mkern 1mu.}10~ |~ x\mathbin {\widehat{\enskip }}2\}$
$= \{ ~ x~ |~ \exists y \mathord {\mkern 1mu\cdot \mkern 1mu}y\in 1\mathbin {.\mkern 1mu.}10 \land x=y\mathbin {\widehat{\enskip }}2~ \}$
$= \{ ~ x\mathbin {\widehat{\enskip }}2~ |~ x\in 1\mathbin {.\mkern 1mu.}10~ \}$

3.3.4.2 Basic sets

$\emptyset$	`{}`	Empty set
$\{ \textit{exprs}\}$	`{exprs}`	Set extension

Description

$\textit{exprs}$ is a comma-separated list of one or more expressions of the same type.

The empty set $\emptyset$ contains no elements. The set extension $\{ \textsf{E}_1,\ldots ,\textsf{E}_ n\}$ is the set that contains exactly the elements $\textsf{E}_1,\ldots ,\textsf{E}_ n$ .

Definition

$\emptyset \mathrel {\widehat=}\{ ~ x~ |~ \mathord {\bot }~ \}$
$\{ \textsf{E}_1,\ldots ,\textsf{E}_ n\} \mathrel {\widehat=}\{ ~ x~ |~ x=\textsf{E}_1\lor \ldots \lor x=\textsf{E}_ n\}$

Types

$\emptyset \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ , where $\alpha$ is an arbitrary type.
$\{ \textsf{E}_1,\ldots ,\textsf{E}_ n\} \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ with $\textsf{E}_1\in \alpha ,\ldots ,\textsf{E}_ n\in \alpha$

WD

$\mathcal{L}(\emptyset ) \mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\{ \textsf{E}_1,\ldots ,\textsf{E}_ n\} ) \mathrel {\widehat=}\mathcal{L}(\textsf{E}_1) \land \ldots \land \mathcal{L}(\textsf{E}_ n)$

3.3.4.3 Subsets

$\subseteq$	`<:`	subset
$\not\subseteq$	`/<:`	not a subset
$\subset$	`<<:`	strict subset
$\not\subset$	`/<<:`	not a strict subset

Description: $\textsf{S}\subseteq \textsf{T}$ checks if $\textsf{S}$ is a subset of $\textsf{T}$ , i.e. if all elements of $\textsf{S}$ occur in $\textsf{T}$ . $\textsf{S}\subset \textsf{T}$ checks if $\textsf{S}$ is a subset of $\textsf{T}$ and $\textsf{S}$ does not equal $\textsf{T}$ . $\textsf{S}\not\subseteq \textsf{T}$ and $\textsf{S}\not\subset \textsf{T}$ are the respective negated variants.
Definition: $\textsf{S}\subseteq \textsf{T}\mathrel {\widehat=}\forall e \mathord {\mkern 1mu\cdot \mkern 1mu}e\in \textsf{S}\mathbin \Rightarrow e\in \textsf{T}$
$\textsf{S}\not\subseteq \textsf{T}\mathrel {\widehat=}\lnot (\textsf{S}\subseteq \textsf{T})$
$\textsf{S}\subset \textsf{T}\mathrel {\widehat=}\textsf{S}\subseteq \textsf{T}\land \textsf{S}\neq \textsf{T}$
$\textsf{S}\not\subset \textsf{T}\mathrel {\widehat=}\lnot (\textsf{S}\subset \textsf{T})$
Types: $\textsf{S}\mathbin {\Box }\textsf{T}$ is a predicate with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ , $\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ for each operator $\mathbin {\Box }$ of $\subseteq$ , $\not\subseteq$ , $\subset$ , $\not\subset$ .
WD: $\mathcal{L}(\textsf{S}\mathbin {\Box }\textsf{T}) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \mathcal{L}(\textsf{T})$ for each operator $\mathbin {\Box }$ of $\subseteq$ , $\not\subseteq$ , $\subset$ , $\not\subset$ .

3.3.4.4 Operations on sets

$\mathbin {\mkern 1mu\cup \mkern 1mu}$	`\/`	Union
$\mathbin {\mkern 1mu\cap \mkern 1mu}$	`/\`	Intersection
$\setminus$	`\`	Set subtraction

Description: The union $\textsf{S}\mathbin {\mkern 1mu\cup \mkern 1mu}\textsf{T}$ denotes the set that contains all elements that are in $\textsf{S}$ or $\textsf{T}$ . The intersection $\textsf{S}\mathbin {\mkern 1mu\cap \mkern 1mu}\textsf{T}$ denotes the set that contains all elements that are in both $\textsf{S}$ and $\textsf{T}$ . The set subtraction or set difference $\textsf{S}\setminus \textsf{T}$ denotes all elements that are in $\textsf{S}$ but not in $\textsf{T}$ .
Definition: $\textsf{S}\mathbin {\mkern 1mu\cup \mkern 1mu}\textsf{T}\mathrel {\widehat=}\{ ~ x~ |~ x\in \textsf{S}\lor x\in \textsf{T}~ \}$
$\textsf{S}\mathbin {\mkern 1mu\cap \mkern 1mu}\textsf{T}\mathrel {\widehat=}\{ ~ x~ |~ x\in \textsf{S}\land x\in \textsf{T}~ \}$
$\textsf{S}\setminus \textsf{T}\mathrel {\widehat=}\{ ~ x~ |~ x\in \textsf{S}\land x\not\in \textsf{T}~ \}$
Types: $\textsf{S}\mathbin {\Box }\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\textsf{T}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ for each operator $\mathbin {\Box }$ of $\mathbin {\mkern 1mu\cup \mkern 1mu}$ , $\mathbin {\mkern 1mu\cap \mkern 1mu}$ , $\setminus$
WD: $\mathcal{L}(\textsf{S}\mathbin {\Box }\textsf{T}) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \mathcal{L}(\textsf{T})$ for each operator $\mathbin {\Box }$ of $\mathbin {\mkern 1mu\cup \mkern 1mu}$ , $\mathbin {\mkern 1mu\cap \mkern 1mu}$ , $\setminus$

3.3.4.5 Power sets

$\mathop {\mathbb P\hbox{}}\nolimits$	`POW`	Power set
$\mathop {\mathbb P\hbox{}}\nolimits _1$	`POW1`	Set of non-empty subsets

Description: $\mathop {\mathbb P\hbox{}}\nolimits (\textsf{S})$ denotes the set of all subsets of the set $\textsf{S}$ . $\mathop {\mathbb P\hbox{}}\nolimits (\textsf{S})$ denotes the set of all non-empty subsets of the set $\textsf{S}$ .
Definition: $\mathop {\mathbb P\hbox{}}\nolimits (\textsf{S}) \mathrel {\widehat=}\{ ~ x~ |~ x\subseteq \textsf{S}~ \}$
$\mathop {\mathbb P\hbox{}}\nolimits _1(\textsf{S}) \mathrel {\widehat=}\mathop {\mathbb P\hbox{}}\nolimits (\textsf{S})\setminus \{ \emptyset \}$
Types: $\mathop {\mathbb P\hbox{}}\nolimits (\alpha )\in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha ))$ and $\mathop {\mathbb P\hbox{}}\nolimits _1(\alpha )\in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha ))$ with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ .
WD: $\mathcal{L}(\mathop {\mathbb P\hbox{}}\nolimits (\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S})$
$\mathcal{L}(\mathop {\mathbb P\hbox{}}\nolimits _1(\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S})$

3.3.4.6 Finite sets

$\mathrm{finite}$	`finite`	Finite set
$\mathop {\mathrm{card}}\nolimits$	`card`	Cardinality of a finite set

Description: $\mathrm{finite}(\textsf{S})$ is a predicate that states that $\textsf{S}$ is a finite set. $\mathop {\mathrm{card}}\nolimits (\textsf{S})$ denotes the cardinality of $\textsf{S}$ . The cardinality is only defined for finite sets.
Definition: $\mathrm{finite}(\textsf{S}) ~ \mathrel {\widehat=}~ \exists n,b~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ n\in \mathord {\mathbb N}\land b\in \textsf{S}\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } 1\mathbin {.\mkern 1mu.}n$
$\exists b~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ b\in \textsf{S}\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } 1\mathbin {.\mkern 1mu.}\mathop {\mathrm{card}}\nolimits (\textsf{S})$
Types: $\mathrm{finite}(\textsf{S})$ is a predicate and $\mathop {\mathrm{card}}\nolimits (\textsf{S})\in \mathord {\mathbb Z}$ with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ , i.e. $\textsf{S}$ must be a set.
WD: $\mathcal{L}(\mathrm{finite}(\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S})$
$\mathcal{L}(\mathop {\mathrm{card}}\nolimits (\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \mathrm{finite}(\textsf{S})$

3.3.4.7 Partition

$\mathrm{partition}$

partition

Partitions of a set

Description

$\mathrm{partition}(\textsf{S},\textsf{s}_1,\ldots ,\textsf{s}_ n)$ is a predicate that states that the sets $\textsf{s}_1,\ldots ,\textsf{s}_ n$ constitute a partition of $\textsf{S}$ . The union of all elements of a partition is $\textsf{S}$ and all elements are disjoint.

$\mathrm{partition}(\textsf{S})$ is equivalent to $\textsf{S}= \emptyset$ and $\mathrm{partition}(\textsf{S},\textsf{s})$ to $\textsf{S}= \textsf{s}$ .

Definition

$\mathrm{partition}(\textsf{S},\textsf{s}_1,\ldots ,\textsf{s}_ n) \mathrel {\widehat=}\textsf{S}=\textsf{s}_1\mathbin {\mkern 1mu\cup \mkern 1mu}\ldots \mathbin {\mkern 1mu\cup \mkern 1mu}\textsf{s}_ n \land \forall i,j \mathord {\mkern 1mu\cdot \mkern 1mu}i\neq j \mathbin \Rightarrow \textsf{s}_ i\mathbin {\mkern 1mu\cap \mkern 1mu}\textsf{s}_ j = \emptyset$

Types

$\mathrm{partition}(\textsf{S},\textsf{s}_1,\ldots ,\textsf{s}_ n)$ is a predicate with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\textsf{s}_ i\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ for $i\in 1\mathbin {.\mkern 1mu.}n$

WD

$\mathcal{L}(\mathrm{partition}(\textsf{S},\textsf{s}_1,\ldots ,\textsf{s}_ n)) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \mathcal{L}(\textsf{s}_1) \land \ldots \land \mathcal{L}(\textsf{s}_ n)$

3.3.4.8 Generalized union and intersection

$\mathrm{union}$	`union`	Generalized union
$\mathrm{inter}$	`inter`	Generalized intersection

Description: $\mathrm{union}(\textsf{S})$ is the union of all elements of $\textsf{S}$ . $\mathrm{inter}(\textsf{S})$ is the intersection of all elements of $\textsf{S}$ . The intersection is only defined for non-empty $\textsf{S}$ .
Definition: $\mathrm{union}(\textsf{S}) \mathrel {\widehat=}\{ ~ x~ |~ \exists s \mathord {\mkern 1mu\cdot \mkern 1mu}s\in \textsf{S}\land x\in s~ \}$
$\mathrm{inter}(\textsf{S}) \mathrel {\widehat=}\{ ~ x~ |~ \forall s \mathord {\mkern 1mu\cdot \mkern 1mu}s\in \textsf{S}\mathbin \Rightarrow x\in s~ \}$
Types: $\mathrm{union}(\textsf{S})\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\mathrm{inter}(\textsf{S})\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ with $\textsf{S}\in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha ))$ .
WD: $\mathcal{L}(\mathrm{union}(\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S})$
$\mathcal{L}(\mathrm{inter}(\textsf{S})) \mathrel {\widehat=}\mathcal{L}(\textsf{S}) \land \textsf{S}\neq \emptyset$

3.3.4.9 Quantified union and intersection

$\bigcup \nolimits$	`UNION`	Quantified union
$\bigcap \nolimits$	`INTER`	Quantified intersection

Description

$\bigcup \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}$ is the union of all values of $\textsf{E}$ for valuations of the identifiers $x_1\ldots ,x_ n$ that fulfill the predicate $\textsf{P}$ . The types of $x_1,\ldots ,x_ n$ must be inferable by $\textsf{P}$ .

Analogously is $\bigcap \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}$ the intersection of all values of $\textsf{E}$ for valuations of the identifiers $x_1\ldots ,x_ n$ that fulfill the predicate $\textsf{P}$ .

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: $\bigcup \nolimits \textsf{E}~ |~ \textsf{P}$ and $\bigcap \nolimits \textsf{E}~ |~ \textsf{P}$ .

Definition

$\bigcup \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}= \mathop {\mathrm{union}}\nolimits (\{ ~ x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}\} )$
$\bigcap \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}= \mathop {\mathrm{inter}}\nolimits (\{ ~ x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}\} )$
$\bigcup \nolimits \textsf{E}~ |~ \textsf{P}= \bigcup \nolimits \textsl{Free}(\textsf{E})~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}$
$\bigcap \nolimits \textsf{E}~ |~ \textsf{P}= \bigcap \nolimits \textsl{Free}(\textsf{E})~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}$

Types

With $\textsf{E}\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\textsf{P}$ being a predicate:
$(\bigcup \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}) \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$
$(\bigcap \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}) \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$
$(\bigcup \nolimits \textsf{E}~ |~ \textsf{P}) \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$
$(\bigcap \nolimits \textsf{E}~ |~ \textsf{P}) \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$

WD

$\mathcal{L}(\bigcup \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}) \mathrel {\widehat=}(~ \forall x_1\ldots ,x_ n \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{E}))~ )$
$\mathcal{L}(\bigcap \nolimits x_1\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \textsf{P}~ |~ \textsf{E}) \mathrel {\widehat=}(~ \forall x_1\ldots ,x_ n \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{E}))~ ) \land \exists x_1\ldots ,x_ n \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P})$
$\mathcal{L}(\bigcup \nolimits \textsf{E}~ |~ \textsf{P}) \mathrel {\widehat=}(~ \forall \textsl{Free}(\textsf{E}) \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{E}))~ )$
$\mathcal{L}(\bigcap \nolimits \textsf{E}~ |~ \textsf{P}) \mathrel {\widehat=}(~ \forall \textsl{Free}(\textsf{E}) \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P}) \land (\textsf{P}\mathbin \Rightarrow \mathcal{L}(\textsf{E}))~ ) \land \exists \textsl{Free}(\textsf{E}) \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(\textsf{P})$