Library SCHROEDER.Equipollence
Require Import Ensembles.
Require Import Relations_1.
Require Import Functions.
Section Equipollence.
Variable U : Type.
Variable A B : Ensemble U.
Let Rela := Relation U.
Inductive equipollence : Prop :=
equipollence_intro : forall f : Rela, bijection U A B f -> equipollence.
Inductive inf_card : Prop :=
inf_card_intro : forall f : Rela, injection U A B f -> inf_card.
End Equipollence.