feat(library/data/set,finset): finish porting properties of card to sets

library/data/finset/card.lean

@@ -170,6 +170,21 @@ have H : card s₁ + 0 = card s₁ + card (s₂ \ s₁),
 assert H1 : s₂ \ s₁ = ∅, from eq_empty_of_card_eq_zero (add.left_cancel H)⁻¹,
 by rewrite [-union_diff_cancel Hsub, H1, union_empty]
 
+lemma exists_two_of_card_gt_one {s : finset A} : 1 < card s → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
+begin
+  intro h,
+  induction s with a s nain ih₁,
+   {exact absurd h dec_trivial},
+   {induction s with b s nbin ih₂,
+    {exact absurd h dec_trivial},
+     clear ih₁ ih₂,
+     existsi a, existsi b, split,
+      {apply mem_insert},
+      split,
+      {apply mem_insert_of_mem _ !mem_insert},
+      {intro aeqb, subst a, exact absurd !mem_insert nain}}
+end
+
 theorem Sum_const_eq_card_mul (s : finset A) (n : nat) : (∑ x ∈ s, n) = card s * n :=
 begin
   induction s with a s' H IH,
@@ -209,21 +224,6 @@ finset.induction_on s
                 card_union_of_disjoint H8, H6])
 end deceqB
 
-lemma exists_two_of_card_gt_one {s : finset A} : 1 < card s → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
-begin
-  intro h,
-  induction s with a s nain ih₁,
-   {exact absurd h dec_trivial},
-   {induction s with b s nbin ih₂,
-    {exact absurd h dec_trivial},
-     clear ih₁ ih₂,
-     existsi a, existsi b, split,
-      {apply mem_insert},
-      split,
-      {apply mem_insert_of_mem _ !mem_insert},
-      {intro aeqb, subst a, exact absurd !mem_insert nain}}
-end
-
 lemma dvd_Sum_of_dvd (f : A → nat) (n : nat) (s : finset A) : (∀ a, a ∈ s → n ∣ f a) → n ∣ Sum s f :=
 begin
   induction s with a s nain ih,

library/data/finset/to_set.lean

@@ -94,4 +94,10 @@ definition decidable_bounded_exists (s : finset A) (p : A → Prop) [h : decidab
   decidable (∃₀ x ∈ ts s, p x) :=
 decidable_of_decidable_of_iff _ !any_iff_exists
 
+/- properties -/
+
+theorem inj_on_to_set {B : Type} [h : decidable_eq B] (f : A → B) (s : finset A) :
+  inj_on f s = inj_on f (ts s) :=
+rfl
+
 end finset

library/data/set/finite.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 
@@ -211,12 +211,12 @@ by rewrite [card_insert_of_not_mem !not_mem_empty, card_empty]
 /- Note: the induction tactic does not work well with the set induction principle with the
    extra predicate "finite". -/
 theorem eq_empty_of_card_eq_zero {s : set A} [fins : finite s] : card s = 0 → s = ∅ :=
-induction_on_finite s 
+induction_on_finite s
   (by intro H; exact rfl)
   (begin
     intro a s' fins' anins IH H,
     rewrite (card_insert_of_not_mem anins) at H,
-    apply nat.no_confusion H 
+    apply nat.no_confusion H
   end)
 
 theorem card_upto (n : ℕ) : card {i | i < n} = n :=
@@ -230,7 +230,7 @@ begin
   apply finset.card_add_card
 end
 
-theorem card_union (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] : 
+theorem card_union (s₁ s₂ : set A) [fins₁ : finite s₁] [fins₂ : finite s₂] :
   card (s₁ ∪ s₂) = card s₁ + card s₂ - card (s₁ ∩ s₂) :=
 calc
   card (s₁ ∪ s₂) = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) - card (s₁ ∩ s₂) : add_sub_cancel
