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 /mathcomp | |
| parent | 317267c618ecff861ec6539a2d6063cef298d720 (diff) | |
Added ssrfun theorem `inj_compr` (#432)
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrfun.v | 4 |
1 files changed, 4 insertions, 0 deletions
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. |