From 3b84a638741a4892a8ed69943418fb0f5fc99f27 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Apr 2015 20:52:18 -0700
Subject: [PATCH] fix(library/algebra/function): terminology

---
 library/algebra/function.lean | 24 +++++++++++++++++++++---
 library/data/list/set.lean    |  2 +-
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index 980a932b3..7cdbcc83d 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -67,15 +67,33 @@ 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 right_inv_eq {finv : B → A} {f : A → B} (rinv : f ∘ finv = id) : ∀ x, f (finv x) = x :=
+take x, show (f ∘ finv) x = x, by rewrite rinv
 
-lemma injective_def {f : A → B} (h : injective f) : ∀ a b, f a = f b → a = b :=
-take a b, assume faeqfb,
+definition injective (f : A → B) : Prop := ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂
+
+definition surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b
+
+definition has_left_inverse (f : A → B) : Prop := ∃ finv : B → A, finv ∘ f = id
+
+definition has_right_inverse (f : A → B) : Prop := ∃ finv : B → A, f ∘ finv = id
+
+lemma injective_of_has_left_inverse {f : A → B} : has_left_inverse f → injective f :=
+assume h, 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)
 
+lemma surjective_of_has_right_inverse {f : A → B} : has_right_inverse f → surjective f :=
+assume h, take b,
+obtain (finv : B → A) (inv : f ∘ finv = id), from h,
+let  a : A := finv b in
+have h : f a = b, from calc
+  f a  = (f ∘ finv) b : rfl
+   ... = id b         : by rewrite (right_inv_eq inv)
+   ... = b            : rfl,
+exists.intro a h
 end function
 
 -- copy reducible annotations to top-level
diff --git a/library/data/list/set.lean b/library/data/list/set.lean
index d3177ef1e..3a3f9cb42 100644
--- a/library/data/list/set.lean
+++ b/library/data/list/set.lean
@@ -277,7 +277,7 @@ have d₄    : nodup (a::l₂),       from nodup_cons nain₂ d₃,
 have disj₂ : disjoint l₁ (a::l₂), from disjoint.comm (disjoint_cons_of_not_mem_of_disjoint nain₁ (disjoint.comm disj)),
 nodup_append_of_nodup_of_nodup_of_disjoint d₂ d₄ disj₂
 
-theorem nodup_map {f : A → B} (inj : injective f) : ∀ {l : list A}, nodup l → nodup (map f l)
+theorem nodup_map {f : A → B} (inj : has_left_inverse f) : ∀ {l : list A}, nodup l → nodup (map f l)
 | []      n := begin rewrite [map_nil], apply nodup_nil end
 | (x::xs) n :=
   assert nxinxs : x ∉ xs,           from not_mem_of_nodup_cons n,