Berestein

いや、集合論の定理の方です。 ℕ ⊆ A ⊆ ℕ なら、A = ℕ みたいなのです。(要素の個数的な⊆です)

　　List Bool
　　ℕ ∧ ℕ

が ℕ と一対一な証明はやってたんですが、Hω2 つまり、List (Maybe Bool) はどうなのと。

List A が可算なら

　　ℕ ⊆ List A ⊆ List (Maybe A) ⊆ (List A ∧ List Bool) ⊆ ℕ

って感じなので、

　　(List A ∧ List Bool) は List (Maybe A) でないものも含んでるので
　　それをのぞいて数えなおせば良い

ってことは Bernstein で証明できるはず。 なんですが、ぜんぜんできない。

そこでわかったんですが、 Bernstein って集合じゃないとだめらしい。しかも、得られる Bijection は構成的ではないらしい。

直接証明も難しくはないんだが、そこそこめんどうではある。でも、まぁ、こういう

　　構成的じゃないけど、いきなり写像の存在が言える

のは集合論のすごいところだなとは思いました。

Bernstein の方の証明もだいぶ書いてある。両方書くのは悪くないな。