Add Cartesian product and some of its properties.

Lebesgue/Subset.v

@@ -79,10 +79,24 @@ Definition partition : Prop :=
 End Base_Def.
 
 
+Section Prod_Def.
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable A1 : U1 -> Prop. (* Subset. *)
+Variable A2 : U2 -> Prop. (* Subset. *)
+
+Definition prod : U1 * U2 -> Prop :=
+  fun x => A1 (fst x) /\ A2 (snd x).
+
+End Prod_Def.
+
+
 Ltac subset_unfold :=
   unfold emptyset, fullset,
       empty, full, incl, same, disj,
-      compl, union, inter, diff, sym_diff.
+      compl, union, inter, diff, sym_diff,
+      prod.
 
 Ltac subset_auto :=
   subset_unfold; try tauto; try easy.
@@ -1513,3 +1527,40 @@ apply partition_inter_l.
 Qed.
 
 End Partition_Facts.
+
+
+Section Prod_Facts.
+
+(** Facts about Cartesian product. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Lemma prod_fullset :
+  prod (@fullset U1) (@fullset U2) = fullset.
+Proof.
+apply subset_ext; subset_auto.
+Qed.
+
+Variable A1 B1 : U1 -> Prop. (* Subset. *)
+Variable A2 B2 : U2 -> Prop. (* Subset. *)
+
+Lemma prod_inter :
+  inter (prod A1 A2) (prod B1 B2) = prod (inter A1 B1) (inter A2 B2).
+Proof.
+apply subset_ext; subset_auto.
+Qed.
+
+Lemma prod_compl_union :
+  compl (prod A1 A2) = union (prod (compl A1) A2) (prod fullset (compl A2)).
+Proof.
+apply subset_ext; intros x; subset_auto.
+Qed.
+
+Lemma prod_compl_disj :
+  disj (prod (compl A1) A2) (prod fullset (compl A2)).
+Proof.
+subset_auto.
+Qed.
+
+End Prod_Facts.
+