User Manual for Rodin v.2.3: Sets

3.3.4 Sets

3.3.4.1 Set comprehensions

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

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

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

Definition

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

Types

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

WD

$\mathcal{L}(\{ ~ x_1,\ldots ,x_ n~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ |~ E~ \} ) \quad \mathrel {\widehat=}\quad \forall x_1,\ldots ,x_ n \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(P) \land (P \mathbin \Rightarrow \mathcal{L}(E))$
$\mathcal{L}(\{ ~ E~ |~ P~ \} ) \quad \mathrel {\widehat=}\quad \forall \textsl{Free}(E) \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(P) \land (P \mathbin \Rightarrow \mathcal{L}(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 $\{ E_1,\ldots ,E_ n\}$ is the set that contains exactly the elements $E_1,\ldots ,E_ n$ .

Definition

$\emptyset = \{ ~ x~ |~ \mathord {\bot }~ \}$
$\{ E_1,\ldots ,E_ n\} = \{ ~ x~ |~ x=E_1\lor \ldots \lor x=E_ n\}$

Types

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

WD

$\mathcal{L}(\emptyset ) \mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\{ E_1,\ldots ,E_ n\} ) \mathrel {\widehat=}\mathcal{L}(E_1) \land \ldots \land \mathcal{L}(E_ n)$

3.3.4.3 Subsets

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

Description: $S\subseteq T$ checks if $S$ is a subset of $T$ , i.e. if all elements of $S$ occurr in $T$ . $S\subset T$ checks if $S$ is a subset of $T$ and $S$ does not equal $T$ . $S\not\subseteq T$ resp. $S\not\subset T$ are the respective negated variants.
Definition: $S \subseteq T \mathrel {\widehat=}\forall e \mathord {\mkern 1mu\cdot \mkern 1mu}e\in S \mathbin \Rightarrow e\in T$
$S \not\subseteq T \mathrel {\widehat=}\lnot (S \subseteq T)$
$S \subset T \mathrel {\widehat=}S \subseteq T \land S\neq T$
$S \not\subset T \mathrel {\widehat=}\lnot (S \subset T)$
Types: $S \mathbin {\Box }T$ is a predicate with $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ , $T\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and for each operator $\mathbin {\Box }$ of $\subseteq$ , $\not\subseteq$ , $\subset$ , $\not\subset$ .
WD: $\mathcal{L}(S\mathbin {\Box }T) \mathrel {\widehat=}\mathcal{L}(S) \land \mathcal{L}(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 $S\mathbin {\mkern 1mu\cup \mkern 1mu}T$ denotes the set that contains all elements that are in $S$ or $T$ . The intersection $S\mathbin {\mkern 1mu\cap \mkern 1mu}T$ denotes the set that contains all elment that are in both $S$ and $T$ . The set subtraction or set difference $S\setminus T$ denotes all elements that are in $S$ but not in $T$ .
Definition: $S\mathbin {\mkern 1mu\cup \mkern 1mu}T = \{ ~ x~ |~ x\in S\lor x\in T~ \}$
$S\mathbin {\mkern 1mu\cap \mkern 1mu}T = \{ ~ x~ |~ x\in S\land x\in T~ \}$
$S\setminus T = \{ ~ x~ |~ x\in S\land x\not\in T~ \}$
Types: $S\mathbin {\Box }T\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ with $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $T\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and for each operator $\mathbin {\Box }$ of $\mathbin {\mkern 1mu\cup \mkern 1mu}$ , $\mathbin {\mkern 1mu\cap \mkern 1mu}$ , $\setminus$
WD: $\mathcal{L}(S\mathbin {\Box }T) \mathrel {\widehat=}\mathcal{L}(S) \land \mathcal{L}(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 (S)$ denotes the set of all subsets of the set $S$ . $\mathop {\mathbb P\hbox{}}\nolimits (S)$ denotes the set of all non-empty subsets of the set $S$ .
Definition: $\mathop {\mathbb P\hbox{}}\nolimits (S) = \{ ~ x~ |~ x\subseteq S~ \}$
$\mathop {\mathbb P\hbox{}}\nolimits _1(S) = \mathop {\mathbb P\hbox{}}\nolimits (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 $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ .
WD: $\mathcal{L}(\mathop {\mathbb P\hbox{}}\nolimits (S)) \mathrel {\widehat=}\mathcal{L}(S)$
$\mathcal{L}(\mathop {\mathbb P\hbox{}}\nolimits _1(S)) \mathrel {\widehat=}\mathcal{L}(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}(S)$ is a predicate that states that $S$ is a finite set. $\mathop {\mathrm{card}}\nolimits (S)$ denotes the cardinality of $S$ . The cardinality is only defined for finite sets.
Definition: $\mathrm{finite}(S) ~ \mathrel {\widehat=}~ \exists n,b~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ n\in \mathord {\mathbb N}\land b\in S\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } 1\mathbin {.\mkern 1mu.}n$
$\mathop {\mathrm{card}}\nolimits (S)=n ~ \mathrel {\widehat=}~ \exists b~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ b\in S\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } 1\mathbin {.\mkern 1mu.}n$
Types: $\mathrm{finite}(S)$ is a predicate and $\mathop {\mathrm{card}}\nolimits (S)\in \mathord {\mathbb Z}$ with $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ , i.e. $S$ must be a set.
WD: $\mathcal{L}(\mathrm{finite}(S)) \mathrel {\widehat=}\mathcal{L}(S)$
$\mathcal{L}(\mathop {\mathrm{card}}\nolimits (S)) \mathrel {\widehat=}\mathcal{L}(S) \land \mathrm{finite}(S)$

3.3.4.7 Partition

$\mathrm{partition}$

partition

Partitions of a set

Description

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

$\mathrm{partition}(S)$ is equivalent to $S = \emptyset$ .

Definition

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

Types

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

WD

$\mathcal{L}(\mathrm{partition}(S,s_1,\ldots ,s_ n)) \mathrel {\widehat=}\mathcal{L}(S) \land \mathcal{L}(s_1) \land \ldots \land \mathcal{L}(s_ n)$

3.3.4.8 Generalized union and intersection

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

Description: $\mathrm{union}(S)$ is the union of all elements of $S$ . $\mathrm{inter}(S)$ is the intersection of all elements of $S$ . The intersection is only defined for non-empty $S$ .
Definition: $\mathrm{union}(S) = \{ ~ x~ |~ \exists s \mathord {\mkern 1mu\cdot \mkern 1mu}s\in S \land x\in s~ \}$
$\mathrm{inter}(S) = \{ ~ x~ |~ \forall s \mathord {\mkern 1mu\cdot \mkern 1mu}s\in S \mathbin \Rightarrow x\in s~ \}$
Types: $\mathrm{union}(S)\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\mathrm{inter}(S)\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ with $S\in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha ))$ .
WD: $\mathcal{L}(\mathrm{union}(S)) \mathrel {\widehat=}\mathcal{L}(S)$
$\mathcal{L}(\mathrm{inter}(S)) \mathrel {\widehat=}\mathcal{L}(S) \land 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}~ P~ |~ E$ is the union of all values of $E$ for valuations of the identifiers $x_1\ldots ,x_ n$ that fulfill the predicate $P$ . The types of $x_1,\ldots ,x_ n$ must be inferable by $P$ .

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

Like set comprehensions (Section 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 E~ |~ P$ and $\bigcap \nolimits E~ |~ P$ .

Definition

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

Types

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

WD

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