Optimistic Mathematics のサイトで「Zornの補題」を選出公理から数式の変形で導くということを試みています。あまりうまくいっていないのですがとりあえず引用しておきます。
Zornの補題
集合Xにおける関係≦が、 (1) x≦x、 (2) x≦y, y≦z ⇒ x≦z、 (3) x≦y, y≦x ⇒ x=y を満たすとき、(X;≦)を順序集合といいます。 Xの元x,yがx≦yまたはy≦xを満たすときx,yは比較可能であるといいます。 Xの任意の2元が比較可能であるとき、(X;≦)は全順序集合または鎖であるといいます。 Y⊆Xとすると(Y;≦)も順序集合となります。 (Y;≦)が鎖のとき(X;≦)に含まれる鎖といいます。 Y⊆Xに対して、a∈Xが任意のx∈Yに対してx≦aとなるとき、 aをYの上界といいます。 Yの上界全体の集合をu.b.Yと書きます。 u.b.Y≠φのとき、Yは上に有界であるといいます。
集合Xの部分集合全体の集合をXのべき集合といい、P(X)と書きます。
命題(Zornの補題) (X;≦)は順序集合とし、それに含まれる任意の鎖は上に有界であるとすると、 Xには極大元が存在する。
定義 GをXに含まれる鎖全体の集合とします。 (G={C∈P(X)|任意のx,y∈Cは比較可能}) f:G→Gを次のように定義します。
選出公理により、g:P(X)-{φ}→Xで Xの空でない各部分集合Aに対しg(A)∈Aとなるものがあります。 C∈Gとすれば仮定によりu.b.C≠φ。 もしu.b.C-C≠φならば、f(C)=C∪{g(u.b.C-C)}とします。 (f(C)∈Gとなります。) u.b.C-C=φならば、f(C)=Cとします。
f(C)=Cとすると、u.b.C⊆Cとなります。 x0∈u.b.Cとします。 もしx0
命題 Gは塔である。
証明 (i) φの任意の2元は比較可能なので、φ∈G。
(ii) C∈Gとすると、f(C)の定義よりf(C)∈G。
(iii) D⊆Gとし、(D;⊆)は鎖をなしているとすれば、 Dの元全体の和集合はGの元となることを示します。 x, x'∈∪C∈DCが比較可能であることを示せばよい。 x∈C, x'∈ C', C, C'∈D となるようなC, C'が存在します。 (D;⊆)は鎖であるから、C⊆C'またはC'⊆C。 C'⊆Cとすればx, x'∈Cとなり、 x, x'は比較可能となります。 C⊆C'とすればx, x'∈C'となり、 x, x'は比較可能となります。
[証明終わり]
命題 すべての塔の共通部分T0は最小の塔となる。
証明 (i) 任意の塔Tに対してφ∈Tなので φ∈∩Tは塔T=T0となります。
(ii) C∈∩Tは塔T=T0とすると 任意の塔Tに対してC∈Tとなるのでf(C)∈Tとなります。 f(C)∈∩Tは塔T=T0となります。
(iii) D⊆T0=∩Tは塔Tとし、 (D;⊆)は鎖をなしているとすれば、 Dの元全体の和集合はT0の元となることを示します。 任意の塔Tに対してD⊆Tであり(D;⊆)は鎖をなしているので ∪C∈DC∈Tとなります。 よって∪C∈DC∈∩Tは塔T=T0となります。
[証明終わり]
命題 (T0;⊆)は鎖となる。
証明 T0のどの元とも比較可能な T0の元全体の集合をSとし、 S=T0を示せばよい。 (φ∈SだからS≠φ)
(1) C'∈SのときV(C')={C∈T0|C⊆C'またはp(C')⊆C} とおけばV(C')は塔となる。
証明 (i) φ⊆C'なのでφ∈V(C')となります。
(ii) C∈V(C')ならばC⊆C'またはp(C')⊆C。 C⊆C'ならばC=C'またはC⊂C'。 C=C'ならばf(C')=f(C)。 C⊂C'とします。 T0は塔でC∈T0であるからf(C)∈T0。 Sの定義からC'⊆f(C)またはf(C)⊆C'。 C'⊆f(C)とするとC⊂C'だからf(C)=Cとはならないので、 f(C)=C∪{x}となるxが存在します。 C⊂C'⊆f(C)=C∪{x}となるので、f(C)=C'。 よってf(C)⊆C'。 f(C')⊆CならばC⊆f(C)からf(C')⊆f(C)。
(iii) D⊆V(C'), (D;⊆)は鎖とします。 D'=∪C∈DCとおきます。 すべてのC∈Dが、C⊆C'とすると、D'⊆C'となります。 あるC∈Dが、C⊆C'ではないとすると、C∈V(C')であることから、 f(C')⊆Cとなり、f(C')⊆C⊆D'となります。
(2) Sは塔となる。
証明 (i) 任意のC∈T0に対してφ⊆Cなので、φ∈Sとなります。
(ii) (1)よりT0=V(C')。 T0の任意の元CとSの任意の元C'に対して C⊆C'またはf(C')⊆Cとなります。 C⊆C'のときはC⊆f(C')となりf(C')∈S。
(iii) D⊆S, (D;⊆)は鎖とします。 D'=∪C∈DCとおきます。C'∈C(X)とします。 すべてのC∈Dが、C⊆C'とすると、D'⊆C'となります。 あるC∈Dが、C⊆C'ではないとすると、C∈Sであることから、 C'⊆Cとなり、C'⊆C⊆D'となります。
[証明終わり]
T0が塔になること、 T0が鎖になることの証明を詳しく見てみます。
T0が塔になることの証明
Xを集合、O⊆Xとします。 G⊆P(X)、 P⊆P(G)で
- O⊆C (∀C∈G)
- O∈G
- Z⊆G∧Z∈P ⇒ ∪Z∈G (∀Z∈P(G))
をみたすものとします。 f: G→G を
- C⊆f(C) (∀C∈G)
- C⊆D∧D⊆f(C) ⇒ C=D∨D=f(C) (∀C∈G∀D∈G)
をみたすものとします。
- Init(Y)={O}={C∈G|C=O} ⊆ G (Y⊆G)
- Suc(Y)={f(C)|C∈Y}=∪C∈G{D∈G|D=f(C)∧C∈Y} ⊆ G (Y⊆G)
- Lim(Y)={∪Z|Z⊆Y∧Z∈P}∩G= ∪Z∈P(G){C∈G|C=∪Z∧Z⊆Y∧Z∈P} ⊆ G (Y⊆G)
と定義すると以下のことが成り立ちます。
- Y⊆Y' ⇒ Init(Y)⊆Init(Y') (∀Y∈P(G)∀Y'∈P(G))
- Y⊆Y' ⇒ Suc(Y)⊆Suc(Y') (∀Y∈P(G)∀Y'∈P(G))
- Y⊆Y' ⇒ Lim(Y)⊆Lim(Y') (∀Y∈P(G)∀Y'∈P(G))
- Init(∩X)⊆∩{Init(Y)|Y∈X} (∀X∈P(P(G)))
∩X⊆Y (∀Y∈X)
⇒ Init(∩X)⊆Init(Y) (∀Y∈X)
⇒ Init(∩X)⊆∩{Init(Y)|Y∈X}
- Suc(∩X)⊆∩{Suc(Y)|Y∈X} (∀X∈P(P(G)))
∩X⊆Y (∀Y∈X)
⇒ Suc(∩X)⊆Suc(Y) (∀Y∈X)
⇒ Suc(∩X)⊆∩{Suc(Y)|Y∈X}
- Lim(∩X)⊆∩{Lim(Y)|Y∈X} (∀X∈P(P(G)))
∩X⊆Y (∀Y∈X)
⇒ Lim(∩X)⊆Lim(Y) (∀Y∈X)
⇒ Lim(∩X)⊆∩{Lim(Y)|Y∈X}
- Suc(∪X)=∪{Suc(Y)|Y∈X} (∀X∈P(P(G)))
次のように定義します。
- T1 = {Y∈P(G)|Init(Y)⊆Y} ⊆ P(G)
- T2 = {Y∈P(G)|Suc(Y)⊆Y} ⊆ P(G)
- T3 = {Y∈P(G)|Lim(Y)⊆Y} ⊆ P(G)
- T* = T1∩T2∩T3 ⊆ P(G)
- T0 = ∩T* ⊆ G
T0∈T*
証明 (i) T0∈T1
Y∈T1 (∀Y∈T*)
⇔ Init(Y)∈Y (∀Y∈T*)
⇒ ∩{Init(Y)|Y∈T*}⊆∩T*
⇒ Init(∩T*)⊆∩T*
⇔ ∩T*∈T1
⇒ T0∈T1
(ii) T0∈T2
Y∈T2 (∀Y∈T*)
⇔ Suc(Y)⊆Y (∀Y∈T*)
⇒ ∩{Suc(Y)|Y∈T*}⊆∩T*
⇒ Suc(∩T*)⊆∩T*
⇔ ∩T*∈T2
⇒ T0∈T2
(iii) T0∈T3
Y∈T3 (∀Y∈T*)
⇔ Lim(Y)⊆Y (∀Y∈T*)
⇒ ∩{Lim(Y)|Y∈T*}⊆∩T*
⇒ Lim(∩T*)⊆∩T*
⇔ ∩T*∈T3
⇒ T0∈T3
[証明終わり]
T0が鎖になることの証明
次のように定義します。
- L(C) = {D∈G|D⊆C} ⊆ G (C∈G)
- U(C) = {D∈G|C⊆D} ⊆ G (C∈G)
- S(C) = L(C)∪U(C) ⊆ G (C∈G)
- S = {C∈G|T0⊆S(C)}
- V(C) = L(C)∪U(f(C)) ⊆ G (C∈G)
次のことが成り立ちます。
- Suc(U(C))⊆U(C) (∀C∈G)
Suc(U(C))
= ∪D∈G{E∈G|f(D)=E∧D∈U(C)}
= ∪D∈G({E∈G|f(D)=E}∩{E∈G|C⊆D})
⊆ ∪D∈G({E∈G|D⊆E}∩{E∈G|C⊆D})
⊆ ∪D∈G{E∈G|C⊆E}
= {E∈G|C⊆E}
= U(C)
- Suc(L(C))∩U(C)={C,f(C)}⊆L(C)∪U(f(C))=V(C) (∀C∈G)
Suc(L(C))∩U(C)
= (∪D∈G{E∈G|f(D)=E∧D∈L(C)})∩U(C)
= ∪D∈G({E∈G|f(D)=E}∩{E∈G|D⊆C}∩{E∈G|C⊆E})
⊆ ∪D∈G({E∈G|f(D)=E}∩({E∈G|D=C}∪{E∈G|C=E}))
⊆ ∪D∈G({E∈G|f(C)=E}∪{E∈G|C=E})
= {E∈G|f(C)=E}∪{E∈G|C=E}
- Z⊆L(C)⇒{∪Z}∩G⊆L(C) (∀C∈G∀Z∈P(G))
- Z∩U(C)≠φ⇒{∪Z}∩G⊆U(C) (∀C∈G∀Z∈P(G))
- Z⊆L(C)∪U(D)⇒{∪Z}∩G⊆L(C)∪U(D) (∀C∈G∀D∈G∀Z∈P(G))
{E∈G|E=∪Z}∩{E∈G|Z⊆L(C)∪U(D)}
⊆ {E∈G|E=∪Z}∩({E∈G|Z⊆L(C)}∪{E∈G|Z∩U(D)≠φ})
⊆ {E∈G|E=∪Z}∩({E∈G|∪Z∈L(C)}∪{E∈G|∪Z∈U(D)})
⊆ L(C)∪U(D)
- Lim(L(C)∪U(D))⊆L(C)∪U(D) (∀C∈G∀D∈G)
- S=∩{S(C)|C∈T0}
- V(C)⊆S(f(C)) (∀C∈G)
- f(C)∈{D∈G|V(C)⊆S(D)} (∀C∈G)
∀C∈G(C∈S ⇒ T0∩V(C)∈T*)
証明 (i) T0∩V(C)∈T1
O⊆C
⇔ O∈L(C)
⇒ O∈V(C)
⇔ V(C)∈T1
⇒ T0∩V(C)∈T1
(ii) T0∩V(C)∈T2
Suc(V(C))=Suc(L(C)∪U(f(C)))=Suc(L(C))∪Suc(U(f(C)))
Suc(U(f(C)))⊆U(f(C))
Suc(T0)⊆T0⊆S(C)
Suc(T0∩V(C))⊆S(C)∩(Suc(L(C))∪Suc(U(f(C)))) =L(C)∪(U(C)∩Suc(L(C)))∪U(f(C))⊆V(C)
⇒ T0∩V(C)∈T2
(iii) T0∩V(C)∈T3
Lim(L(C)∪U(f(C)))⊆L(C)∪U(f(C))
⇔ Lim(V(C))⊆V(C)
⇔ V(C)∈T3
⇒ T0∩V(C)∈T3
[証明終わり]
T0∩S∈T*
証明 (i) T0∩S∈T1
O⊆C (∀C∈T0)
⇔ O∈L(C) (∀C∈T0)
⇒ O∈S(C) (∀C∈T0)
⇔ O∈∩{S(C)|C∈T0}=S
⇔ S∈T1
⇒ T0∩S∈T1
(ii) T0∩S∈T2
{f(C)}⊆{D∈G|V(C)⊆S(D)}⊆{D∈G|T0⊆S(D)}=S (∀C∈S)
⇒ Suc(S)={f(C)|C∈S}⊆S
⇔ S∈T2
⇒ T0∩S∈T2
(iii) T0∩S∈T3
Lim(L(C)∪U(C))⊆L(C)∪U(C) (∀C∈G)
⇔ Lim(S(C))⊆S(C) (∀C∈G)
⇔ S(C)∈T3 (∀C∈G)
⇒ S=∩{S(C)|C∈T0}∈T3
⇒ T0∩S∈T3
[証明終わり]
T0が塔になることの証明
p∈P(X×Y), f:Z→X, g:Z→Y に対して p+: P(X)→P(Y), p-: P(Y)→P(X), p*(f,g): P(Z)→P(Z) を
- p+(A) = ∪x∈A{y∈Y|(x,y)∈p} (∀A∈P(X))
- p-(B) = ∪y∈B{x∈X|(x,y)∈p} (∀B∈P(X))
- p*(f,g)(C) = {z∈C|(f(z),g(z))∈p} (∀C∈P(Z))
と定義します。
h:X→Y に対して h+: P(X)→P(Y), h-: P(Y)→P(X),
- h+(A) = ∪x∈A{y∈Y|h(x)=y} (∀A∈P(X))
- h-(B) = ∪y∈B{x∈X|h(x)=y} (∀B∈P(X))
と定義します。
f: P(X)→P(Y) が
- f(A) = ∪x∈Af({x}) (∀A∈P(X)) を満たすとき、f は IMG を満たす
- y,z∈f({x}) ⇒ y = z (∀x∈X∀y∈Y∀z∈Y) を満たすとき、f は MAP を満たす
- A≠φ ⇒ f(A)≠φ (∀A∈P(X)) を満たすとき、f は EXT を満たす
と定義します。
f,k: P(X)→P(Y), g: P(Y)→P(Z) のとき
- (-f)(B) = {x∈X|f({x})∩B≠φ} (∀B∈P(Y))
- (f+g)(A) = ∪y∈f(A)g({y}) (∀A∈P(X))
- (f*g)(A) = ∩y∈f(A)g({y}) (∀A∈P(X))
- (f∪k)(A) = ∪x∈A(f({x})∪k({x})) (∀A∈P(X))
- (f∩k)(A) = ∪x∈A(f({x})∩k({x})) (∀A∈P(X))
と定義します。 f,k: P(X)→P(Y), g: P(Y)→P(Z) が IMG を満たすとすると
- (f+g)(A) = g(f(A)) (∀A∈P(X))
- (f∪k)(A) = f(A)∪k(A) (∀A∈P(X))
となります。
f,k: P(X)→P(Y), g: P(Y)→P(Z) のとき 次のことが成り立ちます。
(f+g)+h=f+(g+h) (h: P(Z)→P(V))
( (f+g)+h )(A)
= {v∈V|∃z∈Z(z∈(f+g)(A)∧v∈h({z}))}
= {v∈V|∃z∈Z(∃y∈Y(y∈f(A)∧z∈g({y}))∧v∈h({z}))}
= {v∈V|∃y∈Y(y∈f(A)∧∃z∈Z(z∈g({y})∧v∈h({z})))}
= {v∈V|∃y∈Y(y∈f(A)∧v∈(g+h)({y}))}
= (f+(g+h))(A) (∀A∈P(X))
(f+g)*h⊇f+(g*h) (h: P(Z)→P(V))
( (f+g)*h )(A)
= {v∈V|∀z∈Z(z∈(f+g)(A)⇒v∈h({z}))}
= {v∈V|∀z∈Z(∃y∈Y(y∈f(A)∧z∈g({y}))⇒v∈h({z}))}
⊇ {v∈V|∃y∈Y(y∈f(A)∧∀z∈Z(z∈g({y})⇒v∈h({z})))}
= {v∈V|∃y∈Y(y∈f(A)∧v∈(g*h)({y}))}
= (f+(g*h))(A) (∀A∈P(X))
g が IMG を満たすとき (f+g)*h=f+(g*h) (h: P(Z)→P(V))
( (f+g)*h )(A)
= {v∈V|∀z∈Z(z∈(f+g)(A)⇒v∈h({z}))}
= {v∈V|∀z∈Z(z∈g(f(A))⇒v∈h({z}))}
= (g*h)(f(A))
= (f+(g*h))(A) (∀A∈P(X))
f⊆k∧g⊆h⇒f+g⊆k+h (h: P(Y)→P(Z))
(f+g)(A)
= {z∈Z|∃y∈Y(y∈f(A)∧z∈g({y}))}
⊆ {z∈Z|∃y∈Y(y∈k(A)∧z∈h({y}))}
= (k+h)(A) (∀A∈P(X))
k⊆f∧g⊆h⇒f*g⊆k*h (h: P(Y)→P(Z))
(f+g)(A)
= {z∈Z|∀y∈Y(y∈f(A)⇒z∈g({y}))}
⊆ {z∈Z|∀y∈Y(y∈k(A)⇒z∈h({y}))}
= (k+h)(A) (∀A∈P(X))
f⊆k⇒-f⊆-k
(-f)(B)
= {x∈X|f({x})∩B≠φ}
⊆ {x∈X|k({x})∩B≠φ}
= (-k)(B) (∀B∈P(Y))
f が IMG を満たすとき -(-f)=f
(-(-f))(A)
= {y∈Y|(-f)({y})∩A≠φ}
= {y∈Y|∃x∈X(x∈(-f)({y})∧x∈A)}
= {y∈Y|∃x∈X(y∈f({x})∧x∈A)}
= f(A) (∀A∈P(X))
1⊆f+(-f)
( (f+(-f) )(A)
= {x∈X|f({x})∩f(A)≠φ}
⊇ A (∀A∈P(X))
(f*g)+h⊆f*(g+h) (h: P(Z)→P(V))
( (f*g)+h )(A)
= {v∈V|∃z∈Z∀y∈Y( (y∈f(A)⇒z∈g({y}) )∧v∈h({z}))}
⊆ {v∈V|∀y∈Y∃z∈Z(y∈f(A)⇒(z∈g({y})∧v∈h({z})))}
= (f*(g+h))(A) (∀A∈P(X))
f⊆(f*g)*(-g)
( (f*g)*(-g) )(A)
= {y∈Y|∀z∈Z(z∈(f*g)(A)⇒y∈(-g)({z}))}
= {y∈Y|∀z∈Z(∀v∈Y(v∈f(A)⇒z∈g({v}))⇒y∈(-g)({z}))}
⊇ {y∈Y|∀z∈Z( (y∈f(A)⇒z∈g({y}) )⇒z∈({y}))}
⊇ {y∈Y|y∈f(A)} (∀A∈P(X))
f が MAP を満たすとき (-f)+f⊆1
( (-f)+f )(B)
= {y∈Y|∃x∈X(x∈(-f)(B)∧y∈f({x}))}
= {y∈Y|∃x∈X(∃v∈Y(v∈f({x})∧v∈B)∧y∈f({x}))}
= {y∈Y|∃x∈X(y∈B∧y∈f({x}))}
⊆ {y∈Y|y∈B} (∀B∈P(Y))
g が MAP を満たすとき f*(g+h)=(f*g)*h (h: P(Z)→P(V))
(f*(g+h))(A)
= {v∈V|∀y∈Y(y∈f(A)⇒v∈(g+h)({y}))}
= {v∈V|∀y∈Y(y∈f(A)⇒∃z∈Z(z∈g({y})∧v∈h({z})))}
= {v∈V|∀y∈Y(y∈f(A)⇒∀z∈Z(z∈g({y})⇒v∈h({z})))}
= (f*(g*h))(A) (∀A∈P(X))
f*(g*h)⊆(f+g)*h (h: P(Z)→P(V))
(f*(g*h))(A)
= {v∈V|∀y∈Y(y∈f(A)⇒∀z∈Z(z∈g({y})⇒v∈h({z})))}
= {v∈V|∀z∈Z∀y∈Y(y∈f(A)⇒(z∈g({y})⇒v∈h({z})))}
= {v∈V|∀z∈Z∀y∈Y( (y∈f(A)∧z∈g({y}) )⇒v∈h({z}))}
⊆ {v∈V|∀z∈Z(∃y∈Y(y∈f(A)∧z∈g({y}))⇒v∈h({z}))}
= {v∈V|∀z∈Z(z∈(f+g)(A)⇒v∈h({z}))}
= ( (f+g)*h )(A) (∀A∈P(X))
f, k が IMG を満たすとき -(f∪k)=(-f)∪(-k)
(-(f∪k))(B)
= {x∈X|(f∪k)({x})∩B≠φ}
= {x∈X|(f({x})∪k({x}))∩B≠φ}
= {x∈X|f({x})∩B≠φ}∪{x∈X|k({x})∩B≠φ}
= (-f)(B)∪(-k)(B)
= ( (-f)∪(-k) )(B) (∀B∈P(Y))
(-(f∩k))({y})=( (-f)∩(-k) )({y}) (∀y∈Y)
(-(f∩k))({y})
= {x∈X|(f∩k)({x})∩{y}≠φ}
= {x∈X|(f({x})∩k({x}))∩{y}≠φ}
= {x∈X|f({x})∩{y}≠φ}∩{x∈X|k({x})∩{y}≠φ}
= (-f)({y})∩(-k)({y})
= ( (-f)∩(-k) )({y}) (∀y∈Y)
1*(-(f∩k))=1*( (-f)∩(-k) )
(1*(-(f∩k)))(B)
= {x∈X|∀y∈Y(y∈B∧x∈(-(f∩k))({y}))}
= {x∈X|∀y∈Y(y∈B∧(f∩k)({x})∩{y}≠φ)}
= {x∈X|∀y∈Y(y∈B∧y∈(f∩k)({x}))}
= {x∈X|∀y∈Y(y∈B∧y∈(f({x})∩k({x}))}
= {x∈X|∀y∈Y(y∈B∧y∈f({x})∧y∈k({x}))}
= {x∈X|∀y∈Y(y∈B∧x∈(-f)({y})∧x∈(-k)({y}))}
= {x∈X|∀y∈Y(y∈B∧x∈(-f)({y})∩(-k)({y}))}
= {x∈X|∀y∈Y(y∈B∧x∈( (-f)∩(-k) )({y}))}
= (1*( (-f)∩(-k) ))(B) (∀B∈P(Y))
-(f+g)=(-g)+(-f)
(-(f+g))(C)
= {x∈X|(f+g)({x})∩C≠φ}
= {x∈X|∃z∈Z(z∈(f+g)({x})∧z∈C)}
= {x∈X|∃z∈Z(∃y∈Y(y∈f({x})∧z∈g({y}))∧z∈C)}
= {x∈X|∃y∈Y(∃z∈Z(z∈g({y})∧z∈C)∧y∈f({x}))}
= {x∈X|∃y∈Y(y∈(-g)(C)∧x∈(-f)({y}))}
= ( (-g)+(-f) )(C) (∀C∈P(Z))
g が EXT を満たすとき f+(g*h)⊆f+(g+h) (h: P(Y)→P(Z))
(f+(g*h))(A)
= {v∈V|∃y∈Y(y∈f(A)∧v∈(g*h)({y}))}
= {v∈V|∃y∈Y(y∈f(A)∧∀z∈Z(z∈g({y})⇒v∈h({z})))}
⊆ {v∈V|∃y∈Y(y∈f(A)∧∃z∈Z(z∈g({y})∧v∈h({z})))}
= {v∈V|∃y∈Y(y∈f(A)∧v∈(g+h)({y}))}
= (f+(g+h))(A) (∀A∈P(X))
g が EXT を満たすとき f*(g*h)⊆f*(g+h) (h: P(Y)→P(Z))
(f*(g*h))(A)
= {v∈V|∀y∈Y(y∈f(A)⇒v∈(g*h)({y}))}
= {v∈V|∀y∈Y(y∈f(A)⇒∀z∈Z(z∈g({y})⇒v∈h({z})))}
⊆ {v∈V|∀y∈Y(y∈f(A)⇒∃z∈Z(z∈g({y})∧v∈h({z})))}
= {v∈V|∀y∈Y(y∈f(A)⇒v∈(g+h)({y}))}
= (f*(g+h))(A) (∀A∈P(X))
(f+g)∪(f+h)=f+(g∪h) (h: P(Y)→P(Z))
( (f+g)∪(f+h) )(A)
= {z∈Z|∃x∈X(x∈A∧(z∈(f+g)({x})∨z∈(f+h)({x})))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈g({y}))∨∃y∈Y(y∈f({x})∧z∈h({y}))))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧(z∈g({y})∨z∈h({y}))))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈(g∪h)({y}))}
= {z∈Z|∃x∈X(x∈A∧z∈(f+(g∪h))({x}))}
= (f+(g∪h))(A) (∀A∈P(X))
(f+g)∩(f+h)⊇f+(g∩h) (h: P(Y)→P(Z))
( (f+g)∩(f+h) )(A)
= {z∈Z|∃x∈X(x∈A∧(z∈(f+g)({x})∧z∈(f+h)({x})))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈g({y}))∧∃y∈Y(y∈f({x})∧z∈h({y}))))}
⊇ {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧(z∈g({y})∧z∈h({y}))))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈(g∩h)({y}))}
= {z∈Z|∃x∈X(x∈A∧z∈(f+(g∩h))({x}))}
= (f+(g∩h))(A) (∀A∈P(X))
f が MAP を満たすとき (f+g)∩(f+h)=f+(g∩h) (h: P(Y)→P(Z))
( (f+g)∩(f+h) )(A)
= {z∈Z|∃x∈X(x∈A∧(z∈(f+g)({x})∧z∈(f+h)({x})))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈g({y}))∧∃y∈Y(y∈f({x})∧z∈h({y}))))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧(z∈g({y})∧z∈h({y}))))}
= {z∈Z|∃x∈X(x∈A∧(∃y∈Y(y∈f({x})∧z∈(g∩h)({y}))}
= {z∈Z|∃x∈X(x∈A∧z∈(f+(g∩h))({x}))}
= (f+(g∩h))(A) (∀A∈P(X))
f, k が IMG を満たすとき 1*f⊆1*k⇒f⊆k
f(A)
= ∪x∈Af({x})
= ∪x∈A∩y∈{x}f({y})
= ∪x∈A(1 * f)({x})
⊆ ∪x∈A(1 * k)({x})
= ∪x∈A∩y∈{x}k({y})
= ∪x∈Ak({x})
= k(A) (∀A∈P(X))
{x}⊆(f*(-f)){x}
(f*(-f)){x}
= {v∈X|∀y∈Y(y∈f({x})⇒v∈(-f)({y}))}
= {v∈X|∀y∈Y(y∈f({x})⇒y∈f({v}))}
⊇ {x}
k∩h⊆(f*( (-f)+k) )∩h (h: P(X)→P(Y))
( (f*( (-f)+k) )∩h )(A)
= ∪x∈A( (f*( (-f)+k) )({x})∩h({x}))
⊇ ∪x∈A( ( (f*(-f) )+k )({x})∩h({x}))
⊇ ∪x∈A(k({x})∩h({x}))
= (k∩h)(A) (∀A∈P(X))
(f+g)∩(f*h)⊆f+(g∩h) (h: P(Y)→P(Z))
( (f+g)∩(f*h) )(A)
= {z∈Z|∃x∈X(x∈A∧z∈(f+g)({x})∧z∈(f*h)({x}))}
= {z∈Z|∃x∈X(x∈A∧∃y∈Y(y∈f({x})∧z∈g({y}))∧∀y∈Y(y∈f({x})⇒z∈h({y})))}
⊆ {z∈Z|∃x∈X(x∈A∧∃y∈Y(y∈f({x})∧z∈g({y})∧z∈h({y}))}
= ( (f+(g∩h) )(A) (∀A∈P(X))
(f∪k)+g=(f+g)∪(k+g)
( (f∪k)+g )(A)
= {z∈Z|∃y∈Y(y∈(f∪k)(A)∧z∈g({y}))}
= {z∈Z|∃y∈Y(∃x∈X(x∈A∧(y∈f({x})∨y∈k({x}))∧z∈g({y})))}
= {z∈Z|∃x∈X(x∈A∧∃y∈Y( (y∈f({x})∨y∈k({x}) )∧z∈g({y})))}
= {z∈Z|∃x∈X(x∈A∧ (∃y∈Y( (y∈f({x})∧z∈g({y}) )∨∃y∈Y(y∈k({x}))∧z∈g({y}))))}
= ( (f+g)∪(k+g) )(A) (∀A∈P(X))
(f∩k)+g⊆(f+g)∩(k+g)
( (f∩k)+g )(A)
= {z∈Z|∃y∈Y(y∈(f∩k)(A)∧z∈g({y}))}
= {z∈Z|∃y∈Y(∃x∈X(x∈A∧(y∈f({x})∧y∈k({x}))∧z∈g({y})))}
= {z∈Z|∃x∈X(x∈A∧∃y∈Y( (y∈f({x})∧y∈k({x}) )∧z∈g({y})))}
⊆ {z∈Z|∃x∈X(x∈A∧ (∃y∈Y( (y∈f({x})∧z∈g({y}) )∧∃y∈Y(y∈k({x}))∧z∈g({y}))))}
= ( (f+g)∩(k+g) )(A) (∀A∈P(X))
e: X→P(X), u: P(X)⊇{{x}|x∈X}→X を
- e(x) = {x}
- u({x}) = x
と定義します。
Xを集合、G⊆P(X)、P⊆P(G)、p: P(G)→P(G)、p(H)=H∩P、 c: P(X)→P(X)、c(Y)=Y∩Gとします。 o, s: G→G を
- 1 ⊆ o+ + ⊆+
- s+ ⊆ ⊆+
- ⊆+ ∩ (s+ + ⊆-) ⊆ 1 ∪ s+
を満たすものとします。 j: P(P(X))→P(X) を IMG を満たし、 ξ が IMG、MAP、EXT を満たし ζ が ψ + ζ ⊆ ψ (∀ψ: P(G)→P(G)) を満たすならば
- ξ + ⊆- + ζ + j ⊆ ξ
- ξ + ⊆+ + ζ + j ⊇ ξ または ξ + ⊆+ + ζ + j = Φ (Φ: P(G)→P(G), Φ(H)=φ)
を満たすものとします。
- Init = o+: P(G)→P(G)
- Suc = s+: P(G)→P(G)
- Lim = e + ⊆- + p + j+ + c: P(G)→P(G)
- T1 = ⊆*(Init,1) = ⊆*(o+,1): P(P(G))→P(P(G))
- T2 = ⊆*(Suc,1) = ⊆*(s+,1): P(P(G))→P(P(G))
- T3 = ⊆*(Lim,1) = ⊆*(e + ⊆- + p + j+ + c, 1) : P(P(G))→P(P(G))
- T* = T1 + T2 + T3 : P(P(G))→P(P(G))
- ρ: P(G)→P(P(G)), ρ(X) = P(G)
- τ = ρ + (T* * u): P(G)→P(G)
と定義します。 f: P(G)→P(G) とすると次のことが成り立ちます。
- f + Init ⊆ f ⇔ f + e + T1 = f + e ⇔ (f + e + T1) * u ⊆ f
- f + Suc ⊆ f ⇔ f + e + T2 = f + e ⇔ (f + e + T2) * u ⊆ f
- f + Lim ⊆ f ⇔ f + e + T3 = f + e ⇔ (f + e + T3) * u ⊆ f
- f + e + T1 = f + e, f + e + T2 = f + e, f + e + T3 = f + e ⇒ f + e + T* = f + e
- f + e + T* = f + e ⇒ τ ⊆ f
τ = ρ + (T* * u) = (ρ + T*) * u ⊆ (f + e + T*) * u = (f + e) * u = f
τ + e + T* = τ + e
証明 (i) τ + e + T1 = τ + e
(T1 * u) + Init ⊆ T1 * (u + Init) = T1 * (T1 + u + Init) ⊆ T1 * (T1 + u) = T1 * u
τ + Init = ρ + (T* * u) + Init = ρ + ( (T* + T1) * u ) + Init = ρ + T* + (T1 * u) + Init
⊆ ρ + T* + (T1 * u) = ρ + (T* + T1) * u = ρ + (T* * u) = τ
(ii) τ + e + T2 = τ + e
(T2 * u) + Suc ⊆ T2 * (u + Suc) = T2 * (T2 + u + Suc) ⊆ T2 * (T2 + u) = T2 * u
τ + Suc = ρ + (T* * u) + Suc = ρ + ( (T* + T2) * u ) + Suc = ρ + T* + (T2 * u) + Suc
⊆ ρ + T* + (T2 * u) = ρ + (T* + T2) * u = ρ + (T* * u) = τ
(iii) τ + e + T3 = τ + e
(T3 * u) + Lim ⊆ T3 * (u + Suc) = T3 * (T3 + u + Lim) ⊆ T3 * (T3 + u) = T3 * u
τ + Lim = ρ + (T* * u) + Lim = ρ + ( (T* + T3) * u ) + Lim = ρ + T* + (T3 * u) + Lim
⊆ ρ + T* + (T3 * u) = ρ + (T* + T3) * u = ρ + (T* * u) = τ
[証明終わり]
T0が鎖になることの証明
次のように定義します。
- β = ⊆- ∪ (Suc + ⊆+): P(G)→P(G)
- γ = ⊆- ∪ ⊆+: P(G)→P(G)
- α = (⊆- + Suc) ∩ ⊆+: P(G)→P(G)
次のことが成り立ちます。
- α ⊆ β
1
⊆ (1 * α) * (-α)
= (1 * α) * (-( (⊆- + s+ ) ∩ ⊆+))
= (1 * α) * ( (-(⊆- + s+) ) ∩ (-⊆+))
= (1 * α) * ( (s- + ⊆+) ∩ ⊆- )
⊆ (1 * α) * ( (s- + ⊆+) ∩ (s- * (s+ + ⊆-)) )
⊆ (1 * α) * (s- + (⊆+ ∩ (s+ + ⊆-)))
⊆ (1 * α) * (s- + (1 ∪ s+))
= (1 * α) * (s- ∪ (s- + s+))
= (1 * α) * (s- ∪ 1)
(1 * α)
⊆ ( (1 * α) * (1 ∪ s-) ) * (-(1 ∪ s-))
⊆ 1 * (-(1 ∪ s-))
= 1 * (1 ∪ s+)
α ⊆ 1 ∪ s+ ⊆ β
- ξ、η が IMG、MAP、EXT を満たすならば ( (ξ + ⊆-) ∪ (η + ⊆+) ) + Lim ⊆ (ξ + ⊆-) ∪ (η + ⊆+) (∀ξ,η: P(G)→P(G))
ζ が ψ + ζ ⊆ ψ (∀ψ: P(G)→P(G))を満たすならば
( (ξ + ⊆-) ∪ (η + ⊆+) ) + ζ + j
= (ξ + ⊆- + ζ + j) ∪ (η + ⊆+ + ζ + j) ⊆ ξ または ⊇ η
( (ξ + ⊆-) ∪ (η + ⊆+) ) + Lim
= ( (ξ + ⊆-) ∪ (η + ⊆+) ) + e + ⊆- + p + + j+ + c
⊆ (ξ + ⊆-) ∪ (η + ⊆+)
- β ⊆ Suc + γ
β
= ⊆- ∪ (s+ + ⊆+)
⊆ (s+ + s- + ⊆-) ∪ (s+ + ⊆+)
= s+ + ( (s- + ⊆-) ∪ ⊆+ )
= s+ + ( (-(-⊆- + -s-)) ∪ ⊆+ )
= s+ + ( (-(⊆+ + s+)) ∪ ⊆+ )
⊆ s+ + ( (-(⊆+ + ⊆+)) ∪ ⊆+ )
⊆ s+ + ( (-⊆+) ∪ ⊆+ )
⊆ s+ + (⊆- ∪ ⊆+)
= Suc + γ
- -γ = γ
-γ = -(⊆- ∪ ⊆+) = (-⊆-) ∪ (-⊆+) = ⊆+ ∪ ⊆- = γ
- (τ * γ) * τ ⊆ (τ * γ) * γ
A∈P(G), (τ * γ)(A)≠φ のとき
( (τ * γ) * τ )(A)
= ∩y∈(τ * γ)(A)τ({y})
= ∩y∈(τ * γ)(A)τ(A)
= τ(A)
⊆ ( (τ * γ) * (-γ) )(A)
= ( (τ * γ) * γ )(A)
A∈P(G), (τ * γ)(A)=φ のとき
( (τ * γ) * τ )(A)
= ∩y∈φτ({y})
= ∩y∈φγ({y})
= ( (τ * γ) * γ )(A)
τ ⊆ (τ * γ) * β
証明 (i) ( (τ * γ) * (β ∩ τ) ) + e + T1 = ( (τ * γ) * (β ∩ τ) ) + e
β + Init ⊆ ⊆- ⊆ β
(β ∩ τ) + Init ⊆ β + Init ⊆ β
(β ∩ τ) + Init ⊆ τ + Init ⊆ τ
(β ∩ τ) + Init ⊆ β ∩ τ
( (τ * γ) * (β ∩ τ) ) + Init ⊆ (τ * γ) * (β ∩ τ)
(ii) ( (τ * γ) * (β ∩ τ) ) + e + T2 = ( (τ * γ) * (β ∩ τ) ) + e
β + Suc
= (⊆- ∪ (Suc + ⊆+)) + Suc
⊆ (⊆- + Suc) ∪ (Suc + ⊆+ + Suc)
⊆ (⊆- + Suc) ∪ (Suc + ⊆+ + ⊆+)
⊆ (⊆- + Suc) ∪ (Suc + ⊆+)
( (τ * γ) * (β ∩ τ) ) + Suc
⊆ (τ * γ) * ( (β ∩ τ) + Suc)
⊆ (τ * γ) * ( (β + Suc) ∩ (τ + Suc) )
⊆ (τ * γ) * ( ( (⊆- + Suc) ∪ (Suc + ⊆+) ) ∩ τ )
⊆ (τ * γ) * ( ( (⊆- + Suc) ∪ (Suc + ⊆+) ) ∩ γ ∩ τ )
⊆ (τ * γ) * ( ( (⊆- + Suc) ∪ (Suc + ⊆+) ) ∩ (⊆- ∪ ⊆+) ∩ τ)
⊆ (τ * γ) * ( (⊆- ∪ ( (⊆- + Suc) ∩ ⊆+ ) ∪ (Suc + ⊆+) ) ∩ τ)
⊆ (τ * γ) * (β ∩ τ)
(iii) ( (τ * γ) * (β ∩ τ) ) + e + T3 = ( (τ * γ) * (β ∩ τ) ) + e
β + Lim
= (⊆- ∪ (Suc + ⊆+)) + Lim
⊆ ⊆- ∪ (Suc + ⊆+)
= β
(β ∩ τ) + Lim ⊆ β + Lim ⊆ β
(β ∩ τ) + Lim ⊆ τ + Lim ⊆ τ
(β ∩ τ) + Lim ⊆ β ∩ τ
( (τ * γ) * (β ∩ τ) ) + Lim ⊆ (τ * γ) * (β ∩ τ)
[証明終わり]
τ ⊆ τ * γ
証明 (i) (τ * γ) + e + T1 ⊆ (τ * γ) + e
γ + Init ⊆ ⊆- ⊆ γ
τ * (γ + Init) ⊆ τ * γ
(τ * γ) + Init ⊆ τ * γ
(ii) (τ * γ) + e + T2 ⊆ (τ * γ) + e
τ ⊆ (τ * γ) * β ⊆ (τ * γ) * (Suc + γ) ⊆ ( (τ * γ) + Suc ) * γ
(τ * γ) + Suc ⊆ ( ( (τ * γ) + Suc ) * γ ) * γ ⊆ τ * γ
(iii) (τ * γ) + e + T2 ⊆ (τ * γ) + e
γ + Lim
= (⊆- ∪ ⊆+) + Lim
⊆ ⊆- ∪ ⊆+
= γ
τ * (γ + Lim) ⊆ τ * γ
(τ * γ) + Lim ⊆ τ * γ
[証明終わり]