@@ -249,10 +249,68 @@ calc
   card s₂ = card (s₁ ∪ (s₂ \ s₁))    : {this}
       ... = card s₁ + card (s₂ \ s₁) : card_union_of_disjoint H1
 
-theorem card_le_card_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) : 
+theorem card_le_card_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂] (H : s₁ ⊆ s₂) :
   card s₁ ≤ card s₂ :=
 calc
   card s₂ = card s₁ + card (s₂ \ s₁) : card_eq_card_add_card_diff H
       ... ≥ card s₁                  : le_add_right
 
+variable {B : Type}
+
+theorem card_image_eq_of_inj_on {f : A → B} {s : set A} [fins : finite s] (injfs : inj_on f s) :
+  card (image f s) = card s :=
+begin
+  rewrite [↑card, to_finset_image];
+  apply finset.card_image_eq_of_inj_on,
+  rewrite to_set_to_finset,
+  apply injfs
+end
+
+theorem card_le_of_inj_on (a : set A) (b : set B) [finb : finite b]
+    (Pex : ∃ f : A → B, inj_on f a ∧ (image f a ⊆ b)) :
+  card a ≤ card b :=
+by_cases
+  (assume fina : finite a,
+    obtain f H, from Pex,
+    finset.card_le_of_inj_on (to_finset a) (to_finset b)
+      (exists.intro f
+        begin
+          rewrite [finset.subset_eq_to_set_subset, finset.to_set_image, *to_set_to_finset],
+          exact H
+        end))
+  (assume nfina : ¬ finite a,
+    by rewrite [card_of_not_finite nfina]; exact !zero_le)
+
+theorem card_image_le (f : A → B) (s : set A) [fins : finite s] : card (image f s) ≤ card s :=
+by rewrite [↑card, to_finset_image]; apply finset.card_image_le
+
+theorem inj_on_of_card_image_eq {f : A → B} {s : set A} [fins : finite s]
+  (H : card (image f s) = card s) : inj_on f s :=
+begin
+  rewrite -to_set_to_finset,
+  apply finset.inj_on_of_card_image_eq,
+  rewrite [-to_finset_to_set (finset.image _ _), finset.to_set_image, to_set_to_finset],
+  exact H
+end
+
+theorem card_pos_of_mem {a : A} {s : set A} [fins : finite s] (H : a ∈ s) : card s > 0 :=
+have (#finset a ∈ to_finset s), by rewrite [finset.mem_eq_mem_to_set, to_set_to_finset]; apply H,
+finset.card_pos_of_mem this
+
+theorem eq_of_card_eq_of_subset {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
+    (Hcard : card s₁ = card s₂) (Hsub : s₁ ⊆ s₂) :
+  s₁ = s₂ :=
+begin
+  rewrite [-to_set_to_finset s₁, -to_set_to_finset s₂, -finset.eq_eq_to_set_eq],
+  apply finset.eq_of_card_eq_of_subset Hcard,
+  rewrite [to_finset_subset_to_finset_eq],
+  exact Hsub
+end
+
+theorem exists_two_of_card_gt_one {s : set A} (H : 1 < card s) : ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b :=
+assert fins : finite s, from
+  by_contradiction
+    (assume nfins, by rewrite [card_of_not_finite nfins at H]; apply !not_succ_le_zero H),
+by rewrite [-to_set_to_finset s]; apply finset.exists_two_of_card_gt_one H
+
 end set

library/data/set/function.lean

@@ -75,6 +75,12 @@ setext (take y, iff.intro
         obtain x [(xt : x ∈ t) (fxy : f x = y)], from yift,
         mem_image (or.inr xt) fxy)))
 
+theorem image_empty (f : X → Y) : image f ∅ = ∅ :=
+eq_empty_of_forall_not_mem
+  (take y, suppose y ∈ image f ∅,
+    obtain x [(H : x ∈ empty) H'], from this,
+    H)
+
 /- maps to -/
 
 definition maps_to [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := ∀⦃x⦄, x ∈ a → f x ∈ b