From a009cf24e341e48da7efda989d966189dc749480 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 10 May 2015 20:07:03 +1000 Subject: [PATCH] feat(library/data/finset/{basic,card,comb}.lean: add theorems, including card of an injective image --- library/data/finset/basic.lean | 6 ++++++ library/data/finset/card.lean | 38 ++++++++++++++++++++++++++++++---- library/data/finset/comb.lean | 36 +++++++++++++++++++++++++++++++- library/data/set/function.lean | 6 ++++++ 4 files changed, 81 insertions(+), 5 deletions(-) diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index ee8fdbf2d..dac9fd4dc 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -463,6 +463,12 @@ quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h₁ h₂, h₁ a h₂) theorem subset_of_forall {s₁ s₂ : finset A} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ := quot.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H) +theorem subset_insert [h : decidable_eq A] (s : finset A) (a : A) : s ⊆ insert a s := +subset_of_forall (take x, assume H : x ∈ s, mem_insert_of_mem _ H) + +theorem eq_of_subset_of_subset {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ := +ext (take x, iff.intro (assume H, mem_of_subset_of_mem H₁ H) (assume H, mem_of_subset_of_mem H₂ H)) + /- upto -/ section upto definition upto (n : nat) : finset nat := diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean index 4ead83106..a30d49e97 100644 --- a/library/data/finset/card.lean +++ b/library/data/finset/card.lean @@ -5,14 +5,14 @@ Author: Jeremy Avigad Cardinality calculations for finite sets. -/ -import data.finset.comb +import data.finset.to_set data.set.function open nat eq.ops namespace finset -variable {A : Type} -variable [deceq : decidable_eq A] -include deceq +variables {A B : Type} +variables [deceqA : decidable_eq A] [deceqB : decidable_eq B] +include deceqA theorem card_add_card (s₁ s₂ : finset A) : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) := finset.induction_on s₂ @@ -58,4 +58,34 @@ calc ... = card s₁ + card (s₂ \ s₁) : card_union_of_disjoint H1 ... ≥ card s₁ : le_add_right +section card_image +open set +include deceqB + +theorem card_image_eq_of_inj_on {f : A → B} {s : finset A} : + inj_on f (ts s) → card (image f s) = card s := +finset.induction_on s + (assume H : inj_on f (ts empty), calc + card (image f empty) = 0 : card_empty + ... = card empty : card_empty) + (take t a, + assume H : a ∉ t, + assume IH : inj_on f (ts t) → card (image f t) = card t, + assume H1 : inj_on f (ts (insert a t)), + have H2 : ts t ⊆ ts (insert a t), by rewrite [-subset_eq_to_set_subset]; apply subset_insert, + have H3 : card (image f t) = card t, from IH (inj_on_of_inj_on_of_subset H1 H2), + have H4 : f a ∉ image f t, + proof + assume H5 : f a ∈ image f t, + obtain x (H6 : x ∈ t ∧ f x = f a), from exists_of_mem_image H5, + have H7 : x = a, from H1 (mem_insert_of_mem _ (and.left H6)) !mem_insert (and.right H6), + show false, from H (H7 ▸ and.left H6) + qed, + calc + card (image f (insert a t)) = card (insert (f a) (image f t)) : image_insert + ... = card (image f t) + 1 : card_insert_of_not_mem H4 + ... = card t + 1 : H3 + ... = card (insert a t) : card_insert_of_not_mem H) +end card_image + end finset diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean index 7742349b1..351aa204a 100644 --- a/library/data/finset/comb.lean +++ b/library/data/finset/comb.lean @@ -27,6 +27,11 @@ rfl theorem mem_image_of_mem (f : A → B) {s : finset A} {a : A} : a ∈ s → f a ∈ image f s := quot.induction_on s (take l, assume H : a ∈ elt_of l, mem_to_finset (mem_map f H)) +theorem mem_image_of_mem_of_eq {f : A → B} {s : finset A} {a : A} {b : B} + (H1 : a ∈ s) (H2 : f a = b) : + b ∈ image f s := +eq.subst H2 (mem_image_of_mem f H1) + theorem exists_of_mem_image {f : A → B} {s : finset A} {b : B} : b ∈ image f s → ∃a, a ∈ s ∧ f a = b := quot.induction_on s @@ -37,10 +42,39 @@ theorem mem_image_iff (f : A → B) {s : finset A} {y : B} : y ∈ image f s ↔ iff.intro exists_of_mem_image (assume H, obtain x (H1 : x ∈ s ∧ f x = y), from H, - eq.subst (and.right H1) (mem_image_of_mem f (and.left H1))) + mem_image_of_mem_of_eq (and.left H1) (and.right H1)) theorem mem_image_eq (f : A → B) {s : finset A} {y : B} : y ∈ image f s = ∃x, x ∈ s ∧ f x = y := propext (mem_image_iff f) + +theorem mem_image_of_mem_image_of_subset {f : A → B} {s t : finset A} {y : B} + (H1 : y ∈ image f s) (H2 : s ⊆ t) : y ∈ image f t := +obtain x (H3: x ∈ s ∧ f x = y), from exists_of_mem_image H1, +have H4 : x ∈ t, from mem_of_subset_of_mem H2 (and.left H3), +show y ∈ image f t, from mem_image_of_mem_of_eq H4 (and.right H3) + +theorem image_insert [h' : decidable_eq A] (f : A → B) (s : finset A) (a : A) : + image f (insert a s) = insert (f a) (image f s) := +ext (take y, iff.intro + (assume H : y ∈ image f (insert a s), + obtain x (H1 : x ∈ insert a s ∧ f x = y), from exists_of_mem_image H, + have H2 : x = a ∨ x ∈ s, from eq_or_mem_of_mem_insert (and.left H1), + or.elim H2 + (assume H3 : x = a, + have H4 : f a = y, from eq.subst H3 (and.right H1), + show y ∈ insert (f a) (image f s), from eq.subst H4 !mem_insert) + (assume H3 : x ∈ s, + have H4 : f x = y, from and.right H1, + have H5 : f x ∈ image f s, from mem_image_of_mem f H3, + show y ∈ insert (f a) (image f s), from eq.subst H4 (mem_insert_of_mem _ H5))) + (assume H : y ∈ insert (f a) (image f s), + have H1 : y = f a ∨ y ∈ image f s, from eq_or_mem_of_mem_insert H, + or.elim H1 + (assume H2 : y = f a, + have H3 : f a ∈ image f (insert a s), from mem_image_of_mem f !mem_insert, + show y ∈ image f (insert a s), from eq.subst (eq.symm H2) H3) + (assume H2 : y ∈ image f s, + show y ∈ image f (insert a s), from mem_image_of_mem_image_of_subset H2 !subset_insert))) end image /- filter and set-builder notation -/ diff --git a/library/data/set/function.lean b/library/data/set/function.lean index 8012e0f54..0ee35ec5d 100644 --- a/library/data/set/function.lean +++ b/library/data/set/function.lean @@ -96,6 +96,12 @@ assume H1 : g (f x1) = g (f x2), have H2 : f x1 = f x2, from Hg fx1b fx2b H1, show x1 = x2, from Hf x1a x2a H2 +theorem inj_on_of_inj_on_of_subset {f : X → Y} {a b : set X} (H1 : inj_on f b) (H2 : a ⊆ b) : + inj_on f a := +take x1 x2 : X, assume (x1a : x1 ∈ a) (x2a : x2 ∈ a), +assume H : f x1 = f x2, +show x1 = x2, from H1 (H2 x1a) (H2 x2a) H + /- surjectivity -/ definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f '[a]