Library Schroeder.Schroeder


If A is of cardinal less than B and conversely, then A and B are equipollent In other words, if there is an injective map from A to B and an injective map from B to A then there exists a map from A onto B.
(based on a proof by Fraenkel)

Require Import Ensembles. Require Import Relations_1. Require Import Powerset. Require Import Classical_Prop.
Require Import Setminus_fact.
Require Import Sums.
Require Import Functions.
Require Import Equipollence.

Section Schroeder_Bernstein.

We need the decidability of the belonging relation on sets This is equivalent to classical logic

Definition in_or_not_in (U : Type) (x : U) (A : Ensemble U) :=
  classic (In U A x).

A and B are sets of elements in the univers U

Variable U : Type.

Let SU := Ensemble U.

Variable A B : SU.
  Section Bijection.

We now show that if f and g are injections resp from A to B and from B to A, then there is a subset J of A s.t. h, defined to be f on A and the converse of g on A\J is a bijection from A to B

  Variable f g : Relation U.
  Hypothesis f_inj : injection U A B f.   Hypothesis g_inj : injection U B A g.

  Let Imf : Ensemble U -> Ensemble U := Im U f.
  Let Img : Ensemble U -> Ensemble U := Im U g.

Constructing J s.t. g(B\f(J))=A\J
(Setminus U A C) denotes the difference A\C (Included U A C) means that A is included in C

    Let F (C : SU) := Setminus U A (Img (Setminus U B (Imf C))).

    Let D (C : SU) := Included U C (F C).

    Let J := Set_Sum U D.

