From 3b0f666646f30202a9e434ccafcb927b3dc60324 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Apr 2015 15:43:44 -0700
Subject: [PATCH] feat(library/algebra/function): define injective

---
 library/algebra/function.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index f76509f20..7e9ff6cd9 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -46,6 +46,18 @@ infixl  on                 := on_fun
 infixr  $                  := app
 notation f `-[` op `]-` g  := combine f op g
 
+lemma left_inv_eq {finv : B → A} {f : A → B} (linv : finv ∘ f = id) : ∀ x, finv (f x) = x :=
+take x, show (finv ∘ f) x = x, by rewrite linv
+
+definition injective (f : A → B) : Prop := ∃ finv : B → A, finv ∘ f = id
+
+lemma injective_def {f : A → B} (h : injective f) : ∀ a b, f a = f b → a = b :=
+take a b, assume faeqfb,
+obtain (finv : B → A) (inv : finv ∘ f = id), from h,
+calc a = finv (f a) : by rewrite (left_inv_eq inv)
+   ... = finv (f b) : faeqfb
+   ... = b          : by rewrite (left_inv_eq inv)
+
 end function
 
 -- copy reducible annotations to top-level