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 | |
| parent | 03dc3079d231817a99cb896c3cd264792c568514 (diff) | |
fingraph: remove fin_inj_bij lemma as duplicate of injF_bij from fintype (#403)
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 5 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 5 |
2 files changed, 6 insertions, 4 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0744c7c..28d1b5c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -114,6 +114,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `ssrnat.mc_1_9` module. One may compile proofs compatible with the version 1.9 in newer versions by using this module. +### Removed + +- `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma + from `fintype` library. + ### Infrastructure - `Makefile` now supports the `test-suite` and `only` targets. Currently, 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'. |