Equivalence of Definitions of Inverse Image Mapping of Relation

From ProofWiki
Jump to navigation Jump to search

Theorem

The following definitions of the concept of Inverse Image Mapping of Relation are equivalent:

Definition 1

The inverse image mapping of $\mathcal R$ is the mapping $\mathcal R^\gets: \powerset T \to \powerset S$ that sends a subset $Y \subseteq T$ to its preimage $\map {\mathcal R^{-1} } Y$ under $\mathcal R$:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \begin {cases} \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} } & : \Img {\mathcal R} \cap Y \ne \O \\ \O & : \Img {\mathcal R} \cap Y = \O \end {cases}$

Definition 2

The inverse image mapping of $\mathcal R$ is the direct image mapping of the inverse $\mathcal R^{-1}$ of $\mathcal R$:

$\mathcal R^\gets = \paren {\mathcal R^{-1} }^\to: \powerset T \to \powerset S$

That is:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} }$


Proof

Consider the mapping defined as:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} }$

Let $\Img {\mathcal R} \cap Y = \O$.

Then:

$\forall t \in T: \neg \exists t \in \Img {\mathcal R} \cap Y$

and so:

$\set {s \in S: \exists t \in Y: \tuple {s, t} \in \mathcal R} = \O$

and so:

$\forall Y \in \powerset T: \map {\mathcal R^\gets} Y = \begin {cases} \set {s \in S: \exists t \in Y: \tuple {t, s} \in \mathcal R^{-1} } & : \Img f \cap Y \ne \O \\ \O & : \Img f \cap Y = \O \end {cases}$

$\blacksquare$