セット（集合）の各要素をセット（集合）の中にユニークにマップするフォーミュラはファンクション（関数）を構成することの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、セット（集合）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のセット（集合）の各要素を別のセット（集合）の中へユニークにマップする任意のフォーミュラはファンクション（関数）を構成するという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義の一覧があります。
本サイトにてこれまで議論された命題の一覧があります。
本体
1: 注
本命題は明らかに思えるかもしれないが、その動機は、当該マップ（写像）は、ファンクション（関数）と呼ばれるにはセット（関数）であると証明されなければならない、ZFCセット（集合）理論においては、ということ。当該プロダクトセット（集合）の一部であることは十分ではない、なぜなら、サブセット（部分集合）公理は正当なフォーミュラを要求するから。したがって、フォーミュラが求められる: 各要素がイメージ（像）になんらかの形でユニークにマップすると知っているというだけでは十分ではない。
2: 記述
任意のセット（集合）たち\(S_1, S_2\)および以下を満たす任意のフォーミュラ\(\phi (s_1, s_2, . . .)\)、ここで、\(s_1 \in S_1\)および\(s_2 \in S_2\)、つまり、それは\(S_1\)の各要素を\(S_2\)のある要素へユニークにマップする、に対して、\(f: S_1 \rightarrow S_2, s_1 \mapsto s_2 \text{ if and only if } \phi (s_1, s_2, . . .)\)はファンクション（関数）である。
3: 証明
\(f \subseteq S_1 \times S_2\)、しかし、\(f\)をサブセット（部分集合）公理によってセット（集合）であると断定するには、正当なフォーミュラが必要である。\(f = \{p \in S_1 \times S_2\vert \exists s_1 \in S_1, \exists s_2 \in S_2, \phi (s_1, s_2, . . .), p = \langle s_1, s_2 \rangle\}\)。各\(s_1 \in S_1\)に対して、ユニークな要素\(p = \langle s_1, s_2 \rangle \in f\)がある、\(\phi\)に対する仮定によって。したがって、\(f\)はファンクション（関数）である。
