プロダクトセット（集合）のプロダクトサブセット（部分集合）は、プロダクトサブセット（部分集合）たちでそれらの各々はコンポーネントサブセット（部分集合）および他の全体セット（集合）たちを取るものであるものたちのインターセクション（共通集合）であることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、セット（集合）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のプロダクトセット（集合）の任意のプロダクトサブセット（部分集合）は、プロダクトサブセット（部分集合）たちでそれらの各々はあるコンポーネントサブセット（部分集合）および他の全体セット（集合）たちを取るものであるものたちのインターセクション（共通集合）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述1
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(\{S'_j \in \{\text{ 全てのセット（集合）たち }\}: j \in J\}\):
\(\times_{j \in J} S'_j\):
\(\{S_j \subseteq S'_j: j \in J\}\):
\(\times_{j \in J} S_j\): \(\subseteq \times_{j \in J} S'_j\)
//
ステートメント（言明）たち:
\(\times_{j \in J} S_j = \cap_{l \in J} \times_{j \in J} S_{l, j}\)、ここで、\(j = l\)である時は\(S_{l, j} = S_l\)で、その他の場合\(S_{l, j} = S'_j\)
//
\(\times_{j \in J} S_j\)は\(\times_{j \in J} S'_j\)のサブセット（部分集合）であるとみなされている、なぜなら、各\(p \in \times_{j \in J} S_j\)に対して、\(p\)は\(J\)から\(\cup_{j \in J} S_j\)の中への\(p (j) \in S_j\)を満たすあるファンクション（関数）である、それは、\(J\)から\(\cup_{j \in J} S'_j\)の中への\(p (j) \in S'_j\)を満たすファンクション（関数）とみなされている。
2: 証明1
全体戦略: ステップ1: 各\(p \in \times_{j \in J} S_j\)に対して、\(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\)であることを見る; ステップ2: 各\(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\)に対して、\(p \in \times_{j \in J} S_j\)であることを見る。
ステップ1:
\(p \in \times_{j \in J} S_j\)を任意のものとしよう。
各\(l \in J\)に対して、\(p \in \times_{j \in J} S_{l, j}\)、なぜなら、\(j = l\)に対して、\(p (j) \in S_l = S_{l, j}\)、そして、各\(j \neq l\)に対して、\(p (j) \in S'_j = S_{l, j}\)。
したがって、\(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\)。
ステップ2:
\(p \in \cap_{l \in J} \times_{j \in J} S_{l, j}\)を任意のものとしよう。
各\(l \in J\)に対して、\(p \in \times_{j \in J} S_{l, j}\)、各\(j \in J\)に対して、\(p (j) \in S_{l, j}\)、したがって、\(p (l) \in S_{l, l} = S_l\)。
したがって、\(p \in \times_{j \in J} S_j\)。
3: 構造化された記述2
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(\{S'_1, ..., S'_n\}\):
\(S'_1 \times ... \times S'_n\):
\(\{S_1 \subseteq S'_1, ..., S_n \subseteq S'_n\}\):
\(S_1 \times ... \times S_n\): \(\subseteq S'_1 \times ... \times S'_n\)
//
ステートメント（言明）たち:
\(S_1 \times ... \times S_n = \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\)、ここで、\(j = l\)である時は\(S_{l, j} = S_l\)、そうでない時は、\(S_{l, j} = S'_j\)
//
4: 証明2
全体戦略: ステップ1: 各\(p \in S_1 \times ... \times S_n\)に対して、\(p \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\)であることを見る; ステップ2: 各\(p \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\)に対して、\(p \in S_1 \times ... \times S_n\)であることを見る。
ステップ1:
\(p = (p_1, ..., p_n) \in S_1 \times ... \times S_n\)を任意のものとしよう。
各\(l \in \{1, ..., n\}\)に対して、\(p \in S_{l, 1} \times ... \times S_{l, n}\)、なぜなら、\(j = l\)に対して\(p_j \in S_l = S_{l, j}\)、そうでなければ\(p_j \in S'_j = S_{l, j}\)。
したがって、\(p \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\)。
ステップ2:
\(p = (p_1, ..., p_n) \in \cap_{l \in \{1, ..., n\}} S_{l, 1} \times ... \times S_{l, n}\)を任意のものとしよう。
各\(l \in \{1, ..., n\}\)に対して、\(p \in S_{l, 1} \times ... \times S_{l, n}\)、したがって、\(p_l \in S_{l, l} = S_l\)。
したがって、\(p \in S_1 \times ... \times S_n\)。
