Library Coqtail.Sets.Cartesian_product

Require Export Ensembles.
Require Export My_Finite_sets_facts.

Section Sets.

Variable U V: Type.

Definition Product (B:Ensemble U) (C:Ensemble V) : Ensemble(U×V) :=
fun (u:U×V) ⇒ let (x,y):=u in B x ∧ C y.

End Sets.