このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

各点で連続ならば連続

証明シェル 半形式証明スクリプト 具体例

次の命題を考える。

  • ターゲット命題： fが各点で連続ならば連続

通常は無意識に使っている選択公理の使い所が分かるように書いたので、証明が長くなった。

記号の乱用

記号の乱用をして、位相空間とその台集合を同じ記号で表す、つまり、X = (X, OX) のように書く。x∈X の開近傍〈open neighborhood〉の全体をN(x, X)と書く。

  • N(x, X) := {U∈OX | x∈U} ---(開近傍の定義)

Xを省略してN(x)と書くこともある。そのときは、適宜補って読む。

Γ（大文字ガンマ）は、仮定とする命題の集まりを表すが、明示されてない仮定をひっくるめてΓと書く。Γは出現ごとに違う意味かもしれない。省略記号「…」などと同じ。

例えば、証明要求の変形において

 Γ |-? A⇒B
 ------------
 Γ, A |-? B
 ------------
 Γ |-? B

1行目と2行目のΓは同じだが、3行目のΓはAを内部に含めてΓと呼んでいる。Γ' とか書けばよいが、面倒なのでΓ一文字で済ませる。

  • Γの意味： 色々変わるかも知れないが、その時点で使ってよい仮定の集まり。

セットアップ

  • 写像 f:X→Y がある。この時点では連続かどうかは分からない。

証明要求は、

  • Γ |-? fは各点で連続⇒fは連続

証明要求を変形して（証明のお膳立て作業）、

  • Γ, fは各点で連続 |-? fは連続

「fは連続」を論理式に直して、

  • Γ, fは各点で連続 |-? ∀B∈OY. f*(B)∈OX

さらに変形して、

  • Γ, fは各点で連続, B∈OY |-? f*(B)∈OX

記号を簡略化するために、A = f*(B) と置くと、

  • Γ, fは各点で連続, B∈OY, A = f*(B) |-? A∈OX

仮定に名前〈ラベル〉を付けておく。ラベル付けとラベルの参照方法については「ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2) - 檜山正幸のキマイラ飼育記」の「この記事の記述方法について」を参照。

  • fは各点で連続 ---(各点連続性)
  • B∈OY ---(Bは開集合)
  • A = f*(B) ---(Aの定義)

現時点でのターゲット命題は、

  • ターゲット命題： Aは開集合である。

これが示せれば、証明が完了する。

族Fの構成

Aでインデックスされた、Xの開集合族の族Fを構成（定義）する。この場合の「族の族」の意味は、

  • F:A→Pow(OX)

「『開集合族』の族」で、二重鉤括弧内の“族”は「集合の集合」、外側の“族”は「集合を値とする写像」の意味。

これからやることの雰囲気を知るには、次の絵が理解を助けるかもしれない。

Fは次のように定義する。

  • x∈A に対して、F(x) := {U∈N(x) | f*(U)⊆B} ---(Fの定義)

この定義からただちに次が言える。

  1. U∈F(x) ⇒ U∈OX ---(F1)
  2. U∈F(x) ⇒ x∈U ---(F2)
  3. U∈F(x) ⇒ U⊆A ---(F3)

念のために$(F3)を示すなら：



証明要求： Γ, U∈F(x) |-? U⊆A
$(Fの定義)と仮定 U∈F(x) より

 f*(U)⊆B

$?(像と逆像の随伴性)より

 U⊆f*(B)

$(Aの定義)より

 U⊆A

ターゲットが示せた。

選択公理の適用

Fに選択公理を適用したいが、そのためには、次の命題が必要。

  • サブターゲット命題： ∀x∈A. F(x)は空ではない ---(Fの非空性)

このサブターゲットに対する証明要求は、

  • Γ |-? ∀x∈A. F(x)は空ではない

変形して、

  • Γ, x∈A |-? F(x)は空ではない

「空ではない」を論理式にすると、

  • Γ, x∈A |-? ∃U∈OX. U∈F(x)