We show that so-built J is the subset we are looking for
J is Tarski's fix-point of F, a function which is growing w.r.t. inclusion
Lemma: F is growing

      Lemma F_growing :
       forall C C' : SU, Included U C C' -> Included U (F C) (F C').
      Proof.
        intros; unfold F in |- *.
        apply Setminus_contravariant.
        unfold Img in |- *.
        apply Im_stable_par_incl.
        apply Setminus_contravariant.
        unfold Imf in |- *.
        apply Im_stable_par_incl.
        assumption.
      Qed.

We show F(J)=A\Img(B\Imf(J))=J
First left-to-right inclusion
Lemma: J_is_in_FJ (Included U J (F J))

         Lemma J_is_in_FJ : Included U J (F J).
         Proof.
           unfold J in |- *.
           apply Set_Sum_is_majoring.
           intros C C_in_D.
           cut (Transitive (Ensemble U) (Included U)).
             2: apply Inclusion_is_transitive.
           intro Incl_is_trans.
           unfold Transitive in Incl_is_trans.
           apply Incl_is_trans with (F C).
             assumption.
             apply F_growing.
             apply Set_Sum_is_minoring.
             assumption.
         Qed.

Then right-to-left inclusion
Lemma: FJ_is_in_J (Included U (F J) J)

         Lemma FJ_is_in_J : Included U (F J) J.
         Proof.
           unfold J in |- *.
           apply Set_Sum_is_minoring.
           red in |- *.
           red in |- *.
           apply F_growing.
           exact J_is_in_FJ.
         Qed.

We show that h, which is f on J and g elsewhere, is a bijection

    Inductive h (x y : U) : Prop :=
      | hl_intro : In U J x -> f x y -> h x y
      | hr_intro : Setminus U B (Imf J) y -> g y x -> h x y.

Theorem: h_bij (bijection U A B h)

  Theorem h_bij : bijection U A B h.

h is from A to B
    Lemma h1 : Rel U A B h.
    Proof.
        apply Rel_intro; do 2 intro; intro h_x_y.
          elim h_x_y.
            elim f_inj.
            intro f_Rel; intros.
            elim f_Rel.
            intros f_sur_A f_sur_B.
            apply f_sur_A with y; assumption.

          elim g_inj.
          intro g_Rel; intros.
          elim g_Rel.
          intros g_sur_B g_sur_A.
          apply g_sur_A with y; assumption.

        elim h_x_y.
          elim f_inj.
          intro f_Rel; intros.
          elim f_Rel.
          intros f_sur_A f_sur_B.
          apply f_sur_B with x; assumption.

        elim g_inj.
        intro g_Rel; intros.
        elim g_Rel.
        intros g_sur_B g_sur_A.
        apply g_sur_B with x; assumption.

    Qed.

h satisfies to_at_most_one_output
    Lemma h2 : to_at_most_one_output U h.
    Proof.
      red in |- *; intros x y z h_x_y h_x_z.
      elim h_x_y.

        elim h_x_z.
          elim f_inj.
          unfold to_at_most_one_output in |- *; intros f_Rel f_au_plus_1_im; intros.
          apply f_au_plus_1_im with x; assumption.

          do 2 intro; intro x_in_J; intro.
          cut (Included U J (F J)).
            unfold Included in |- *; unfold F in |- *;
             unfold Setminus in |- *; intro Hyp.
            elim (Hyp x x_in_J).
            intros x_in_A x_in_non_Img.
            elim x_in_non_Img.
            red in |- *.
            red in |- *.
            apply Im_intro with z; assumption.
          exact J_is_in_FJ.

        elim h_x_z.
          intro x_in_J; intros.
          cut (Included U J (F J)).
            unfold Included in |- *; unfold F in |- *;
             unfold Setminus in |- *; intro Hyp.
            elim (Hyp x x_in_J).
            intros x_in_A x_in_non_Img.
            elim x_in_non_Img.
            red in |- *.
            red in |- *.
            apply Im_intro with y; assumption.
          exact J_is_in_FJ.

          elim g_inj.
          unfold from_at_most_one_input in |- *; do 3 intro; intro g_au_plus_1_ant;
           intros.
          apply g_au_plus_1_ant with x; assumption.

    Qed.

h satisfies to_at_least_one_output
    Lemma h3 : to_at_least_one_output U A h.
    Proof.
      red in |- *.
      intros.
      elim (in_or_not_in U x (Img (Setminus U B (Imf J)))).

      unfold Img in |- *; intro x_in_Img.
      elim x_in_Img.
      intros y g_y_x H1.
      exists y.
      apply hr_intro; assumption.

      intros.
        elim f_inj.
        unfold to_at_least_one_output in |- *; do 2 intro; intro f_au_moins_1_im;
         intro.
        elim (f_au_moins_1_im x H).
        intros y f_x_y.
        exists y.
        apply hl_intro.
          apply FJ_is_in_J.
          red in |- *; red in |- *; red in |- *.
          split; assumption.
        assumption.

    Qed.

h satisfies from_at_most_one_input
    Lemma h4 : from_at_most_one_input U h.
    Proof.
      red in |- *; do 3 intro; intros h_x_z h_y_z.
      elim h_x_z.

        elim h_y_z.
          elim f_inj.
          intros.
          cut (forall x y z : U, f x z -> f y z -> x = y).
          intro Hyp; apply Hyp with z; assumption.
          assumption.

          unfold Setminus in |- *; intro z_in_Setminus_B_Imf_J; intros.
          elim z_in_Setminus_B_Imf_J.
          intros z_in_B z_in_non_Imf_J.
          elim z_in_non_Imf_J.
          red in |- *.
          red in |- *.
          apply Im_intro with x; assumption.

        elim h_y_z.
          unfold Setminus in |- *; do 2 intro; intro z_in_Setminus_B_Imf_J;
           intros.
          elim z_in_Setminus_B_Imf_J.
          intros z_in_B z_in_non_Imf_J.
          elim z_in_non_Imf_J.
          red in |- *.
          red in |- *.
          apply Im_intro with y; assumption.

          elim g_inj.
          intros.
          cut (forall z x y : U, g z x -> g z y -> x = y).
          intro Hyp; apply Hyp with z; assumption.
          assumption.

    Qed.

h satisfies from_at_least_one_input
    Lemma h5 : from_at_least_one_input U B h.
    Proof.
      red in |- *.
      intros.
      elim (in_or_not_in U y (Imf J)).

      unfold Imf in |- *; intro y_in_Imf.
          elim y_in_Imf.
          intros x f_x_y; intro.
          exists x.
          apply hl_intro; assumption.

        intros.
          elim g_inj.
          unfold to_at_least_one_output in |- *; do 2 intro; intro g_au_moins_1_im;
           intro.
          elim (g_au_moins_1_im y H).
          intros x g_y_x.
          exists x.
          apply hr_intro.
          red in |- *.
          split; assumption.
          assumption.

    Qed.

We can now resume the proof of h_bij

    Proof.
    exact (bijection_intro U A B h h1 h2 h3 h4 h5).
    Qed.

  End Bijection.

Schroeder-Bernstein-Cantor Theorem

Theorem Schroeder : A <=_card B -> B <=_card A -> A =_card B.

Proof.

  intros A_inf_B B_inf_A.
  elim A_inf_B.
  intros.
  elim B_inf_A.
  intros.
  apply equipollence_intro with (h f f0).
  apply h_bij; assumption.

Qed.

End Schroeder_Bernstein.