読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Bolzano & Weierstrassの定理(有界な数列は収束する部分列を持つ)

Bolzano Weierstrass の定理はCoqではもう既に証明されていて、しかもそれは標準ライブラリに備わっている!
Rtopology.vというライブラリのソースを見ればこの定理を見つけることができる。

Theorem Bolzano_Weierstrass :
  forall (un:nat -> R) (X:R -> Prop),
    compact X -> (forall n:nat, X (un n)) ->  exists l : R, ValAdh un l.

実数列unは nat -> R 型で、領域 X ⊂ R はR -> Prop 型で表現しているようだ。

ValAdh un lの定義は以下のとおりで、lに収束するunの部分列が存在することと同等の命題みたいだ。

Definition ValAdh (un:nat -> R) (x:R) : Prop :=
  forall (V:R -> Prop) (N:nat),
    neighbourhood V x ->  exists p : nat, (N <= p)%nat /\ V (un p).