パーシャリーオーダードセット（半順序集合）、サブセット（部分集合）、サブセット（部分集合）のサブセット（部分集合）に対して、サブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）はサブセット（部分集合）のサブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）内に包含されており、サブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）はサブセット（部分集合）のサブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）内に包含されていることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
ターゲットコンテキスト
- 読者は、任意のパーシャリーオーダードセット（半順序集合）、任意のサブセット（部分集合）、当該サブセット（部分集合）の任意のサブセット（部分集合）に対して、当該サブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のローワーバウンド（下限）たちのセット（集合）内に包含されており、当該サブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）は当該サブセット（部分集合）のサブセット（部分集合）のアッパーバウンド（上限）たちのセット（集合）内に包含されているという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S\): \(\in \{\text{ 全てのパーシャリーオーダードセット（半順序集合）たち }\}\)
\(S^`\): \(\subseteq S\)
\(S^{``}\): \(\subseteq S^`\)
//
ステートメント（言明）たち:
\(Lb (S^`) \subseteq Lb (S^{``})\)
\(\land\)
\(Ub (S^`) \subseteq Ub (S^{``})\)
//
2: 証明
全体戦略: ステップ1: \(Lb (S^`) \subseteq Lb (S^{``})\)であることを見る; ステップ2: \(Ub (S^`) \subseteq Ub (S^{``})\)であることを見る。
ステップ1:
\(Lb (S^`) \subseteq Lb (S^{``})\)であることを見よう。
\(s \in Lb (S^`)\)を任意のものとしよう。
各\(p \in S^{``}\)に対して、\(p \in S^`\)、したがって、\(s \le p\)、なぜなら、\(s \in Lb (S^`)\)、それが意味するのは、\(s \in Lb (S^{``})\)。
したがって、\(Lb (S^`) \subseteq Lb (S^{``})\)。
ステップ2:
\(Ub (S^`) \subseteq Ub (S^{``})\)であることを見よう。
\(s \in Ub (S^`)\)を任意のものとしよう。
各\(p \in S^{``}\)に対して、\(p \in S^`\)、したがって、\(p \le s\)、なぜなら、\(s \in Ub (S^`)\)、それが意味するのは、\(s \in Ub (S^{``})\)。
したがって、\(Ub (S^`) \subseteq Ub (S^{``})\)。
