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.