From 340afa32ab9610421f694fa205cffa4aef0c6fe7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 16 Feb 2024 17:34:32 +0100
Subject: [PATCH] Move stuff around. Shorten some proofs. Add and prove
f_inv_id_{l,r}.
---
FEM/Compl/Function_compl.v | 27 +++++++++++++--------------
1 file changed, 13 insertions(+), 14 deletions(-)
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 5754be57..3d341988 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -530,9 +530,15 @@ Definition f_inv : T2 -> T1 := proj1_sig f_inv_EX.
Lemma f_inv_correct_l : cancel f f_inv.
Proof. apply (proj2_sig f_inv_EX). Qed.
+Lemma f_inv_id_l : f_inv \o f = id.
+Proof. apply can_equiv, f_inv_correct_l. Qed.
+
Lemma f_inv_correct_r : cancel f_inv f.
Proof. apply (proj2_sig f_inv_EX). Qed.
+Lemma f_inv_id_r : f \o f_inv = id.
+Proof. apply can_equiv, f_inv_correct_r. Qed.
+
End Inverse_Def.
@@ -543,15 +549,10 @@ Context {f : T1 -> T2}.
Hypothesis Hf : bijective f.
Lemma f_inv_uniq_l : forall (g : T2 -> T1), cancel f g -> g = f_inv Hf.
-Proof.
-intros; apply fun_ext, (bij_can_eq Hf); [easy | apply f_inv_correct_l].
-Qed.
+Proof. move=>> H; apply (bij_can_uniq_r Hf H), f_inv_correct_l. Qed.
Lemma f_inv_uniq_r : forall (g : T2 -> T1), cancel g f -> g = f_inv Hf.
-Proof.
-move=>> Hg; apply: (inj_can_uniq_l _ Hg);
- [apply bij_inj; easy | apply f_inv_correct_r].
-Qed.
+Proof. move=>> H; apply (bij_can_uniq_l Hf H), f_inv_correct_r. Qed.
Lemma f_inv_bij : bijective (f_inv Hf).
Proof. apply (bij_can_bij Hf), f_inv_correct_l. Qed.
@@ -578,8 +579,12 @@ End Inverse_Facts1.
Section Inverse_Facts2.
Context {T1 T2 : Type}.
-Context {f : T1 -> T2}.
+Context {f g : T1 -> T2}.
Hypothesis Hf : bijective f.
+Hypothesis Hg : bijective g.
+
+Lemma f_inv_ext : same_fun f g -> f_inv Hf = f_inv Hg.
+Proof. move=> /fun_ext_equiv H; subst; f_equal; apply proof_irrel. Qed.
Lemma f_inv_invol : forall (Hf1 : bijective (f_inv Hf)), f_inv Hf1 = f.
Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_correct_r. Qed.
@@ -587,12 +592,6 @@ Proof. intros; apply eq_sym, f_inv_uniq_l, f_inv_correct_r. Qed.
Lemma f_inv_invol_alt : f_inv (f_inv_bij Hf) = f.
Proof. apply f_inv_invol. Qed.
-Context {g : T1 -> T2}.
-Hypothesis Hg : bijective g.
-
-Lemma f_inv_ext : same_fun f g -> f_inv Hf = f_inv Hg.
-Proof. move=> /fun_ext_equiv H; subst; f_equal; apply proof_irrel. Qed.
-
End Inverse_Facts2.
--
GitLab