任意のℕの無限部分集合 から ℕ への全単射はあるか？あるならどのように構成するか？ といった疑問が浮かびました。直観的にはYesですが、構成法は少し考えないとわかりませんでした。
実際インターネットでも同じような質問と回答がなされています:
そしてそこからより面白い系が証明できます:
無限集合A からℕへの単射があるなら、Aからℕ への全単射が存在する。
回答
前述のリンクを読むのが早いのですが、一応証明の概略を示します。無限部分集合をPと呼ぶことにすると、Pの要素を小さい順にa,b,c,d,...などとならべたとき、その順にℕの要素 0,1,2,3,..... を割り当てる写像は全単射です。単射なのはあたりまえです。全射性（＝任意のℕの要素 n が与えられたとき対応するPの要素はあるか？）は、Pが無限集合なので当然あります。ということで全単射をつくれました。
最近形式証明にはまっているのでCoqでも証明してみました。証明に選択公理を使っているかどうかはっきりしなかった（最小値を選ぶところでツォルンの補題とかつかってない？とか）のですが、Coqでの証明をしてみると、選択公理は使っていないよと、Coq先生が教えてくれました。
Require Import Arith Lia Classical.
Require Import Ensembles Finite_sets_facts Infinite_sets Wf_nat.
Ltac inv H := inversion H;subst;try discriminate;clear H.
(* 自然数の部分集合における最小値 *)
Definition minR (P:Ensemble nat) n :=
In _ P n /\ (forall m, m < n -> ~In _ P m).
(* 部分集合に要素があれば最小値は存在し *)
Lemma inh_min: forall (P:Ensemble nat),
Inhabited _ P -> exists n, minR P n.
Proof. unfold min; intros P Pinh. destruct Pinh as [n Hn]. revert Hn.
apply (lt_wf_ind _). intros a IH H. clear n.
destruct(classic(forall m, m < a -> ~P m)).
exists a. split;auto.
apply not_all_ex_not in H0. destruct H0 as [m].
apply not_imply_elim in H0 as H1.
apply not_imply_elim2 in H0 as H2.
assert (H3: P m) by (now apply NNPP).
destruct (IH _ H1 H3) as [k [Hk1 Hk2]].
now exists k. Qed.
(* 最小値は、あれば唯一に決まる *)
Lemma min_inj : forall P n m, minR P n -> minR P m -> n =m.
Proof. intros P n m H. revert m. induction H.
intros m Hm. inv Hm.
destruct (lt_eq_lt_dec n m) as [[|]|].
pose proof (H2 _ l). contradiction. auto.
pose proof (H0 _ l). contradiction. Qed.
(* 無限集合は要素を持ち *)
Lemma inf_inh: forall (P:nat->Prop), ~Finite _ P -> Inhabited _ P.
Proof. intros P Pinf.
destruct (approximant_can_be_any_size _ _ P Pinf 1) as [B [H1 H2]].
inv H1. inv H2. apply Inhabited_intro with (x:=x).
auto with sets. Qed.
(* 有限個の要素を取り出してもなお無限である *)
Lemma inf_sub: forall (P:nat->Prop) (a:nat),
~Finite _ P -> ~Finite _ (Subtract _ P a).
Proof. intros ? ? ? ?. destruct(classic (P a)).
apply H. replace P with (Add _ (Subtract nat P a) a).
now apply Add_preserves_Finite. auto with sets.
pose proof (Non_disjoint_union' _ _ _ H1). now rewrite H2 in H0. Qed.
Lemma inf_setminus: forall (P A: nat->Prop),
~Finite _ P -> Finite _ A -> ~Finite _ (Setminus _ P A).
Proof. intros. induction H0.
- now rewrite Seminus_Empty_set_r.
- unfold Add. rewrite Setminus_Union_r.
intros HC. elim IHFinite.
destruct (classic(P x)).
replace (Setminus nat P A) with
(Add _ (Setminus nat (Setminus nat P A) (Singleton nat x)) x).
now apply Add_preserves_Finite.
remember (Setminus nat P A) as X.
apply Extensionality_Ensembles;cbv;split;intros ? ?.
destruct H3. destruct H3. auto. inv H3. split. auto. auto.
destruct (Nat.eq_dec x x0). subst.
apply Union_intror. cbv. constructor.
apply Union_introl. cbv. split. auto. intros. inv H4. contradiction.
replace (Setminus nat (Setminus nat P A) (Singleton nat x)) with
(Setminus nat P A) in HC. assumption.
apply Extensionality_Ensembles;cbv;split;intros ? ?.
split. auto. intros. inv H4. now destruct H3. destruct H3. auto. Qed.
(** 道具がそろったので証明はじめ *)
Section Construct_Bijection.
Variable P: nat->Prop.
Variable Pinf: ~Finite _ P.
(* Q := 自身より小さい数の集合 *)
Definition Q (a:nat): nat->Prop := fun x:nat => x < a /\ P x.
(* Q は有限集合 *)
Lemma q_fin: forall a, Finite _ (Q a).
Proof. induction a.
- replace (Q 0) with (Empty_set nat).
now apply Empty_is_finite.
apply Extensionality_Ensembles. cbv;split;intros ? ?.
inv H. destruct H. lia.
- assert (Q (S a) = Q a \/ Q (S a) = (Add _ (Q a) a)).
{ destruct (classic(P a)).
right. apply Extensionality_Ensembles;cbv;split;intros ? ?.
destruct H0. destruct (Nat.eq_dec x a).
subst. apply Union_intror. auto with sets.
apply Union_introl. cbv. split. lia. auto.
inv H0. cbv in H1. destruct H1. split. lia. auto.
inv H1. split. lia. auto.
left. apply Extensionality_Ensembles;cbv;split;intros ? ?.
destruct H0. destruct (Nat.eq_dec x a). subst. contradiction.
split. lia. auto. destruct H0. split. lia. auto. }
destruct H. now rewrite H. rewrite H.
now apply Add_preserves_Finite. Qed.
Lemma surj_helper: forall a n, P a -> cardinal _ (Q a) n->
exists b, cardinal _ (Q b) (S n) /\ P b.
Proof. intros. assert (~Finite _ (Subtract _ (Setminus _ P (Q a)) a)).
{ apply inf_sub. apply inf_setminus.
assumption. apply cardinal_finite in H0. auto. }
destruct (inh_min _ (inf_inh _ H1)) as [b Hb].
exists b. split.
replace (Q b) with (Add _ (Q a) a).
apply card_add.
- auto.
- cbv. intros []. lia.
- destruct Hb.
destruct H2.
destruct H2.
assert (a<>b). { intro HC. elim H4. subst. constructor. }
assert (a<b). { apply NNPP; intros HC. apply H5. cbv. split. lia. auto. }
apply Extensionality_Ensembles;cbv;split;intros ? ?.
+ inv H8. destruct H9. split;auto. lia.
inversion H9. symmetry in H8. subst. split. lia. auto.
+ destruct (Nat.eq_dec a x). subst.
constructor 2. constructor.
constructor 1. cbv. destruct H8. split;auto.
assert (x < b). lia. apply NNPP;intros HC. elim (H3 _ H10).
cbv. split. split. auto. intros []. lia. intros. inv H11. contradiction.
- inv Hb. inv H2. inv H4. auto. Qed.
(** ここからメイン *)
(* P ->N の関数構成。 rank a n は a は n番目に小さいと読んでもよい *)
Inductive rank (a:nat): nat-> Prop :=
| Def_of_rank n: P a -> cardinal _ (Q a) n -> rank a n.
(* rank はP内の要素であれば存在し *)
Lemma rank_functional a: P a -> exists k, rank a k.
Proof. intros. pose proof (q_fin a).
destruct (finite_cardinal _ _ H0) as [n Hn].
exists n. now constructor. Qed.
(* rank は存在すれば一意に決まる *)
Lemma rank_inj a n1 n2: rank a n1 -> rank a n2 -> n1 = n2.
Proof. intros H. revert n2. induction H;intros. inv H1.
eapply cardinal_unicity;eassumption. Qed.
(*全射性は？ 任意のn番目となる 要素a は常にあるか？ 無限だからある *)
Lemma rank_surj n: exists a, rank a n.
Proof. induction n.
- destruct (inh_min _ (inf_inh _ Pinf)) as [a]. exists a.
constructor. now inv H. enough ((Q a) = Empty_set _).
rewrite H0. constructor.
destruct H. apply Extensionality_Ensembles;cbv;split;intros ? ?.
exfalso. destruct H1. pose proof (H0 x). apply H3. lia. auto. inv H1.
- destruct IHn as [a]. inv H.
destruct (surj_helper _ _ H0 H1) as [b [Hb1 Hb2]].
exists b. now constructor. Qed.
(* rank が bijection なのはほぼ自明 *)
Definition f := fun a n => P a -> rank a n.
Definition g:= fun n a => rank a n.
Lemma id_r: forall a n, P a -> f a n -> g n a.
Proof. cbv;auto. Qed.
Lemma id_l: forall a n, g n a -> f a n.
Proof. cbv;auto. Qed.
End Construct_Bijection.