リニアリーオーダードセット（線形順序集合）およびサブセット（部分集合）に対して、セット（集合）の要素はサブセット（部分集合）のインフィマム（下限）である、もしも、要素がサブセット（部分集合）の各要素に等しいかそれより小さく、要素より大きいセット（集合）の各要素に対して、より小さいサブセット（部分集合）の要素がある場合、そしてその場合に限って、ことの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、リニアリーオーダードセット（線形順序集合）の定義を知っている。
- 読者は、パーシャリーオーダードセット（半順序集合）のサブセット（部分集合）のインフィマム（下限）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のリニアリーオーダードセット（線形順序集合）および任意のサブセット（部分集合）に対して、当該セット（集合）の任意の要素は当該サブセット（部分集合）のインフィマム（下限）である、もしも、当該要素が当該サブセット（部分集合）の各要素に等しいかそれより小さく、当該要素より大きい当該セット（集合）の各要素に対して、より小さい当該サブセット（部分集合）のある要素がある場合、そしてその場合に限って、という命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(S'\): \(\in \{\text{ 全てのリニアリーオーダードセット（線形順序集合）たち }\}\)で、任意のリニアオーダリング（線形順序）\(\lt'\)を持つもの
\(S\): \(\subseteq S'\)
\(s'\): \(\in S'\)
//
ステートメント（言明）たち:
\(s' = Inf (S)\)
\(\iff\)
\((\forall s \in S (s' \le s)) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s' \lt' s'' (\exists s \in S (s \lt' s'')))\)
//
2: 注
本命題は、\(S = \emptyset\)である時も成立する（空虚に）。
3: 証明
全体戦略: ステップ1: \(s' = Inf (S)\)であると仮定する; ステップ2: \((\forall s \in S (s' \le s)) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s' \lt' s'' (\exists s \in S (s \lt' s'')))\)であることを見る; ステップ3: \((\forall s \in S (s' \le s)) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s' \lt' s'' (\exists s \in S (s \lt' s'')))\)であると仮定する; ステップ4: \(s' = Inf (S)\)であることを見る; ステップ5: 本命題は、\(S = \emptyset\)である時も成立することをチェックする。
ステップ1:
\(s' = Inf (S)\)であると仮定しよう。
ステップ2:
\(s \in S\)を任意のものとしよう。
\(Inf (S) \in Lb (S)\)であるから、\(s' \le s\)、ローワーバウンド（下限）たちのセット（集合）の定義によって。
したがって、\(\forall s \in S (s' \le s)\)。
\(s'' \in S'\)を、\(s' \lt' s''\)を満たす任意のものとしよう。
\(s \lt' s''\)を満たす\(s \in S\)は無かったと仮定しよう。
それが意味することになるのは、各\(s \in S\)に対して、\(s'' \le' s\)、なぜなら、\(S'\)はリニアリーオーダード（線形順序付き）であった。
それが意味することになるのは、\(s'' \in Lb (S)\)。
しかし、\(s' \lt' s''\)であったから、\(s'\)は\(Lb (S)\)のマキシマム（最大）ではなかった、\(s' = Inf (S)\)に反する矛盾。
したがって、\(s \lt' s''\)を満たすある\(s \in S\)がある。
ステップ3:
\((\forall s \in S (s' \le s)) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s' \lt' s'' (\exists s \in S (s \lt' s'')))\)であると仮定しよう。
ステップ4:
\(s' \in Lb (S)\)、ローワーバウンド（下限）たちのセット（集合）の定義によって。
\(s'\)は\(Lb (S)\)のマキシマム（最大）でなかったと仮定しよう。
それが意味することになるのは、\(s'' \le' s'\)が成立しないある\(s'' \in Lb (S)\)があったということ。
\(S'\)はリニアリーオーダード（線形順序付き）であったから、\(s' \lt' s''\)。
仮定によって、\(s \lt' s''\)を満たすある\(s \in S\)があることになる、それが意味することになるのは、\(s'' \le' s\)は成立しないということ。
それが意味することになるのは、\(s'' \notin Lb (S)\)、\(s'' \in Lb (S)\)に反する矛盾。
したがって、\(s'\)は\(Lb (S)\)のマキシマム（最大）である。
したがって、\(s' = Inf (S)\)。
ステップ5:
本命題は、\(S = \emptyset\)である時も成立することをチェックしよう。
\(Lb (S) = S'\)。
\(Inf (S) = Max (Lb (S)) = Max (S')\)。
したがって、もしも、\(s' = Inf (S)\)である場合、\(\forall s \in S (s' \le s)\)は空虚に成立する、そして、\(\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s' \lt' s'' (\exists s \in S (s \lt' s''))\)は空虚に成立する: そうした\(s''\)は無い。
もしも、\((\forall s \in S (s' \le s)) \land (\forall s'' \in S' \text{ で、以下を満たすもの、つまり、 } s' \lt' s'' (\exists s \in S (s \lt' s'')))\)が成立する場合、そうした\(s''\)は無い、なぜなら、そうでなければ、\(\exists s \in S (s \lt' s'')\)は成立しないことになる、したがって、\(s' = Max (S') = Inf (S)\)。
