現代数学概説Ⅰ
1章 $2 例題2
以下を示せ。
1) Γ(x) ∍y ⇔ Γ.exp-1(y)∍x.
2) A'⊆A⊆M とする時 Γ(A')⊆Γ(A).
3) B'⊆B⊆N とする時 Γ.exp-1(B')⊆Γ.exp-1(B).
4) A⊆DomΓ とする時 A⊆Γ.exp-1 (Γ(A)).
5) B⊆ImΓ とする時 B⊆Γ(Γ.exp-1(A)).
注) .exp-1はマイナス1乗を示し、Γ.exp-1(x)はΓ(x)の逆対応を示す。
==============================
1) Γ(x) ∍y ⇔ Γ.exp-1(y)∍x.
対応の定義により
Γ=(G, M, N). GはΓのgraphで M, Nは集合
M∍x, N∍y, G∍(x,y)
逆対応の定義により
G.exp-1 は (y, x)である。
従って、
Γ(x) ∍y ⇔ Γ.exp-1(y)∍x.
は明らか。
□
---------------------------------------------------
2) A'⊆A⊆M とする時 Γ(A')⊆Γ(A).
対応の定義により
Γ=(G, M, N).
forall x : M∍x, N∍y, G∍(x, y)、G(A)∍y
定義により全てのxに対応するyがある。
従って、A'⊆A ⇒ G(A')⊆G(A).
G(A)はΓ(A)と読み替えることが出来るので
A'⊆A⊆M ⇒ Γ(A')⊆Γ(A).
□
---------------------------------------------------
3) B'⊆B⊆N とする時 Γ.exp-1(B')⊆Γ.exp-1(B).
2)より
B'⊆B⊆N ⇒ Γ(B')⊆Γ(B).
1)より
Γ(B')⊆Γ(B) ⇒ Γ.exp-1(B')⊆Γ.exp-1(B).
従って、
B'⊆B⊆N ⇒ Γ.exp-1(B')⊆Γ.exp-1(B).
は明らか。
□
----------------------------------------------------
4) A⊆DomΓ とする時 A⊆Γ.exp-1 (Γ(A)).
定義より
Γ=(G, M, N). :: G:対応 M:始集合 N:終集合
2)より
A ⊆ DomΓ ⊆ M ⇒ Γ(A) ⊆ ImΓ.
故に
Γ(A) ⊆ ImΓ⊆N
3)より
Γ(A) ⊆ ImΓ⊆N ⇒Γ.exp-1(Γ(A)) ⊆ ImΓ.exp-1
1)より、一対多も含まれる事も有りうるので
A ⊆ Γ.exp-1(Γ(A)).
□
5) B⊆ImΓ とする時 B⊆Γ(Γ.exp-1 (A)).
定義より
Γ=(G, M, N). :: G:対応 M:始集合 N:終集合
3)より
B ⊆ ImΓ ⊆ N ⇒ Γ.exp-1(B) ⊆ DomΓ.
故に
Γ.exp-1(B) ⊆ DomΓ.exp-1⊆N
2)より
Γ(B) ⊆ DomΓ⊆N ⇒Γ(Γ.exp-1(A)) ⊆ DomΓ.exp-1
1)より、一対多も含まれる事も有りうるので
B ⊆ Γ(Γ.exp-1(A)).
□
==============================
4), 5)は定義、用語がごちゃごちゃしており
混乱してしまった。頭のよろしい人なら難なく通過できるのでしょうけど、私が解いたら1週間かかりました。。汗）
肝は、対応、逆対応を経ると広がる所でしょうか。
SOFTWARE FOUNDATIONSに出てくる非形式証明は、
内部仕様、又は設計仕様にあたるみたい。
後日Coqで証明してみて、非形式証明の出来を確認する。
これを続ければ、その内Coq使いと思えるようになるのかな。。
