From ec6c4d83399b5d5d17166f1e7c46dd0eb0d1e977 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 10 Nov 2016 16:25:00 -0500
Subject: [PATCH] image_incl_eq_one

---
 algebra/subgroup.hlean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 1ed07ee..a018646 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -308,4 +308,18 @@ namespace group
     reflexivity
   end
 
+  definition image_incl_injective {G H : Group} (f : G →g H) : Π (x y : image f), (image_incl f x = image_incl f y) → (x = y) :=
+  begin
+    intro x y,
+    intro p,
+    fapply subtype_eq,
+    exact p
+  end 
+
+  definition image_incl_eq_one {G H : Group} (f : G →g H) : Π (x : image f), (image_incl f x = 1) → x = 1 :=
+  begin
+    intro x,
+    fapply image_incl_injective f x 1,
+  end
+
 end group