Evaluation Mapping is Injective iff Mappings Separate Points

From ProofWiki
Jump to navigation Jump to search


Let $X$ be a topological space.

Let $\family {Y_i}_{i \mathop \in I}$ be an indexed family of topological spaces for some indexing set $I$.

Let $\family {f_i : X \to Y_i}_{i \mathop \in I}$ be an indexed family of continuous mappings.

Let $\ds Y = \prod_{i \mathop \in I} Y_i$ be the product space of $\family {Y_i}_{i \mathop \in I}$.

Let $f : X \to Y$ be the evaluation mapping induced by $\family{f_i}_{i \mathop \in I}$.


$f$ is an injection if and only if $\family {f_i : X \to Y_i}_{i \mathop \in I}$ separates points


We have:

$f$ is an injection
\(\ds \iff \ \ \) \(\ds \forall x, y \in X : x \ne y : \ \ \) \(\ds \map f x\) \(\ne\) \(\ds \map f y\) Definition of Injection
\(\ds \iff \ \ \) \(\ds \forall x, y \in X : x \ne y : \ \ \) \(\ds \family{ \map {f_i} x }_{i \in I}\) \(\ne\) \(\ds \family{ \map {f_i} y }_{i \in I}\) Definition of Evaluation Mapping
\(\ds \iff \ \ \) \(\ds \forall x, y \in X : x \ne y : \exists i \in I : \ \ \) \(\ds \map {f_i} x\) \(\ne\) \(\ds \map {f_i} y\) Definition of Cartesian Product of Family
\(\ds \iff \ \ \) \(\ds \family {f_i : X \to Y_i}_{i \mathop \in I} \text{ separates points} \ \ \) \(\ds \) \(\) \(\ds \) Definition of Mappings Separating Points