Library SCHROEDER.Schroeder

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.

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

Variable U : Type.

Let SU := Ensemble U.

Variable A B : SU.
  Section Bijection.

  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.

    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.

      Lemma F_croissante :
       forall C C' : SU, Included U C C' -> Included U (F C) (F C').
        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.

         Lemma J_dans_FJ : Included U J (F J).
           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_croissante.
             apply Set_Sum_is_minoring.
             assumption.
         Qed.

         Lemma FJ_dans_J : Included U (F J) J.
           unfold J in |- *.
           apply Set_Sum_is_minoring.
           red in |- *.
           red in |- *.
           apply F_croissante.
           exact J_dans_FJ.
         Qed.

    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.

    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.

    Lemma h2 : au_plus_une_im 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 au_plus_une_im 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_dans_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_dans_FJ.

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

    Qed.

    Lemma h3 : au_moins_une_im 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 au_moins_une_im 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_dans_J.
          red in |- *; red in |- *; red in |- *.
          split; assumption.
        assumption.

    Qed.

    Lemma h4 : au_plus_un_ant 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.

    Lemma h5 : au_moins_un_ant 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 au_moins_une_im 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.

        Resume h_bij.
    Proof bijection_intro U A B h h1 h2 h3 h4 h5.

  End Bijection.

Theorem Schroeder : inf_card U A B -> inf_card U B A -> equipollence U A B.

  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.