Function_compl:

Move stuff around.
Add and prove Rg_ext, surj_ext, surj_comp_{compat,reg}.

Function_sub:
Add and prove surjS_id, surjS_has_right_inv.

FEM/Compl/Function_compl.v

@@ -272,7 +272,6 @@ Section Range_Facts.
 
 Context {T1 T2 T3 : Type}.
 Context {f : T1 -> T2}.
-Context {g : T2 -> T3}.
 
 Lemma Rg_correct : forall {x2} x1, f x1 = x2 -> Rg f x2.
 Proof. move=> x2 x1 <-; easy. Qed.
@@ -280,6 +279,9 @@ Proof. move=> x2 x1 <-; easy. Qed.
 Lemma Rg_ex : forall {x2}, Rg f x2 <-> exists x1, f x1 = x2.
 Proof. intros; split; [intros [x1 _]; exists x1 | move=> [x1 <-]]; easy. Qed.
 
+Lemma Rg_ext : forall (g : T1 -> T2), same_fun f g -> Rg f = Rg g.
+Proof. move=> g /fun_ext ->; easy. Qed.
+
 Lemma Rg_compl : forall {x2}, ~ Rg f x2 <-> forall x1, f x1 <> x2.
 Proof. intros; rewrite -iff_not_r_equiv not_all_not_ex_equiv; apply Rg_ex. Qed.
 
@@ -289,9 +291,9 @@ Proof. split; intros Hf; [rewrite Hf | apply subset_ext_equiv]; easy. Qed.
 Lemma preimage_Rg : preimage f (Rg f) = fullset.
 Proof. apply preimage_of_image_full. Qed.
 
-Lemma Rg_comp : Rg (g \o f) = image g (Rg f).
+Lemma Rg_comp : forall {g : T2 -> T3}, Rg (g \o f) = image g (Rg f).
 Proof.
-apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
+intros; apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
 intros _ [_ [x1 _]]; apply: Im; easy.
 Qed.
 
@@ -323,17 +325,6 @@ Lemma inj_ext :
   forall {g : T1 -> T2}, same_fun f g -> injective f -> injective g.
 Proof. move=>> H Hf; apply (eq_inj Hf H). Qed.
 
-Lemma inj_has_left_inv : inhabited T1 -> injective f <-> exists g, cancel f g.
-Proof.
-intros [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
-exists (fun x2 => match im_dec f x2 with
-  | inleft H1 => proj1_sig H1
-  | inright _ => a1
-  end).
-intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1];
-    [apply Hf | contradict H1; rewrite not_all_not_ex_equiv; exists x1]; easy.
-Qed.
-
 Lemma inj_comp_compat :
   forall {g : T2 -> T3}, injective f -> injective g -> injective (g \o f).
 Proof. intros; apply inj_comp; easy. Qed.
@@ -346,7 +337,7 @@ End Inj_Facts.
 
 Section Surj_Facts.
 
-Context {T1 T2 : Type}.
+Context {T1 T2 T3 : Type}.
 Context {f : T1 -> T2}.
 
 Lemma surj_correct : incl fullset (Rg f) -> surjective f.
@@ -366,6 +357,24 @@ Qed.
 Lemma surj_equiv_alt : surjective f <-> incl fullset (Rg f).
 Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.
 
+Lemma surj_ext :
+  forall {g : T1 -> T2}, same_fun f g -> surjective f -> surjective g.
+Proof.
+move=>> H Hf; intros x2; destruct (Hf x2) as [x1 Hx1];
+    exists x1; rewrite -H; easy.
+Qed.
+
+Lemma surj_comp_compat :
+  forall {g : T2 -> T3}, surjective f -> surjective g -> surjective (g \o f).
+Proof.
+intros g Hf Hg x3; destruct (Hg x3) as [x2 Hx2], (Hf x2) as [x1 Hx1].
+exists x1; rewrite -Hx2 -Hx1; easy.
+Qed.
+
+Lemma surj_comp_reg :
+  forall (g : T2 -> T3), surjective (g \o f) -> surjective g.
+Proof. intros g H x3; destruct (H x3) as [x1 Hx1]; exists (f x1); easy. Qed.
+
 Lemma surj_id : forall {T : Type}, surjective (id : T -> T).
 Proof. intros T x; exists x; easy. Qed.
 
@@ -399,6 +408,17 @@ Lemma inj_can_uniq_l :
   forall {g h : T2 -> T1}, injective f -> cancel g f -> cancel h f -> g = h.
 Proof. move=>> Hf Hg Hh; apply fun_ext, (inj_can_eq Hg Hf Hh). Qed.
 
+Lemma inj_has_left_inv : inhabited T1 -> injective f <-> exists g, cancel f g.
+Proof.
+intros [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
+exists (fun x2 => match im_dec f x2 with
+  | inleft H1 => proj1_sig H1
+  | inright _ => a1
+  end).
+intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1];
+    [apply Hf | contradict H1; rewrite not_all_not_ex_equiv; exists x1]; easy.
+Qed.
+
 Lemma surj_can_uniq_r :
   forall {g h : T2 -> T1}, surjective f -> cancel f g -> cancel f h -> g = h.
 Proof.
@@ -408,7 +428,7 @@ Qed.
 
 Lemma surj_has_right_inv : surjective f <-> exists g, cancel g f.
 Proof.
-apply iff_sym; split; [intros [g Hg]; apply: can_surj Hg |].
+split; [| intros [g Hg]; apply: can_surj Hg].
 intros Hf; destruct (choice _ Hf) as [g Hg]; exists g; easy.
 Qed.
 

