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.