From 32b07c45610de005ed8908fc1b409feda99e5770 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Apr 2015 17:14:10 -0700
Subject: [PATCH] feat(library/data/finset): define map for finset

---
 library/data/finset/comb.lean    | 25 +++++++++++++++++++++++++
 library/data/finset/default.lean |  2 +-
 2 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 library/data/finset/comb.lean

diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
new file mode 100644
index 0000000000..7c3c205cda
--- /dev/null
+++ b/library/data/finset/comb.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.finset
+Author: Leonardo de Moura
+
+Combinators for finite sets
+-/
+import data.finset.basic
+open list quot subtype decidable perm function
+
+namespace finset
+variables {A B : Type}
+variable [h : decidable_eq B]
+include h
+
+definition map (f : A → B) (s : finset A) : finset B :=
+quot.lift_on s
+  (λ l, to_finset (list.map f (elt_of l)))
+  (λ l₁ l₂ p, quot.sound (perm_erase_dup_of_perm (perm_map _ p)))
+
+theorem map_empty (f : A → B) : map f ∅ = ∅ :=
+rfl
+end finset
diff --git a/library/data/finset/default.lean b/library/data/finset/default.lean
index 34546d3463..346185b86b 100644
--- a/library/data/finset/default.lean
+++ b/library/data/finset/default.lean
@@ -7,4 +7,4 @@ Author: Leonardo de Moura
 
 Finite sets
 -/
-import data.finset.basic data.finset.bigop
+import data.finset.basic data.finset.comb data.finset.bigop