現時点のΓのなかには次が入っていることを注意しておく。

  • ∀x∈X. ∀V∈N(f(x)). ∃U∈N(x). f*(U)⊆V ---(各点連続性)

この命題は、次の推論規則としても使える。

  • Γ, x∈X, V∈N(f(x) |- ∃U∈N(x). f*(U)⊆V ---(各点連続性 規則)

推論規則に現れる自由変数（この例では、x, V）は、リネームや代入（具体化）してもよい。



証明要求： Γ, x∈A |-? ∃U∈OX. U∈F(x)
Γ（様々な仮定）, x∈A から、

  B∈OY

  f(x)∈B

これらと$(開近傍の定義)より、

  B∈N(f(x))

$(各点連続性 規則)を、VにBを代入して使って、

  ∃U∈N(x). f*(U)⊆B


存在が保証された（実在する）Uに関して((ここでも、実際には選択公理の特殊形を使っている。束縛変数Uとは別な文字、例えばWを使ったほうが混乱が少ない。Wは存在するものを1つ選んで名付けたもの。))、

  U∈N(x)

  f*(U)⊆B

$(Fの定義)より

  U∈F(x)

U∈N(x) から U∈OX は言えるので、

 ∃U∈OX. U∈F(x)

ターゲットが示せた。

この時点で、$(Fの非空性)は定理となった。

Fに選択公理が使えるので、次の選択関数Sが存在する。

  • x∈X に対して S(x)∈F(x) ---(Sの選択性)

$(Sの選択性)と、$(F1), $(F2), $(F3)から次が言える。

  1. S(x)∈OX ---(S1)
  2. x∈S(x) ---(S2)
  3. S(x)⊆A ---(S3)

Aが開集合であること

次のサブターゲット命題を考える。

  • サブターゲット命題： ∪{S(x) | x∈A} = A ---(Sの合併)

サブターゲットを2つに分割する。

  • サブターゲット命題： ∪{S(t) | t∈A}⊆A ---(Sの合併 1)
  • サブターゲット命題： A⊆∪{S(t) | t∈A} ---(Sの合併 2)

束縛変数名をtに変えたのは混乱を避けるためである。スコープが違えば同じ変数名を使い回してもよいが、混乱（人的ミス）の危険がある*1。

上記2つのサブターゲットを示す。



証明要求： Γ |-? ∪{S(t) | t∈A}⊆A



（xは任意であるが((これは、x∈X である自由変数の導入を宣言している。forall x in X ... end というブロック構造で、ブロックの終わりを「xは任意だったので」で示している。))）x∈∪{S(t) | t∈A} と仮定する。

合併の定義より、a∈A が存在して

  x∈S(a) ---(1)

$(S3)より

  S(a)⊆A ---(2)

$(1), $(2)より

  x∈A

以上より、

 x∈∪{S(t) | t∈A} ⇒ x∈A

xは任意だったから、

 ∀x∈X.(x∈∪{S(t) | t∈A} ⇒ x∈A)

つまり

 ∪{S(t) | t∈A}⊆A

ターゲットが示せた。
証明要求： Γ |-? A⊆∪{S(t) | t∈A}
（xは任意であるが）x∈A と仮定する。

$(S2)より

  x∈S(x)

よって、

  ∃t∈A.x∈S(t)

合併の定義より

  x∈∪{S(t) | t∈A}

以上より

  x∈A ⇒ x∈∪{S(t) | t∈A}

xは任意だったから、

  ∀x∈X.(x∈A ⇒ x∈∪{S(t) | t∈A})

つまり

  A⊆∪{S(t) | t∈A}

ターゲットが示せた。

この時点で、$(Sの合併)は定理となり、

  • ∪{S(x) | x∈A} = A

$(S1)より、S(x)は開集合であり、開集合の合併は開集合なので、

  • ∪{S(x) | x∈A}∈OX

つまり、

  • A∈OX

最初のターゲットである「Aは開集合」が示せた。

*1:しかし、出現する変数を全部違う文字にすると、すぐさま文字が足りなくなるので、使い回しはやむを得ない。