FEM/Compl/Function_sub.v

@@ -426,35 +426,23 @@ Context {P1 : T1 -> Prop}.
 Variable P2 : T2 -> Prop.
 
 Context {f : T1 -> T2}.
-Context {g : T2 -> T3}.
 
 Lemma injS_comp_compat :
-  funS P1 P2 f -> injS P1 f -> injS P2 g -> injS P1 (g \o f).
+  forall {g : T2 -> T3},
+    funS P1 P2 f -> injS P1 f -> injS P2 g -> injS P1 (g \o f).
 Proof.
-intros Hf0 Hf Hg x1 y1 Hx1 Hy1 H1; apply Hf, Hg; try apply Hf0; easy.
+intros g Hf0 Hf Hg x1 y1 Hx1 Hy1 H1; apply Hf, Hg; try apply Hf0; easy.
 Qed.
 
-End InjS_Facts5.
-
-
-Section InjS_Facts6.
-
-Context {T1 T2 T3 : Type}.
-
-Context {P1 : T1 -> Prop}.
-
-Context {f : T1 -> T2}.
-Variable g : T2 -> T3.
-
-Lemma injS_comp_reg : injS P1 (g \o f) -> injS P1 f.
+Lemma injS_comp_reg : forall (g : T2 -> T3), injS P1 (g \o f) -> injS P1 f.
 Proof.
-intros H x1 y1 Hx1 Hy1 H1; apply H; try rewrite comp_correct H1; easy.
+intros g H x1 y1 Hx1 Hy1 H1; apply H; try rewrite comp_correct H1; easy.
 Qed.
 
-End InjS_Facts6.
+End InjS_Facts5.
 
 
-Section InjS_Facts7.
+Section InjS_Facts6.
 
 Context {T1 T2 T3 : Type}.
 
@@ -471,7 +459,21 @@ Proof.
 move=> Hg Hh Hf H x1 Hx1; apply Hf, H; [apply Hg | apply Hh |]; easy.
 Qed.
 
-End InjS_Facts7.
+End InjS_Facts6.
+
+
+Section SurjS_Facts1.
+
+Context {T : Type}.
+
+Context {P : T -> Prop}.
+
+Context {f : T -> T}.
+
+Lemma surjS_id : same_funS P f (id : T -> T) -> surjS P P f.
+Proof. intros Hf y Hy; exists y; auto. Qed.
+
+End SurjS_Facts1.
 
 
 Section SurjS_Facts1.
@@ -662,6 +664,7 @@ Section CanS_Facts3.
 Context {T1 T2 : Type}.
 
 Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
 
 Context {f : T1 -> T2}.
 
@@ -681,28 +684,30 @@ contradict H1; rewrite not_all_ex_not_equiv;
     exists y1; rewrite not_imp_not_r_and_equiv; easy.
 Qed.
 
-End CanS_Facts3.
-
-
-Section CanS_Facts4.
-
-Context {T1 T2 : Type}.
-
-Context {P1 : T1 -> Prop}.
-Context {P2 : T2 -> Prop}.
-
-Context {f : T1 -> T2}.
-Variable g : T2 -> T1.
+Lemma canS_surjS :
+  forall (g : T2 -> T1), funS P2 P1 g -> canS P2 g f -> surjS P1 P2 f.
+Proof.
+intros g Hg H x2 Hx2; exists (g x2); split; [apply Hg | rewrite H]; easy.
+Qed.
 
-Lemma canS_surjS : funS P2 P1 g -> canS P2 g f -> surjS P1 P2 f.
+Lemma surjS_has_right_inv :
+  inhabited T1 -> surjS P1 P2 f <-> exists g, funS P2 P1 g /\ canS P2 g f.
 Proof.
-intros Hg H x2 Hx2; exists (g x2); split; [apply Hg | rewrite H]; easy.
+intros [a1]; split; [| intros [g Hg]; apply (canS_surjS g); easy].
+intros Hf; exists (fun x2 => match imS_dec P1 f x2 with
+  | inleft H1 => proj1_sig H1
+  | inright _ => a1
+  end); split; [intros y1 [x2 Hx2] | intros x2 Hx2];
+    (destruct (imS_dec P1 f x2) as [[x1 Hx1] | H1]; [easy |]).
+1,2: contradict H1; rewrite not_all_ex_not_equiv;
+    destruct (Hf _ Hx2) as [x1 Hx1];
+    exists x1; rewrite not_imp_not_r_and_equiv; easy.
 Qed.
 
-End CanS_Facts4.
+End CanS_Facts3.
 
 
-Section CanS_Facts5.
+Section CanS_Facts4.
 
 Context {T1 T2 : Type}.
 
@@ -719,10 +724,10 @@ intros H1 H2 H3 H4 x2 Hx2;
     apply H3; [apply H1, Im | easy | rewrite H4//]; apply H2; easy.
 Qed.
 
-End CanS_Facts5.
+End CanS_Facts4.
 
 
-Section CanS_Facts6.
+Section CanS_Facts5.
 
 Context {T1 T2 T3 : Type}.
 
@@ -741,7 +746,7 @@ Proof.
 move=> /funS_equiv H1 H2 H3 x1 Hx1; rewrite -> !comp_correct, H3, H2; auto.
 Qed.
 
-End CanS_Facts6.
+End CanS_Facts5.
 
 
 Section BijS_Facts1.