Rodin Handbook





 
Previous: Sets Up: Mathematical Notation Next: Arithmetic User Manual for Rodin v.2.3

Feedback

3.3.5 Relations

3.3.5.1 Pairs and Cartesian product

$\mapsto $

|->

Pair

$\mathbin \times $

**

Cartesian product

Description

$x\mapsto y$ denotes the pair whose first element is $x$ and second element is $y$.

$S\mathbin \times T$ denotes the set of pairs where the first element is a member of $S$ and second element is a member of $T$.

Definition

$S\mathbin \times T = \{ ~ x\mapsto y~ |~ x\in S\land y\in Y~ \} $

Types

$x\mapsto y\in \alpha \mathbin \times \beta $ with $x\in \alpha $ and $y\in \beta $.
$S\mathbin \times T\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $T\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$.

WD

$\mathcal{L}(x\mapsto y)\mathrel {\widehat=}\mathcal{L}(x)\land \mathcal{L}(y)$
$\mathcal{L}(S\mathbin \times T)\mathrel {\widehat=}\mathcal{L}(S)\land \mathcal{L}(T)$

3.3.5.2 Relations

$\mathbin \leftrightarrow $

<->

Relations

$\mathbin {\leftarrow \mkern -14mu\leftrightarrow }$

<<->

Total relations

$\mathbin {\leftrightarrow \mkern -14mu\rightarrow }$

<->>

Surjective relations

$\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }$

<<->>

Total surjective relations

Description

$S\mathbin \leftrightarrow T$ is the set of relations between the two sets $S$ and $T$. A relation consists of pairs where the first element is of $S$ and the second of $T$. $S\mathbin \leftrightarrow T$ is just an abreviation for $\mathop {\mathbb P\hbox{}}\nolimits (S\mathbin \leftrightarrow T)$.

A total relation is a relation which relates each element of $S$ to at least one element of $T$.

A surjective relation is a relation where there is at least one element of $S$ for each element of $T$ such that both are related.

Definition

$S \mathbin \leftrightarrow T = \mathop {\mathbb P\hbox{}}\nolimits (S\mathbin \times T)$
$S \mathbin {\leftarrow \mkern -14mu\leftrightarrow }T = \{ ~ r~ |~ r\in S\mathbin \leftrightarrow T\land \mathop {\mathrm{dom}}\nolimits (r) = S~ \} $
$S \mathbin {\leftrightarrow \mkern -14mu\rightarrow }T = \{ ~ r~ |~ r\in S\mathbin \leftrightarrow T\land \mathop {\mathrm{ran}}\nolimits (r) = S~ \} $
$S \mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }T = (S \mathbin {\leftarrow \mkern -14mu\leftrightarrow }T) \land (S \mathbin {\leftrightarrow \mkern -14mu\rightarrow }T)$

Types

For $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $T\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ and for each operator $\mathbin {\Box }$ of $\mathbin \leftrightarrow $, $\mathbin {\leftarrow \mkern -14mu\leftrightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\rightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }$:
$S \mathbin {\Box }T\in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta ))$

WD

$\mathcal{L}(S\mathbin {\Box }T) \mathrel {\widehat=}\mathcal{L}(S) \land \mathcal{L}(T)$ for each operator $\mathbin {\Box }$ of $\mathbin \leftrightarrow $, $\mathbin {\leftarrow \mkern -14mu\leftrightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\rightarrow }$, $\mathbin {\leftrightarrow \mkern -14mu\leftrightarrow }$.

3.3.5.3 Domain and Range

$\mathop {\mathrm{dom}}\nolimits $

dom

Domain

$\mathop {\mathrm{ran}}\nolimits $

ran

Range

Description

If $r$ is a relation between the sets $S$ and $T$, the domain $\mathop {\mathrm{dom}}\nolimits (r)$ is the set of elements of $S$ that are related to at least one element of $T$ by $r$.

Likewise the range $\mathop {\mathrm{ran}}\nolimits (r)$ is the set of elements of $T$ where at least one element of $S$ relates to by $r$.

