diff options
| author | Cyril Cohen | 2019-11-22 11:07:28 +0100 |
|---|---|---|
| committer | Assia Mahboubi | 2019-11-22 11:07:28 +0100 |
| commit | 6acef5bb290837871337983037833dad29606d79 (patch) | |
| tree | bc1d4a41a6050c93b3002753e035ad67383680af | |
| parent | 317267c618ecff861ec6539a2d6063cef298d720 (diff) | |
Added ssrfun theorem `inj_compr` (#432)
| -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. |