Add lemmas about id.

Lebesgue/Set_theory/Set_base.v

@@ -2491,6 +2491,13 @@ Variable f : U1 -> U2.
 
 (** Facts about image. *)
 
+Lemma image_id : forall {U : Type} (A : set U), image id A = A.
+Proof.
+intros; apply set_ext_equiv; split; intros x Hx.
+induction Hx as [x Hx]; easy.
+rewrite <- id_eq; easy.
+Qed.
+
 Lemma image_empty_equiv :
   forall A1, empty (image f A1) <-> empty A1.
 Proof.

Lebesgue/Set_theory/Set_fun.v

@@ -21,7 +21,20 @@ From Coq Require Import ClassicalChoice.
 Require Import Set_def.
 
 
-Section Fun_Facts0.
+Section Fun_Facts0a.
+
+Context {U : Type}.
+
+(* Useful? *)
+Lemma id_eq: forall (x : U), id x = x.
+Proof.
+easy.
+Qed.
+
+End Fun_Facts0a.
+
+
+Section Fun_Facts0b.
 
 Context {U1 U2 : Type}.
 
@@ -53,7 +66,7 @@ Proof.
 intros f g h H1 H2 x; now rewrite (H1 x).
 Qed.
 
-End Fun_Facts0.
+End Fun_Facts0b.
 
 
 Section Fun_Facts1.
@@ -110,6 +123,7 @@ Variable f43 : U3 -> U4.
 Variable f32 : U2 -> U3.
 Variable f21 : U1 -> U2.
 
+(* Useful? *)
 Lemma compose_eq : forall (x1 : U1), compose f32 f21 x1 = f32 (f21 x1).
 Proof.
 easy.