diff options
| author | Christian Doczkal | 2020-09-10 18:30:42 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-09-29 11:10:31 +0200 |
| commit | 94e1bf37bbdabe3f2cf300e60a8c4eb856aa4819 (patch) | |
| tree | 8e7872c008b95319b483ec82c181f0b194038bd3 /mathcomp/ssreflect/ssrfun.v | |
| parent | 5b31a9e767694ce134fdff4461a876411eba0f2d (diff) | |
new mem_imset lemmas
Diffstat (limited to 'mathcomp/ssreflect/ssrfun.v')
| -rw-r--r-- | mathcomp/ssreflect/ssrfun.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v index f189dcb..c789e67 100644 --- a/mathcomp/ssreflect/ssrfun.v +++ b/mathcomp/ssreflect/ssrfun.v @@ -21,3 +21,8 @@ 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. + +Definition injective2 (rT aT1 aT2 : Type) (f : aT1 -> aT2 -> rT) := + forall (x1 x2 : aT1) (y1 y2 : aT2), f x1 y1 = f x2 y2 -> (x1 = x2) * (y1 = y2). + +Arguments injective2 [rT aT1 aT2] f. |