プロダクトセット（集合）に対して、プロダクトサブセット（部分集合）でそのコンポーネントたちの一つがサブセット（部分集合）たちのユニオン（和集合）であるものは、プロダクトサブセット（部分集合）たちでそれらの対応するコンポーネントたちがサブセット（部分集合）たちであるものたちのユニオン（和集合）であることの記述/集合
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、プロダクトセット（集合）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のプロダクトセット（集合）に対して、任意のプロダクトサブセット（部分集合）でそのコンポーネントたちの一つが任意のサブセット（部分集合）たちのユニオン（和集合）であるものは、プロダクトサブセット（部分集合）たちでそれらの対応するコンポーネントたちが当該サブセット（部分集合）たちであるものたちのユニオン（和集合）であるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述1
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J_1\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(J_2\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(\{S_j \in \{\text{ 全てのセット（集合）たち }\} \vert j \in J_1 \setminus \{l\}\}\):
\(\{S_{l, m} \in \{\text{ 全てのセット（集合）たち }\} \vert m \in J_2\}\):
\(\{S'_j \in \{\text{ 全てのセット（集合）たち }\} \vert j \in J_1 \land (\forall j \in J_1 \setminus \{l\} (S'_j = S_j); S'_l = \cup_{m \in J_2} S_{l, m})\}\):
\(\{S'_{m, j} \in \{\text{ 全てのセット（集合）たち }\} \vert m \in J_2, j \in J_1 \land (\forall j \in J_1 \setminus \{l\} (S'_{m, j} = S_j); S'_{m, l} = S_{l, m})\}\):
\(\times_{j \in J_1} S'_j\):
\(\cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\):
//
ステートメント（言明）たち:
\(\times_{j \in J_1} S'_j = \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\)
//
2: 証明1
全体戦略: ステップ1: \(\times_{j \in J_1} S'_j \subseteq \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\)であることを見る; ステップ2: \(\cup_{m \in J_2} \times_{j \in J_1} S'_{m, j} \subseteq \times_{j \in J_1} S'_j\)であることを見る; ステップ3: 本命題を結論する。
ステップ1:
\(f \in \times_{j \in J_1} S'_j\)を任意のものとしよう。
各\(j \in J_1\)に対して、\(f (j) \in S'_j\)。
各\(j \in J_1 \setminus \{l\}\)に対して、\(S'_j = S'_{m, j}\)、各\(m \in J_2\)に対して。
\(f (l) \in S'_l = \cup_{m \in J_2} S_{l, m}\)。
したがって、\(f (l) \in S_{l, m} = S'_{m, l}\)、ある\(m \in J_2\)に対して。
したがって、その\(m\)に対して、\(f \in \times_{j \in J_1} S'_{m, j}\)。
したがって、\(f \in \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\)。
ステップ2:
\(f \in \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\)を任意のものとしよう。
\(f \in \times_{j \in J_1} S'_{m, j}\)、ある\(m \in J_2\)に対して。
その\(m\)に対して、各\(j \in J_1\)に対して、\(f (j) \in S'_{m, j}\)、しかし、各\(j \in J_1 \setminus \{l\}\)に対して、\(S'_{m, j} = S_j = S'_j\)、そして、\(S'_{m, l} = S_{l, m} \subseteq \cup_{m' \in J_2} S_{l, m'} = S'_l\)。
したがって、\(f \in \times_{j \in J_1} S'_j\)。
ステップ3:
したがって、\(\times_{j \in J_1} S'_j = \cup_{m \in J_2} \times_{j \in J_1} S'_{m, j}\)。
3: 構造化された記述2
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J_2\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(\{S_1, ..., S_{l - 1}, \widehat{S_l}, S_{l + 1}, ..., S_n\}\): \(S_j \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S_{l, m} \in \{\text{ 全てのセット（集合）たち }\} \vert m \in J_2\}\):
\(\{S'_1, ..., S'_n\}\): \(\forall j \in \{1, ..., n\} \setminus \{l\} (S'_j = S_j); S'_l = \cup_{m \in J_2} S_{l, m}\)
\(\{S'_{m, 1}, ..., S'_{m, n} \vert m \in J_2\}\): \(\forall j \in \{1, ..., n\} \setminus \{l\} (S'_{m, j} = S_j); S'_{m, l} = S_{l, m}\)
\(S'_1 \times ... \times S'_n\):
\(\cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\):
//
ステートメント（言明）たち:
\(S'_1 \times ... \times S'_n = \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\)
//
4: 証明2
全体戦略: ステップ1: \(S'_1 \times ... \times S'_n \subseteq \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\)であることを見る; ステップ2: \(\cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n} \subseteq S'_1 \times ... \times S'_n\)であることを見る; ステップ3: 本命題を結論する。
ステップ1:
\(p = (p^1, ..., p^n) \in S'_1 \times ... \times S'_n\)を任意のものとしよう。
各\(j \in \{1, ..., n\}\)に対して、\(p^j \in S'_j\)。
各\(j \in \{1, ..., n\} \setminus \{l\}\)に対して、\(S'_j = S'_{m, j}\)、各\(m \in J_2\)に対して。
\(p^l \in S'_l = \cup_{m \in J_2} S_{l, m}\)。
したがって、\(p^l \in S_{l, m} = S'_{m, l}\)、ある\(m \in J_2\)に対して。
したがって、その\(m\)に対して、\(p \in S'_{m, 1} \times ... \times S'_{m, n}\)。
したがって、\(p \in \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\)。
ステップ2:
\(p \in \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\)を任意のものとしよう。
\(p \in S'_{m, 1} \times ... \times S'_{m, n}\)、ある\(m \in J_2\)に対して。
その\(m\)に対して、各\(j \in \{1, ..., n\}\)に対して、\(p^j \in S'_{m, j}\)、しかし、各\(j \in \{1, ..., n\} \setminus \{l\}\)に対して、\(S'_{m, j} = S_j = S'_j\)、そして、\(S'_{m, l} = S_{l, m} \subseteq \cup_{m' \in J_2} S_{l, m'} = S'_l\)。
したがって、\(p \in S'_1 \times ... \times S'_n\)。
ステップ3:
したがって、\(S'_1 \times ... \times S'_n = \cup_{m \in J_2} S'_{m, 1} \times ... \times S'_{m, n}\)。