Definition

$\mathop {\mathrm{dom}}\nolimits (r) = \{ ~ x~ |~ \exists y \mathord {\mkern 1mu\cdot \mkern 1mu}x\mapsto y\in r~ \} $
$\mathop {\mathrm{ran}}\nolimits (r) = \{ ~ y~ |~ \exists x \mathord {\mkern 1mu\cdot \mkern 1mu}x\mapsto y\in r~ \} $

Types

$\mathop {\mathrm{dom}}\nolimits (r)\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$ and $\mathop {\mathrm{ran}}\nolimits (r)\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$.

WD

$\mathcal{L}(\mathop {\mathrm{dom}}\nolimits (r)) \mathrel {\widehat=}\mathcal{L}(r)$
$\mathcal{L}(\mathop {\mathrm{ran}}\nolimits (r)) \mathrel {\widehat=}\mathcal{L}(r)$

3.3.5.4 Domain and Range Restrictions

$\mathbin \lhd $

<|

Domain restriction

$\mathbin {\lhd \mkern -14mu-}$

<<|

Domain subtraction

$\mathbin \lhd $

|>

Range restriction

$\mathbin {\lhd \mkern -14mu-}$

|>>

Range subtraction

Description

The domain restriction $S\mathbin \lhd r$ is a subset of the relation $r$ that contains all pairs whose first element is in $S$. $S\mathbin {\lhd \mkern -14mu-}r$ is the subset where the pair’s first element is not in $S$.

Analogously the range restriction $r\mathbin \rhd S$ is a subset that contains all pairs whose second element is in $S$ and $r\mathbin {\rhd \mkern -14mu-}S$ is the set where the pair’s second element is not in $S$.

Definition

$s\mathbin \lhd r = \{ ~ x\mapsto y~ |~ x\mapsto y\in r \land x\in s\} $
$s\mathbin {\lhd \mkern -14mu-}r = \{ ~ x\mapsto y~ |~ x\mapsto y\in r \land x\not\in s\} $
$r\mathbin \rhd s = \{ ~ x\mapsto y~ |~ x\mapsto y\in r \land y\in s\} $
$r\mathbin {\rhd \mkern -14mu-}s = \{ ~ x\mapsto y~ |~ x\mapsto y\in r \land y\not\in s\} $

Types

$s\mathbin \lhd r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\mathbin {\lhd \mkern -14mu-}r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$
$r\mathbin \rhd s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $r\mathbin {\rhd \mkern -14mu-}s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$

WD

$\mathcal{L}(s\mathbin {\Box }r)\mathrel {\widehat=}\mathcal{L}(s)\land \mathcal{L}(r)$ for each operator $\mathbin {\Box }$ of $\mathbin \lhd $, $\mathbin {\lhd \mkern -14mu-}$, $\mathbin \rhd $, $\mathbin {\rhd \mkern -14mu-}$

3.3.5.5 Operations on relations

$\mathbin ;$

;

Relational forward composition

$\circ $

circ

Relational backward composition

$\mathbin {\lhd \mkern -9mu-}$

<+

Relational override

$\mathbin \| $

||

Parallel product

$\mathbin \otimes $

><

Direct product

$\mbox{}^{-1}$

~

Inverse

Description

An element $x$ is related by $r\mathbin ;S$ to an element $y$ if there is an element $z$ such that $R$ relates $x$ to $z$ and $S$ relates $z$ to $y$.

$s\circ r$ can be written as an alternative to $r\mathbin ;s$. This reflects the fact that for two functions $f$ and $g$ holds $f(g(x)) = (f\circ g)(x)$.

The relational overwrite $r\mathbin {\lhd \mkern -9mu-}s$ is equal to $r$ except all entries in $r$ whose first element is in the domain of $s$ are replaced by the corresponding entries in $s$.

If a relation $r$ relates an element $x$ to $z$ and $s$ relates $x$ to $z$, the parallel product $r\mathbin \| s$ relates $x$ to the pair $y\mapsto z$.

