チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

2013-01-06から1日間の記事一覧

Coq で位相空間

前々回の記事「Coq でモジュラー束」で「群 G の部分群を述語 G -> Prop で表す」という方針を採用したところ、割と上手くいくということがわかりました。今回は他の題材として、「連結集合の連続写像による像は連結」であることを、同じ方針により証明して…