パーシャリーオーダードリング（半順序環）、ファイナイト（有限）数のサブセット（部分集合）たちで同一インデックスセット（集合）を持つもの、サブセット（部分集合）たちの合計としてのサブセット（部分集合）で同じインデックスセット（集合）を持つものに対して、サブセット（部分集合）のサプリマム（上限）はサブセット（部分集合）たちのサプリマム（上限）たちの合計に等しいかそれより小さく、サブセット（部分集合）のインフィマム（下限）はサブセット（部分集合）たちのインフィマム（下限）たちの合計に等しいかそれより大きいことの記述/証明
話題
About: リング（環）
この記事の目次
開始コンテキスト
- 読者は、パーシャリーオーダードリング（半順序環）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のサプリマム（上限）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のインフィマム（下限）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のパーシャリーオーダードリング（半順序環）、任意のファイナイト（有限）数のサブセット（部分集合）たちで任意の同一インデックスセット（集合）を持つものたち、当該サブセット（部分集合）たちの合計としてのサブセット（部分集合）で同じインデックスセット（集合）を持つものに対して、もしも、当該サブセット（部分集合）たちのサプリマム（上限）たちが存在する場合、当該サブセット（部分集合）たちのサプリマム（上限）たちの合計は当該サブセット（部分集合）のあるアッパーバウンド（上限）であり、もしも、その上に当該サブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）たちのサプリマム（上限）たちの合計に等しいかそれより小さく、もしも、当該サブセット（部分集合）たちのインフィマム（下限）たちが存在する場合、当該サブセット（部分集合）たちのインフィマム（下限）たちの合計は当該サブセット（部分集合）のあるローワーバウンド（下限）であり、もしも、その上に当該サブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）たちのインフィマム（下限）たちの合計に等しいかそれより大きいという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(R\): \(\in \{\text{ 全てのパーシャリーオーダードリング（半順序環）たち }\}\)で、任意のパーシャルオーダリング（半順序）\(\lt\)を持つもの
\(J\): \(\in \{\text{ 全ての非空インデックスセット（集合）たち }\}\)
\(J'\): \(\in \{\text{ 全ての非空ファイナイト（有限）インデックスセット（集合）たち }\}\)
\(\{S_{j'} = \{s_{j', j} \in R \vert j \in J\} \vert j' \in J'\}\):
\(S\): \(= \{\sum_{j' \in J'} s_{j', j} \vert j \in J\}\)
//
ステートメント（言明）たち:
(
(
\(\forall j' \in J' (\exists Sup (S_{j'}))\)
\(\implies\)
\(\sum_{j' \in J'} Sup (S_{j'}) \in Ub (S)\)
)
\(\land\)
(
\(\forall j' \in J' (\exists Sup (S_{j'})) \land \exists Sup (S)\)
\(\implies\)
\(Sup (S) \le \sum_{j' \in J'} Sup (S_{j'})\)
)
)
\(\land\)
(
(
\(\forall j' \in J' (\exists Inf (S_{j'}))\)
\(\implies\)
\(\sum_{j' \in J'} Inf (S_{j'}) \in Lb (S)\)
)
\(\land\)
(
\(\forall j' \in J' (\exists Inf (S_{j'})) \land \exists Inf (S)\)
\(\implies\)
\(\sum_{j' \in J'} Inf (S_{j'}) \le Inf (S)\)
)
)
//
2: 注
\(Sup (S_{j'})\)や\(Inf (S_{j'})\)は存在しないかもしれない。
\(Sup (S_{j'})\)たちの存在たちや\(Inf (S_{j'})\)たちの存在たちは、\(Sup (S)\)の存在や\(Inf (S)\)の存在を保証しない: 例えば、\(R = \mathbb{Q}\)、\(S_1 = \{q \in \mathbb{Q} \vert q \lt \sqrt{2}\} \cup \{2, 0\}\)、\(S_2 = \{q \in \mathbb{Q} \vert q \lt \sqrt{2}\} \cup \{0, 2\}\)、\(S = \{2 q \in \mathbb{Q} \vert q \lt \sqrt{2}\} \cup \{2 + 0, 0 + 2\}\)、すると、\(Sup (S_1) = 2\)および \(Sup (S_2) = 2\)、しかし、\(Sup (S)\)は存在しない、なぜなら、\(2 \lt 2 \sqrt{2}\)および\(Ub (S) = \{q \in \mathbb{Q} \vert 2 \sqrt{2} \lt q\}\)、それはミニマム（最小値）を持たない。
3: 証明
全体戦略: ステップ1: \(Sup (S_{j'})\)たちが存在すると仮定する; ステップ2: \(\sum_{j' \in J'} Sup (S_{j'}) \in Ub (S)\)であることを見る; ステップ3: \(Sup (S_{j'})\)たちおよび\(Sup (S)\)が存在すると仮定する; ステップ4: \(Sup (S) \le \sum_{j' \in J'} Sup (S_{j'})\)であることを見る; ステップ5: \(Inf (S_{j'})\)たちが存在すると仮定する; ステップ6: \(\sum_{j' \in J'} Inf (S_{j'}) \in Lb (S)\)であることを見る; ステップ7: \(Inf (S_{j'})\)たちおよび\(Inf (S)\)が存在すると仮定する; ステップ8: \(\sum_{j' \in J'} inf (S_{j'}) \le Inf (S)\)であることを見る。
ステップ1:
\(Sup (S_{j'})\)たちが存在すると仮定しよう。
ステップ2:
各\(j' \in J'\)に対して、各\(j \in J\)に対して、\(s_{j', j} \le Sup (S_{j'})\)、なぜなら、\(Sup (S_{j'}) \in Ub (S_{j'})\)。
\(\sum_{j' \in J'} s_{j', j} \le \sum_{j' \in J'} Sup (S_{j'})\)、ここで、左辺は\(S\)の各要素である。
それが意味するのは、\(\sum_{j' \in J'} Sup (S_{j'}) \in Ub (S)\)。
ステップ3:
\(Sup (S_{j'})\)たちおよび\(Sup (S)\)が存在すると仮定しよう。
ステップ4:
ステップ2によって、\(\sum_{j' \in J'} Sup (S_{j'}) \in Ub (S)\)。
\(Sup (S)\)は\(Ub (S)\)のミニマム（最小値）であるから、\(Sup (S) \le \sum_{j' \in J'} Sup (S_{j'})\)。
ステップ5:
\(Inf (S_{j'})\)たちが存在すると仮定しよう。
ステップ6:
各\(j' \in J'\)に対して、各\(j \in J\)に対して、\(Inf (S_{j'}) \le s_{j', j}\)、なぜなら、\(Inf (S_{j'}) \in Lb (S_{j'})\)。
\(\sum_{j' \in J'} Inf (S_{j'}) \le \sum_{j' \in J'} s_{j', j}\)、ここで、右辺は\(S\)の各要素である。
それが意味するのは、\(\sum_{j' \in J'} Inf (S_{j'}) \in Lb (S)\)。
ステップ7:
\(Inf (S_{j'})\)たちおよび\(Inf (S)\)が存在すると仮定しよう。
ステップ8:
ステップ7によって、\(\sum_{j' \in J'} Inf (S_{j'}) \in Lb (S)\)。
\(Inf (S)\)は\(Lb (S)\)のマキシマム（最大値）であるから、\(\sum_{j' \in J'} inf (S_{j'}) \le Inf (S)\)。
