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:

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

$\Box$


Then:

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

$\Box$


Thus we have:

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

$\blacksquare$


Sources