Projection is Surjection/Family of Sets

Theorem

Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets.

Let $\displaystyle \prod_{\alpha \mathop \in I} S_\alpha$ be the Cartesian product of $\family {S_\alpha}_{\alpha \mathop \in I}$.

Let each of $S_\alpha$ be non-empty.

For each $\beta \in I$, let $\displaystyle \pr_\beta: \prod_{\alpha \mathop \in I} S_\alpha \to S_\beta$ be the $\beta$th projection on $\displaystyle S = \prod_{\alpha \mathop \in I} S_\alpha$.

Then $\pr_\beta$ is a surjection.

Proof

Consider the $\beta$th projection.

Let $x_\beta \in S_\beta$.

Let $\map x \beta = x_\beta$

Suppose $\gamma \in I: \gamma \ne \beta$.

As $S_\gamma \ne \O$ it is possible to use the axiom of choice to choose $\map x \gamma \in S_\gamma$.

Then:

$\displaystyle x \in \prod_{\alpha \mathop \in I} S_\alpha$

and:

$\map {\pr_\beta} x = \map x \beta$

Hence the result.

$\blacksquare$
{"ft_lang_label":"__label__en","ft_lang_prob":0.5959492,"math_prob":0.9999695,"size":1084,"snap":"2019-43-2019-47","text_gpt3_token_len":354,"char_repetition_ratio":0.1712963,"word_repetition_ratio":0.012269938,"special_character_ratio":0.33856088,"punctuation_ratio":0.13023256,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":1.0000092,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-14T01:31:17Z\",\"WARC-Record-ID\":\"<urn:uuid:ffbf5d83-ffac-4204-ad74-50bc4a73d5ac>\",\"Content-Length\":\"31703\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:6d4294d5-ab88-48d9-8830-17adf67336d4>\",\"WARC-Concurrent-To\":\"<urn:uuid:15f225c1-f839-4ce6-b46f-66184f379990>\",\"WARC-IP-Address\":\"104.27.169.113\",\"WARC-Target-URI\":\"https://proofwiki.org/wiki/Projection_is_Surjection/Family_of_Sets\",\"WARC-Payload-Digest\":\"sha1:DAEVDMLBQ66ZB5JD3WAIDXLTH2QOCYXT\",\"WARC-Block-Digest\":\"sha1:RE5IBQGMNLEWSTQ5WNLNYXLRVQLQQCDL\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570986648481.7_warc_CC-MAIN-20191014003258-20191014030258-00242.warc.gz\"}"}