From 4239945f4d1efe16a9cf039601e33b0c0277ba49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 29 Mar 2022 18:14:00 +0200
Subject: [PATCH] Proofs of facts about compose.

---
 Lebesgue/Subset.v | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index f89a21e1..53423818 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -2071,19 +2071,27 @@ Variable f12 : U1 -> U2. (* Function. *)
 Variable f23 : U2 -> U3. (* Function. *)
 Variable f34 : U3 -> U4. (* Function. *)
 
+(* Useful? *)
 Lemma compose_assoc :
   compose f34 (compose f23 f12) = compose (compose f34 f23) f12.
 Proof.
-Admitted.
+easy.
+Qed.
 
 Lemma image_compose :
   forall A1, image (compose f23 f12) A1 = image f23 (image f12 A1).
 Proof.
-Admitted.
+intros A1; apply subset_ext_equiv; split; intros x3 Hx3.
+induction Hx3 as [x1 Hx1]; easy.
+induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
+replace (f23 (f12 x1)) with (compose f23 f12 x1); easy.
+Qed.
 
+(* Useful? *)
 Lemma preimage_compose :
   forall A3, preimage (compose f23 f12) A3 = preimage f12 (preimage f23 A3).
 Proof.
-Admitted.
+easy.
+Qed.
 
 End Compose_Facts.
-- 
GitLab