diff options
| author | Anton Trunov | 2019-11-14 17:58:19 +0300 |
|---|---|---|
| committer | Assia Mahboubi | 2019-11-14 15:58:19 +0100 |
| commit | 45940df1c68ba8b4546c5ae0c7e464505a7f0ad6 (patch) | |
| tree | 82a5f0851364189b3a28daefeb4155a2cdc94442 /mathcomp | |
| parent | 03dc3079d231817a99cb896c3cd264792c568514 (diff) | |
fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403)
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 70536dc..671bb95 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -543,9 +543,6 @@ Lemma f_finv : cancel finv f. Proof. exact: (in1T (f_finv_in _ (in2W _))). Qed. Lemma finv_f : cancel f finv. Proof. exact: (in1T (finv_f_in _ (in2W _))). Qed. -Lemma fin_inj_bij : bijective f. -Proof. by exists finv; [apply: finv_f|apply: f_finv]. Qed. - Lemma finv_bij : bijective finv. Proof. by exists f; [apply: f_finv|apply: finv_f]. Qed. @@ -643,7 +640,7 @@ Variables (T : finType) (f f' : T -> T). Lemma finv_eq_can : cancel f f' -> finv f =1 f'. Proof. move=> fK; have inj_f := can_inj fK. -by apply: bij_can_eq fK; [apply: fin_inj_bij | apply: finv_f]. +by apply: bij_can_eq fK; [apply: injF_bij | apply: finv_f]. Qed. Hypothesis eq_f : f =1 f'. |