The direct product $r\mathbin \otimes s$ relates a pair $x\mapsto y$ to a pair $m\mapsto n$ when $r$ relates $x$ to $m$ and $s$ relates $y$ to $n$.

The inverse relation $r^{-1}$ relates an element $x$ to $y$ if the original relation $r$ relates $y$ to $x$.

Definition

$r\mathbin ;s = \{ ~ x \mapsto y~ |~ \exists z\mathord {\mkern 1mu\cdot \mkern 1mu}x \mapsto z \in r \land z \mapsto y \in s~ \} $
$r\circ s = s\mathbin ;r$
$r\mathbin {\lhd \mkern -9mu-}s = s\mathbin {\mkern 1mu\cup \mkern 1mu}(dom(s)\mathbin {\lhd \mkern -14mu-}r)$
$r\mathbin \| s = \{ ~ x\mapsto (y\mapsto z)~ |~ x\mapsto y\in r \land x\mapsto z\in s ~ \} $
$r\mathbin \otimes s = \{ ~ (x\mapsto y)\mapsto (m\mapsto n)~ |~ x\mapsto m\in r \land y\mapsto n\in s ~ \} $
$r^{-1} = \{ y\mapsto x~ |~ x\mapsto y\in r~ \} $

Types

$r\mathbin ;s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \gamma )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\in \mathop {\mathbb P\hbox{}}\nolimits (\beta \mathbin \times \gamma )$
$r\circ s\in \mathop {\mathbb P\hbox{}}\nolimits (\gamma \mathbin \times \alpha )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\in \mathop {\mathbb P\hbox{}}\nolimits (\beta \mathbin \times \gamma )$
$r\mathbin {\lhd \mkern -9mu-}s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$
$r\mathbin \| s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times (\beta \mathbin \times \gamma ))$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \gamma )$
$r\mathbin \otimes s\in \mathop {\mathbb P\hbox{}}\nolimits (~ (\alpha \mathbin \times \gamma )\mathbin \times (\beta \mathbin \times \delta )~ )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $s\in \mathop {\mathbb P\hbox{}}\nolimits (\gamma \mathbin \times \delta )$
$r^{-1}\in \mathop {\mathbb P\hbox{}}\nolimits (\beta \mathbin \times \alpha )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$

WD

$\mathcal{L}(r\mathbin {\Box }s)\mathrel {\widehat=}\mathcal{L}(r)\land \mathcal{L}(s)$ for each operator $\mathbin {\Box }$ of $\mathbin ;$, $\circ $, $\mathbin {\lhd \mkern -9mu-}$, $\mathbin \| $, $\mathbin \otimes $
$\mathcal{L}(r^{-1})\mathrel {\widehat=}\mathcal{L}(r)$

3.3.5.6 Relational image

$[\ldots ]$

[…]

Relational image

Description

The relational image $r[S]$ are those elements in the range of $r$ that are mapped from $S$.

Definition

$r[S] = \{ ~ x,y~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\in S\land x\mapsto y\in r~ |~ y~ \} $

Types

$r[S]\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ with $r\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$

WD

$\mathcal{L}(r[S])\mathrel {\widehat=}\mathcal{L}(r)\land \mathcal{L}(S)$

3.3.5.7 Constant relations

$\mathop {\mathrm{id}}\nolimits $

id

Identity relation

$\mathop {\mathrm{prj}_1}\nolimits $

prj1

First projection

$\mathop {\mathrm{prj}_2}\nolimits $

prj2

Second projection

Description

$\mathop {\mathrm{id}}\nolimits $ is the identity relation that maps every element to itself.

$\mathop {\mathrm{prj}_1}\nolimits $ is a function that maps a pair to its first element. Likewise $\mathop {\mathrm{prj}_2}\nolimits $ maps a pair to its second element.

$\mathop {\mathrm{id}}\nolimits $, $\mathop {\mathrm{prj}_1}\nolimits $ and $\mathop {\mathrm{prj}_2}\nolimits $ are generic definitions. Their type must be infered from the environment.

Definition

