パーシャリーオーダードセット（半順序集合）、サブセット（部分集合）、サブセット（部分集合）のサブセット（部分集合）に対して、サブセット（部分集合）のインフィマム（下限）はサブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、サブセット（部分集合）のサプリマム（上限）はサブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のインフィマム（下限）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のサプリマム（上限）の定義を知っている。
- 読者は、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、当該サブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）内に包含されており、当該サブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）内に包含されているという命題を認めている。
ターゲットコンテキスト
- 読者は、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、もしも、当該サブセット（部分集合）のインフィマム（下限）および当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）が存在する場合、当該サブセット（部分集合）のインフィマム（下限）は当該サブセット（部分集合）のサブセット（部分集合）のインフィマム（下限）に等しいかそれより小さく、もしも、当該サブセット（部分集合）のサプリマム（上限）および当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）が存在する場合、当該サブセット（部分集合）のサプリマム（上限）は当該サブセット（部分集合）のサブセット（部分集合）のサプリマム（上限）に等しいかそれより大きいという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのパーシャリーオーダードセット（半順序集合）たち }\}\)
\(S^`\): \(\subseteq S\)
\(S^{``}\): \(\subseteq S^`\)
//
ステートメント（言明）たち:
(
\(\exists Inf (S^`) \land \exists Inf (S^{``})\)
\(\implies\)
\(Inf (S^`) \le Inf (S^{``})\)
)
\(\land\)
(
\(\exists Sup (S^`) \land \exists Sup (S^{``})\)
\(\implies\)
\(Sup (S^{``}) \le Sup (S^`)\)
)
//
2: 注
\(Inf (S^`)\)または\(Inf (S^{``})\)は独立に存在しないかもしれない: 例えば、\(S = \mathbb{Q}\)でカノニカル（正典）オーダリング（順序）を持つもの、\(S^` = ((- \sqrt{2}, \sqrt{2}) \cap \mathbb{Q}) \subseteq \mathbb{Q}\)、\(S^{``} = ((- 1, 1) \cap \mathbb{Q}) \subseteq \mathbb{Q}\)、そして、\(Inf (S^`)\)は存在しないが\(S^{``}\)は存在する; \(S = \mathbb{Q}\)でカノニカル（正典）オーダリング（順序）を持つもの、\(S^` = ((- 2, 2) \cap \mathbb{Q}) \subseteq \mathbb{Q}\)、\(S^{``} = ((- \sqrt{2}, \sqrt{2}) \cap \mathbb{Q}) \subseteq \mathbb{Q}\)、そして、\(Inf (S^`)\)は存在するが\(S^{``}\)は存在しない。
\(Sup (S^`)\)または\(Sup (S^{``})\)は独立に存在しないかもしれない、同様に。
3: 証明
全体戦略: ステップ1: \(Inf (S^`)\)および\(Inf (S^{``})\)は存在すると仮定する; ステップ2: \(Lb (S^`) \subseteq Lb (S^{``})\)であることを見る; ステップ3: \(Max (Lb (S^`)) \le Max (Lb (S^{``}))\)であることを見る; ステップ4: \(Sup (S^`)\)および\(Sup (S^{``})\)は存在すると仮定する; ステップ5: \(Ub (S^`) \subseteq Ub (S^{``})\)であることを見る; ステップ6: \(Min (Ub (S^{``})) \le Min (Ub (S^`))\)であることを見る。
ステップ1:
\(Inf (S^`)\)および\(Inf (S^{``})\)は存在すると仮定しよう。
ステップ2:
\(Lb (S^`) \subseteq Lb (S^{``})\)、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、当該サブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）内に包含されており、当該サブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）内に包含されているという命題によって。
ステップ3:
\(Inf (S^`) = Max (Lb (S^`))\)および\(Inf (S^{``}) = Max (Lb (S^{``}))\)。
\(Max (Lb (S^`)) \le Max (Lb (S^{``}))\)であることを見よう。
各\(p \in Lb (S^{``})\)に対して、\(p \le Max (Lb (S^{``}))\)、しかし、\(Max (Lb (S^`)) \in Lb (S^`) \subseteq Lb (S^{``})\)であるから、\(Max (Lb (S^`))\)はそうした\(p\)たちの1つである、したがって、\(Max (Lb (S^`)) \le Max (Lb (S^{``}))\)。
ステップ4:
\(Sup (S^`)\)および\(Sup (S^{``})\)は存在すると仮定しよう。
ステップ5:
\(Ub (S^`) \subseteq Ub (S^{``})\)、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、当該サブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）内に包含されており、当該サブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）内に包含されているという命題によって。
ステップ6:
\(Sup (S^`) = Min (Ub (S^`))\)および\(Sup (S^{``}) = Min (Ub (S^{``}))\)。
\(Min (Ub (S^{``})) \le Min (Ub (S^`))\)であることを見よう。
各\(p \in Ub (S^{``})\)に対して、\(Min (Ub (S^{``})) \le p\)、しかし、\(Min (Ub (S^`)) \in Ub (S^`) \subseteq Ub (S^{``})\)であるから、\(Min (Ub (S^`))\)はそうした\(p\)たちの1つである、したがって、\(Min (Ub (S^{``})) \le Min (Ub (S^`))\)。
