Rename function idents in compose statements for smoother reading.

Lebesgue/Set_theory/Set_def_fun_base.v

@@ -40,10 +40,10 @@ End Fun_Base_Def1.
 Section Fun_Base_Def2a.
 
 Context {U1 U2 U3 : Type}. (* Universes. *)
-Variable f23 : U2 -> U3.
-Variable f12 : U1 -> U2.
+Variable f32 : U2 -> U3.
+Variable f21 : U1 -> U2.
 
-Definition compose : U1 -> U3 := fun x1 => f23 (f12 x1).
+Definition compose : U1 -> U3 := fun x1 => f32 (f21 x1).
 
 End Fun_Base_Def2a.
 
@@ -51,11 +51,11 @@ End Fun_Base_Def2a.
 Section Fun_Base_Def2b.
 
 Context {U1 U2 U3 U4 : Type}. (* Universes. *)
-Variable f34 : U3 -> U4.
-Variable f23 : U2 -> U3.
-Variable f12 : U1 -> U2.
+Variable f43 : U3 -> U4.
+Variable f32 : U2 -> U3.
+Variable f21 : U1 -> U2.
 
-Definition compose3 : U1 -> U4 := compose f34 (compose f23 f12).
+Definition compose3 : U1 -> U4 := compose f43 (compose f32 f21).
 
 End Fun_Base_Def2b.
 

Lebesgue/Set_theory/Set_fun.v

@@ -106,41 +106,41 @@ Section Fun_Facts2.
 (** Facts about composition of functions. *)
 
 Context {U1 U2 U3 U4 : Type}.
-Variable f12 : U1 -> U2.
-Variable f23 : U2 -> U3.
-Variable f34 : U3 -> U4.
+Variable f21 : U1 -> U2.
+Variable f32 : U2 -> U3.
+Variable f43 : U3 -> U4.
 
 (* Useful? *)
 Lemma compose_assoc :
-  compose3 f34 f23 f12 = compose (compose f34 f23) f12.
-Proof.
+  compose3 f43 f32 f21 = compose (compose f43 f32) f21.
+Proof
 easy.
 Qed.
 
 Lemma image_compose_fun :
-  image (compose f23 f12) = fun A1 => image f23 (image f12 A1).
+  image (compose f32 f11) = 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.
 induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
-replace (f23 (f12 x1)) with (compose f23 f12 x1); easy.
+replace (f32 (f21 x1)) with (compose f32 f21 x1); easy.
 Qed.
 
 Lemma image_compose :
-  forall A1, image (compose f23 f12) A1 = image f23 (image f12 A1).
+  forall A1, image (compose f32 f21) A1 = image f32 (image f21 A1).
 Proof.
 rewrite image_compose_fun; easy.
 Qed.
 
 (* Useful? *)
 Lemma preimage_compose_fun :
-  preimage (compose f23 f12) = fun A3 => preimage f12 (preimage f23 A3).
+  preimage (compose f32 f21) = fun A3 => preimage f21 (preimage f32 A3).
 Proof.
 easy.
 Qed.
 
 Lemma preimage_compose :
-  forall A3, preimage (compose f23 f12) A3 = preimage f12 (preimage f23 A3).
+  forall A3, preimage (compose f32 f21) A3 = preimage f21 (preimage f32 A3).
 Proof.
 easy.
 Qed.

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -451,22 +451,22 @@ End Image_Preimage_Facts1.
 Section Image_Preimage_Facts2.
 
 Context {U1 U2 U3 : Type}.
-Variable f12 : U1 -> U2.
-Variable f23 : U2 -> U3.
+Variable f21 : U1 -> U2.
+Variable f32 : U2 -> U3.
 
 Lemma Image_compose :
-  forall P1, Image (compose f23 f12) P1 = Image f23 (Image f12 P1).
+  forall P1, Image (compose f32 f21) P1 = Image f32 (Image f21 P1).
 Proof.
 intros; unfold Image; set_unfold; easy.
 Qed.
 
 Lemma Preimage_compose :
-  forall P3, Preimage (compose f23 f12) P3 = Preimage f12 (Preimage f23 P3).
+  forall P3, Preimage (compose f32 f21) P3 = Preimage f21 (Preimage f32 P3).
 Proof.
 intros P3; unfold Preimage; set_ext_auto A1 HA1; induction HA1 as [A3 HA3].
 rewrite preimage_compose; repeat apply Im; easy.
 induction HA3 as [A3 HA3]; unfold preimagep_any; rewrite preimage_compose_fun.
-apply Im with (f := fun A => preimage f12 (preimage f23 A)); easy.
+apply Im with (f := fun A => preimage f21 (preimage f32 A)); easy.
 Qed.
 
 End Image_Preimage_Facts2.