$\mathop {\mathrm{id}}\nolimits = \{ ~ x\mapsto x~ |~ \mathord {\top }~ \} $
$\mathop {\mathrm{prj}_1}\nolimits = \{ ~ (x\mapsto y)\mapsto x~ |~ \mathord {\top }~ \} $
$\mathop {\mathrm{prj}_2}\nolimits = \{ ~ (x\mapsto y)\mapsto y~ |~ \mathord {\top }~ \} $

Types

$\mathop {\mathrm{id}}\nolimits \in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \alpha )$ for an arbitrary type $\alpha $.
$\mathop {\mathrm{prj}_1}\nolimits \in \mathop {\mathbb P\hbox{}}\nolimits ((\alpha \mathbin \times \beta )\mathbin \times \alpha )$ and $\mathop {\mathrm{prj}_1}\nolimits \in \mathop {\mathbb P\hbox{}}\nolimits ((\alpha \mathbin \times \beta )\mathbin \times \beta )$ for arbitrary types $\alpha $ and $\beta $.

WD

$\mathcal{L}(\mathop {\mathrm{id}}\nolimits )\mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\mathop {\mathrm{prj}_1}\nolimits )\mathrel {\widehat=}\mathord {\top }$
$\mathcal{L}(\mathop {\mathrm{prj}_2}\nolimits )\mathrel {\widehat=}\mathord {\top }$

Example

The assumption that a relation $r$ is irreflexive can be expressed by:
$r\mathbin {\mkern 1mu\cap \mkern 1mu}\mathop {\mathrm{id}}\nolimits =\emptyset $

3.3.5.8 Sets of functions

$ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $

+->

Partial functions

$\mathbin \rightarrow $

–>

Total functions

$ \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } $

>+>

Partial injections

$\mathbin \rightarrowtail $

>->

Total injections

$ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } $

+->>

Partial surjections

$\mathbin \twoheadrightarrow $

–>>

Total surjections

$\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } $

>->>

Bijections

Description

A partial function from $S$ to $T$ is a relation that maps an element of $S$ to at most one element of $T$. A function is total if its domain contains all elements of $S$, i.e. it maps every element of $S$ to an element of $T$.

A function is injective (is an injection) if two distinct elements of $S$ are always mapped to distinct elements of $T$. It is also equivalent to say that the inverse of an injective function is a also a function.

A function is surjective (is a surjection) if for every element of $T$ there exists an element in $S$ that is mapped to it.

A function is bijective (is a bijection) if it is both injective and surjective.

Definition

$S \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } T = \{ ~ f ~ |~ f\in S\mathbin \leftrightarrow T \land (\forall e,x,y \mathord {\mkern 1mu\cdot \mkern 1mu}e\mapsto x\in f \land e\mapsto y\in f \mathbin \Rightarrow x=y) ~ \} $
$S \mathbin \rightarrow T = \{ ~ f ~ |~ f\in S \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } T \land \mathop {\mathrm{dom}}\nolimits (f) = S ~ \} $
$S \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } T = \{ ~ f ~ |~ f\in S \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } T \land f^{-1} \in T \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } S ~ \} $
$S \mathbin \rightarrowtail T = (S \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } T) \mathbin {\mkern 1mu\cap \mkern 1mu}(S\mathbin \rightarrow T)$
$S \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } T = \{ ~ f ~ |~ f\in S \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } T \land \mathop {\mathrm{ran}}\nolimits (f) = T ~ \} $
$S \mathbin \twoheadrightarrow T = (S \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } T) \mathbin {\mkern 1mu\cap \mkern 1mu}(S\mathbin \rightarrow T)$
$S \mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } T = (S\mathbin \rightarrowtail T) \mathbin {\mkern 1mu\cap \mkern 1mu}(S\mathbin \twoheadrightarrow T)$

Types

With $S\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$, $T\in \mathop {\mathbb P\hbox{}}\nolimits (\beta )$ and for each operator $\mathbin {\Box }$ of $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $, $\mathbin \rightarrow $, $ \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } $, $\mathbin \rightarrowtail $, $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } $, $\mathbin \twoheadrightarrow $, $\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } $:
$S \mathbin {\Box }T \in \mathop {\mathbb P\hbox{}}\nolimits (\mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta ))$

