From a711467887109376f37e4f85c0d25a2a5eb15dbc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 20 Jun 2022 09:01:46 +0200
Subject: [PATCH] Change variables order. Add compose_eq and compose_id_{l,r}.
---
Lebesgue/Set_theory/Set_fun.v | 25 +++++++++++++++++++++----
1 file changed, 21 insertions(+), 4 deletions(-)
diff --git a/Lebesgue/Set_theory/Set_fun.v b/Lebesgue/Set_theory/Set_fun.v
index c7c00b24..52cf017c 100644
--- a/Lebesgue/Set_theory/Set_fun.v
+++ b/Lebesgue/Set_theory/Set_fun.v
@@ -106,19 +106,36 @@ Section Fun_Facts2.
(** Facts about composition of functions. *)
Context {U1 U2 U3 U4 : Type}.
-Variable f21 : U1 -> U2.
-Variable f32 : U2 -> U3.
Variable f43 : U3 -> U4.
+Variable f32 : U2 -> U3.
+Variable f21 : U1 -> U2.
+
+Lemma compose_eq : forall (x1 : U1), compose f32 f21 x1 = f32 (f21 x1).
+Proof.
+easy.
+Qed.
(* Useful? *)
Lemma compose_assoc :
compose3 f43 f32 f21 = compose (compose f43 f32) f21.
-Proof
+Proof.
+easy.
+Qed.
+
+(* Useful? *)
+Lemma compose_id_l : compose id f21 = f21.
+Proof.
+easy.
+Qed.
+
+(* Useful? *)
+Lemma compose_id_r : compose f32 id = f32.
+Proof.
easy.
Qed.
Lemma image_compose_fun :
- image (compose f32 f11) = fun A1 => image f32 (image f21 A1).
+ image (compose f32 f21) = fun A1 => image f32 (image f21 A1).
Proof.
apply fun_ext; intros A1; apply set_ext_equiv; split; intros x3 Hx3.
induction Hx3 as [x1 Hx1]; easy.
--
GitLab