diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrfun.v | 4 |
2 files changed, 5 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 668aeaa..dbe39cd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -92,6 +92,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `nseq_addn`, `take_take`, `take_drop`, `take_addn`, `takeC`, `take_nseq`, `drop_nseq`, `rev_nseq`, `take_iota`, `drop_iota`. +- Added ssrfun theorem `inj_compr`. ### Changed diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v index de917a9..f189dcb 100644 --- a/mathcomp/ssreflect/ssrfun.v +++ b/mathcomp/ssreflect/ssrfun.v @@ -17,3 +17,7 @@ Definition of_void T (x : void) : T := match x with end. Lemma of_voidK T : pcancel (of_void T) [fun _ => None]. Proof. by case. Qed. + +Lemma inj_compr A B C (f : B -> A) (h : C -> B) : + injective (f \o h) -> injective h. +Proof. by move=> fh_inj x y /(congr1 f) /fh_inj. Qed. |