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