WD

For each operator $\mathbin {\Box }$ of $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } $, $\mathbin \rightarrow $, $ \mathbin {\mkern 9mu\mapstochar \mkern -9mu\rightarrowtail } $, $\mathbin \rightarrowtail $, $ \mathbin {\mkern 6mu\mapstochar \mkern -6mu\twoheadrightarrow } $, $\mathbin \twoheadrightarrow $, $\mathbin { \rightarrowtail \mkern -18mu\twoheadrightarrow } $:
$\mathcal{L}(S\mathbin {\Box }T) \mathrel {\widehat=}\mathcal{L}(S) \land \mathcal{L}(T)$

3.3.5.9 Function application

$(\ldots )$

(…)

Function application

Description

The function application $f(x)$ yields the value for $x$ of the function $f$. It is only defined if $x$ is in the domain of $f$ and if $f$ is a actually a function.

Definition

$f(x) = y \mathrel {\widehat=}x \mapsto y\in f$

Types

$f(x)\in \beta $ with $f\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ and $x\in \alpha $

WD

$\mathcal{L}(f(x))\mathrel {\widehat=}\mathcal{L}(f)\land \mathcal{L}(x)\land f\in \alpha \mathbin {\mkern 6mu\mapstochar \mkern -6mu\rightarrow } \beta \land x\in \mathop {\mathrm{dom}}\nolimits (f)$ with $\mathop {\mathbb P\hbox{}}\nolimits (\alpha \mathbin \times \beta )$ being the type of $f$.

3.3.5.10 Lambda

$\lambda $

%

Lambda

Description

$(\lambda ~ \mathcal{P}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ |~ E~ )$ is a function that maps an “input” $\mathcal{P}$ to a result $E$ such that $P$ holds.

$\mathcal{P}$ is a pattern of identifiers, parentheses and $\mapsto $ which follows the following rules:

  • An identifier $x$ is a pattern.

  • An identifier $x$, followed by an $\mathbin {\raisebox{0.6ex}{\ensuremath{\circ }}\mkern -9mu\raisebox{-0.6ex}{\ensuremath{\circ }}}$ operator is a pattern (See 3.3.7 for more details).

  • A pair $p\mapsto q$ is a pattern when $p$ and $q$ are patterns.

  • $(p)$ is pattern when $p$ is pattern.

In the simplest case, $\mathcal{P}$ is just an identifier.

Definition

$(\lambda ~ \mathcal{P}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ |~ E~ ) = \{ ~ \mathcal{P}\mapsto E~ |~ P~ \} $

Types

$(\lambda ~ \mathcal{P}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ |~ E~ )\in \mathop {\mathbb P\hbox{}}\nolimits (~ \alpha \mathbin \times \beta ~ )$ with $\mathcal{P}\in \alpha $, $P$ being a predicate and $E\in \beta $.

WD

$\mathcal{L}(\lambda ~ \mathcal{P}~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ P~ |~ E~ )~ \mathrel {\widehat=}~ \forall \textsl{Free}(\mathcal{P})~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ \mathcal{L}(P)\land (P\mathbin \Rightarrow \mathcal{L}(E))$

Example

A function $double$ that returns the double value of a natural number:
$double = (\lambda x~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ x\in \mathord {\mathbb N}~ |~ 2\cdot x)$

The dot product of two 2-dimensional vectors can be defined by:
$dotp = (\lambda ~ (a \mapsto b)\mapsto (c \mapsto d)~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ a\in \mathord {\mathbb Z}\land b\in \mathord {\mathbb Z}\land c\in \mathord {\mathbb Z}\land d\in \mathord {\mathbb Z}~ |~ a\cdot c+b\cdot d~ )$

Previous: Sets Up: Mathematical Notation Next: Arithmetic  
User Manual for Rodin v.2.3 : Reference : Mathematical Notation : Relations