Restriction of Mapping is its Intersection with Cartesian Product of Subset with Image

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $f: S \to T$ be a mapping.

Let $X \subseteq S$.

Let $f {\restriction_X}$ be the restriction of $f$ to $X$.


Then:

$f {\restriction_X} = f \cap \paren {X \times \Img f}$

where:

$\Img f$ denotes the image of $f$, defined as:
$\Img f = \set {t \in T: \exists s \in S: t = \map f s}$
$X \times \Img f$ denotes the cartesian product of $X$ with $\Img f$.


Proof

We have:

\(\ds \tuple {x, y}\) \(\in\) \(\ds f {\restriction_X}\)
\(\ds \leadsto \ \ \) \(\ds \tuple {x, y}\) \(\in\) \(\ds f\) Definition of Restriction of Mapping
\(\, \ds \land \, \) \(\ds x\) \(\in\) \(\ds X\) Definition of $x$
\(\, \ds \land \, \) \(\ds y\) \(\in\) \(\ds \Img f\) Definition of Mapping
\(\ds \leadsto \ \ \) \(\ds \tuple {x, y}\) \(\in\) \(\ds f\) Definition of Restriction of Mapping
\(\, \ds \land \, \) \(\ds \tuple {x, y}\) \(\in\) \(\ds X \times \Img f\) Definition of Cartesian Product
\(\ds \leadsto \ \ \) \(\ds \tuple {x, y}\) \(\in\) \(\ds f \cap \paren {X \times \Img f}\) Definition of Set Intersection
\(\ds \leadsto \ \ \) \(\ds f {\restriction_X}\) \(\subseteq\) \(\ds f \cap \paren {X \times \Img f}\) Definition of Subset

$\Box$


Then:

\(\ds \tuple {x, y}\) \(\in\) \(\ds f \cap \paren {X \times \Img f}\)
\(\ds \leadsto \ \ \) \(\ds \tuple {x, y}\) \(\in\) \(\ds f\)
\(\, \ds \land \, \) \(\ds \tuple {x, y}\) \(\in\) \(\ds X \times \Img f\) Definition of Set Intersection
\(\ds \leadsto \ \ \) \(\ds \tuple {x, y}\) \(\in\) \(\ds f\)
\(\, \ds \land \, \) \(\ds x\) \(\in\) \(\ds X\) Definition of Cartesian Product
\(\, \ds \land \, \) \(\ds y\) \(\in\) \(\ds f \sqbrk X\) Definition of Image of Subset under Mapping
\(\ds \leadsto \ \ \) \(\ds \tuple {x, y}\) \(\in\) \(\ds f\)
\(\, \ds \land \, \) \(\ds \tuple {x, y}\) \(\in\) \(\ds f {\restriction_X}\) Definition of Restriction of Mapping
\(\ds \leadsto \ \ \) \(\ds f \cap \paren {X \times \Img f}\) \(\subseteq\) \(\ds f {\restriction_X}\) Definition of Subset

$\Box$


Thus we have:

\(\ds f {\restriction_X}\) \(\subseteq\) \(\ds f \cap \paren {X \times \Img f}\) Definition of Subset
\(\, \ds \land \, \) \(\ds f \cap \paren {X \times \Img f}\) \(\subseteq\) \(\ds f {\restriction_X}\) Definition of Subset
\(\ds \leadsto \ \ \) \(\ds f \cap \paren {X \times \Img f}\) \(=\) \(\ds f {\restriction_X}\) Definition of Set Equality

$\blacksquare$


Sources