ℕの任意の無限部分集合からℕへの全単射の構成

**任意のℕの無限部分集合 から ℕ への全単射はあるか？あるならどのように構成するか？** といった疑問が浮かびました。直観的にはYesですが、構成法は少し考えないとわかりませんでした。

実際インターネットでも同じような質問と回答がなされています:

- https://math.stackexchange.com/questions/19450/do-all-infinite-subsets-of-mathbb-n-have-a-bijective-function-to-mathbb-n

そしてそこからより面白い系が証明できます:

**無限集合A からℕへの単射があるなら、Aからℕ への全単射が存在する。**

   - https://math.stackexchange.com/questions/1411351/if-a-set-is-countable-and-infinite-there-is-a-bijection-between-the-set-and-m

# 回答
前述のリンクを読むのが早いのですが、一応証明の概略を示します。無限部分集合をPと呼ぶことにすると、Pの要素を小さい順にa,b,c,d,...などとならべたとき、その順にℕの要素 0,1,2,3,..... を割り当てる写像は全単射です。単射なのはあたりまえです。全射性（＝任意のℕの要素 n が与えられたとき対応するPの要素はあるか？）は、Pが無限集合なので当然あります。ということで全単射をつくれました。

最近形式証明にはまっているのでCoqでも証明してみました。**証明に選択公理を使っているかどうか**はっきりしなかった（最小値を選ぶところでツォルンの補題とかつかってない？とか）のですが、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.
```