new mem_imset lemmas

2 files changed, 18 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index d6662b4..4a3eaf1 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -1249,6 +1249,11 @@ Qed.
 Lemma imset_f (D : {pred aT}) x : x \in D -> f x \in f @: D.
 Proof. by move=> Dx; apply/imsetP; exists x. Qed.
 
+Lemma mem_imset_eq (D : {pred aT}) x : injective f -> f x \in f @: D = (x \in D).
+Proof.
+by move=> f_inj; apply/imsetP/idP;[case=> [y] ? /f_inj -> | move=> ?; exists x].
+Qed.
+
 Lemma imset0 : f @: set0 = set0.
 Proof. by apply/setP => y; rewrite inE; apply/imsetP=> [[x]]; rewrite inE. Qed.
 
@@ -1269,6 +1274,14 @@ Lemma imset2_f (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 :
   f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)).
 Proof. by move=> Dx Dx2; apply/imset2P; exists x x2. Qed.
 
+Lemma mem_imset2_eq (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 :
+    injective2 f2 ->
+  f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)) = ((x \in D) && (x2 \in D2 x)).
+Proof.
+move=> inj2_f; apply/imset2P/andP => [|[xD xD2]]; last by exists x x2.
+by move => [x' x2' xD xD2 eq_f2]; case: (inj2_f _ _ _ _ eq_f2) => -> ->.
+Qed.
+
 Lemma sub_imset_pre (A : {pred aT}) (B : {pred rT}) :
   (f @: A \subset B) = (A \subset f @^-1: B).
 Proof.
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.