時間が余っているので、全部、トポロジーの本を読む時間に使っています。

例えば、次のような命題を読んでます。
Lemma 2.1. Let f:A→B. If there are functions g:B→A and h:B→A such that
g(f(a))=a for every a in A and f(h(b))=b for every b in B, then f is bijective
and g=h=f^(-1).

意味は簡単に理解できるのに、厳密な証明はExercisesになってるんですよ。
一応、解いてみると、
f is bijective
∵f is injective
　∵[f(a)=f(a')]→[a=a']
　　∵a=g(f(a))=g(f(a'))=a'
∵f is surjective
　∵[b∈B]→[b=f(a) for at least one a∈A]
　　∵∃h(b)∈A, f(h(b))=b
g=h=f^(-1)
∵∀b∈B,∃a∈A, g(b)=g(f(a))=a
　∵f is surjective
∵∀b∈B,∃a∈A, f(h(b))=b
　g(f(h(b))=g(b)
　h(b)=a

意向に沿ったものかはわかりませんが、大体こんなものかと。こういうのを「Ｔ」に
入力したり、自動定理証明とかしたいですね。簡単に書きましたが、これ書くのに
１時間以上かかってます。宇宙人が言った通り、しっかりした本で１日５ページと
いうのは当たりました。実験成功です。ゆっくり精読するつもりです。