Add equivalence binary relation same_fun.

Add extensionality results on (pre)image.

Lebesgue/Subset.v

@@ -136,7 +136,10 @@ Section Base_Def5.
 
 Context {U1 U2 : Type}. (* Universes. *)
 
-Variable f : U1 -> U2. (* Function. *)
+Variable f g : U1 -> U2. (* Function. *)
+
+Definition same_fun : Prop := forall x, f x = g x.
+
 Variable A1 : U1 -> Prop. (* Subset. *)
 Variable A2 : U2 -> Prop. (* Subset. *)
 
@@ -183,7 +186,7 @@ End Prop_Facts0.
 
 Ltac subset_unfold :=
   repeat unfold
-    partition, disj, same, incl, full, nonempty, empty, (* Predicates. *)
+    same_fun, partition, disj, same, incl, full, nonempty, empty, (* Predicates. *)
     preimage, image, pair, (* Constructors. *)
     swap, prod, sym_diff, diff, add, inter, union, compl, (* Operators. *)
     singleton, Prop_cst, fullset, emptyset. (* Constructors. *)
@@ -390,6 +393,34 @@ apply empty_emptyset; intros x Hx; apply (H2 x); auto.
 now rewrite H2.
 Qed.
 
+(** Facts about same_fun. *)
+
+(** It is an equivalence binary relation. *)
+
+Context {V : Type}. (* Universe. *)
+
+(* Useless?
+Lemma same_fun_refl :
+  forall (f : U -> V),
+    same_fun f f.
+Proof.
+easy.
+Qed.*)
+
+Lemma same_fun_sym :
+  forall (f g : U -> V),
+    same_fun f g -> same_fun g f.
+Proof.
+easy.
+Qed.
+
+Lemma same_fun_trans :
+  forall (f g h : U -> V),
+    same_fun f g -> same_fun g h -> same_fun f h.
+Proof.
+intros f g h H1 H2 x; now rewrite (H1 x).
+Qed.
+
 End Prop_Facts.
 
 
@@ -1808,7 +1839,20 @@ Section Image_Facts.
 
 Context {U1 U2 : Type}. (* Universes. *)
 
-Variable f : U1 -> U2. (* Function. *)
+Variable f g : U1 -> U2. (* Functions. *)
+
+Lemma image_ext_fun : forall A1, same_fun f g -> image f A1 = image g A1.
+Proof.
+intros; subset_ext_auto x2 Hx2; destruct Hx2 as [x1 Hx1];
+    exists x1; rewrite (proj2 Hx1); easy.
+Qed.
+
+Lemma image_ext : forall A1 B1, same A1 B1 -> image f A1 = image f B1.
+Proof.
+intros A1 B1 H.
+subset_ext_auto x2 Hx2; destruct Hx2 as [x1 Hx1]; exists x1; split; try easy;
+    [rewrite <- (H x1) | rewrite (H x1)]; easy.
+Qed.
 
 Lemma image_empty_equiv :
   forall A1, empty (image f A1) <-> empty A1.
@@ -1879,7 +1923,17 @@ Section Preimage_Facts.
 
 Context {U1 U2 : Type}. (* Universes. *)
 
-Variable f : U1 -> U2. (* Function. *)
+Variable f g : U1 -> U2. (* Functions. *)
+
+Lemma preimage_ext_fun : forall A2, same_fun f g -> preimage f A2 = preimage g A2.
+Proof.
+intros A2 H; subset_ext_auto x1; rewrite (H x1); easy.
+Qed.
+
+Lemma preimage_ext : forall A2 B2, same A2 B2 -> preimage f A2 = preimage f B2.
+Proof.
+intros; subset_ext_auto.
+Qed.
 
 Lemma preimage_empty_equiv :
   forall A2, empty (preimage f A2) <-> disj A2 (image f fullset).