Zornの補題(1)

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の部分集合Tで次の3条件を満たすものを塔といいます。 (i) φ∈T, (ii) C∈T⇒f(C)∈T, (iii) Tの部分集合Dで(D;⊆)が鎖をなすならば、∪C∈DC∈Tとなる。

命題 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 ⊆ τ * γ
[証明終わり]