From 86b64cf43b36fa79eb44104e3334d8ee6e0ff443 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 31 Dec 2015 10:42:51 -0800 Subject: [PATCH] feat(library/data/set/*,library/algebra/group_bigops): better finiteness lemmas, reindexing for big operations --- library/algebra/group_bigops.lean | 107 ++++++++++++++++--- library/algebra/intervals.lean | 124 ++++++++++++++++++---- library/data/finset/basic.lean | 11 ++ library/data/finset/comb.lean | 3 - library/data/set/basic.lean | 7 ++ library/data/set/classical_inverse.lean | 8 ++ library/data/set/equinumerosity.lean | 6 +- library/data/set/finite.lean | 44 ++++++-- library/data/set/function.lean | 32 +++++- library/data/set/map.lean | 6 ++ library/theories/group_theory/cyclic.lean | 2 +- 11 files changed, 301 insertions(+), 49 deletions(-) diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index 21f6c41bf9..fa298939d3 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -35,7 +35,7 @@ section monoid list.foldl (mulf f) 1 l -- ∏ x ← l, f x - notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r + notation `∏` binders `←` l `, ` r:(scoped f, Prodl l f) := r private theorem foldl_const (f : A → B) : ∀ (l : list A) (b : B), foldl (mulf f) b l = b * foldl (mulf f) 1 l @@ -73,7 +73,7 @@ section monoid | [] := rfl | (a::l) := by rewrite [Prodl_cons, Prodl_one, mul_one] - lemma Prodl_singleton {a : A} {f : A → B} : Prodl [a] f = f a := + lemma Prodl_singleton (a : A) (f : A → B) : Prodl [a] f = f a := !one_mul lemma Prodl_map {f : A → B} : @@ -88,7 +88,8 @@ section monoid | (a::l) := take b, assume Pconst, assert Pconstl : ∀ a', a' ∈ l → f a' = b, from take a' Pa'in, Pconst a' (mem_cons_of_mem a Pa'in), - by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons, add_one, pow_succ b] + by rewrite [Prodl_cons f, Pconst a !mem_cons, Prodl_eq_pow_of_const b Pconstl, length_cons, + add_one, pow_succ b] end monoid @@ -114,7 +115,7 @@ section add_monoid definition Suml (l : list A) (f : A → B) : B := Prodl l f -- ∑ x ← l, f x - notation `∑` binders `←` l, r:(scoped f, Suml l f) := r + notation `∑` binders `←` l `, ` r:(scoped f, Suml l f) := r theorem Suml_nil (f : A → B) : Suml [] f = 0 := Prodl_nil f theorem Suml_cons (f : A → B) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f := @@ -133,6 +134,8 @@ section add_monoid end deceqA theorem Suml_zero (l : list A) : Suml l (λ x, 0) = (0:B) := Prodl_one l + theorem Suml_singleton (a : A) (f : A → B) : Suml [a] f = f a := Prodl_singleton a f + end add_monoid section add_comm_monoid @@ -167,7 +170,7 @@ namespace finset (λ l₁ l₂ p, Prodl_eq_Prodl_of_perm f p) -- ∏ x ∈ s, f x - notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + notation `∏` binders `∈` s `, ` r:(scoped f, Prod s f) := r theorem Prod_empty (f : A → B) : Prod ∅ f = 1 := Prodl_nil f @@ -175,6 +178,9 @@ namespace finset theorem Prod_mul (s : finset A) (f g : A → B) : Prod s (λx, f x * g x) = Prod s f * Prod s g := quot.induction_on s (take u, !Prodl_mul) + theorem Prod_one (s : finset A) : Prod s (λ x, 1) = (1:B) := + quot.induction_on s (take u, !Prodl_one) + section deceqA include deceqA @@ -206,10 +212,38 @@ namespace finset take y, assume H', H2 (mem_insert_of_mem _ H'), assert H4 : f x = g x, from H2 !mem_insert, by rewrite [Prod_insert_of_not_mem f H1, Prod_insert_of_not_mem g H1, IH H3, H4]) - end deceqA - theorem Prod_one (s : finset A) : Prod s (λ x, 1) = (1:B) := - quot.induction_on s (take u, !Prodl_one) + theorem Prod_singleton (a : A) (f : A → B) : Prod '{a} f = f a := + have a ∉ ∅, from not_mem_empty a, + by+ rewrite [Prod_insert_of_not_mem f this, Prod_empty, mul_one] + + theorem Prod_image {C : Type} [deceqC : decidable_eq C] {s : finset A} (f : C → B) {g : A → C} + (H : set.inj_on g (to_set s)) : + (∏ j ∈ image g s, f j) = (∏ i ∈ s, f (g i)) := + begin + induction s with a s anins ih, + {rewrite [*Prod_empty]}, + have injg : set.inj_on g (to_set s), + from set.inj_on_of_inj_on_of_subset H (λ x, mem_insert_of_mem a), + have g a ∉ g '[s], from + suppose g a ∈ g '[s], + obtain b [(bs : b ∈ s) (gbeq : g b = g a)], from exists_of_mem_image this, + have aias : set.mem a (to_set (insert a s)), + by rewrite to_set_insert; apply set.mem_insert a s, + have bias : set.mem b (to_set (insert a s)), + by rewrite to_set_insert; apply set.mem_insert_of_mem; exact bs, + have b = a, from H bias aias gbeq, + show false, from anins (eq.subst this bs), + rewrite [image_insert, Prod_insert_of_not_mem _ this, Prod_insert_of_not_mem _ anins, ih injg] + end + + theorem Prod_eq_of_bij_on {C : Type} [deceqC : decidable_eq C] {s : finset A} {t : finset C} + (f : C → B) {g : A → C} (H : set.bij_on g (to_set s) (to_set t)) : + (∏ j ∈ t, f j) = (∏ i ∈ s, f (g i)) := + have g '[s] = t, + by apply eq_of_to_set_eq_to_set; rewrite to_set_image; exact set.image_eq_of_bij_on H, + using this, by rewrite [-this, Prod_image f (and.left (and.right H))] + end deceqA end finset /- Sum: sum indexed by a finset -/ @@ -222,11 +256,12 @@ namespace finset definition Sum (s : finset A) (f : A → B) : B := Prod s f -- ∑ x ∈ s, f x - notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r + notation `∑` binders `∈` s `, ` r:(scoped f, Sum s f) := r theorem Sum_empty (f : A → B) : Sum ∅ f = 0 := Prod_empty f theorem Sum_add (s : finset A) (f g : A → B) : Sum s (λx, f x + g x) = Sum s f + Sum s g := Prod_mul s f g + theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = (0:B) := Prod_one s section deceqA include deceqA @@ -238,9 +273,15 @@ namespace finset Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := Prod_union f disj theorem Sum_ext {s : finset A} {f g : A → B} (H : ∀x, x ∈ s → f x = g x) : Sum s f = Sum s g := Prod_ext H - end deceqA + theorem Sum_singleton (a : A) (f : A → B) : Sum '{a} f = f a := Prod_singleton a f - theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = (0:B) := Prod_one s + theorem Sum_image {C : Type} [deceqC : decidable_eq C] {s : finset A} (f : C → B) {g : A → C} + (H : set.inj_on g (to_set s)) : + (∑ j ∈ image g s, f j) = (∑ i ∈ s, f (g i)) := Prod_image f H + theorem Sum_eq_of_bij_on {C : Type} [deceqC : decidable_eq C] {s : finset A} {t : finset C} + (f : C → B) {g : A → C} (H : set.bij_on g (to_set s) (to_set t)) : + (∑ j ∈ t, f j) = (∑ i ∈ s, f (g i)) := Prod_eq_of_bij_on f H + end deceqA end finset /- @@ -259,7 +300,7 @@ section Prod noncomputable definition Prod (s : set A) (f : A → B) : B := finset.Prod (to_finset s) f -- ∏ x ∈ s, f x - notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r + notation `∏` binders `∈` s `, ` r:(scoped f, Prod s f) := r theorem Prod_empty (f : A → B) : Prod ∅ f = 1 := by rewrite [↑Prod, to_finset_empty] @@ -270,6 +311,9 @@ section Prod theorem Prod_mul (s : set A) (f g : A → B) : Prod s (λx, f x * g x) = Prod s f * Prod s g := by rewrite [↑Prod, finset.Prod_mul] + theorem Prod_one (s : set A) : Prod s (λ x, 1) = (1:B) := + by rewrite [↑Prod, finset.Prod_one] + theorem Prod_insert_of_mem (f : A → B) {a : A} {s : set A} (H : a ∈ s) : Prod (insert a s) f = Prod s f := by_cases @@ -302,8 +346,30 @@ section Prod (assume nfs : ¬ finite s, by rewrite [*Prod_of_not_finite nfs]) - theorem Prod_one (s : set A) : Prod s (λ x, 1) = (1:B) := - by rewrite [↑Prod, finset.Prod_one] + theorem Prod_singleton (a : A) (f : A → B) : Prod '{a} f = f a := + by rewrite [↑Prod, to_finset_insert, to_finset_empty, finset.Prod_singleton] + + theorem Prod_image {C : Type} {s : set A} [fins : finite s] (f : C → B) {g : A → C} + (H : inj_on g s) : + (∏ j ∈ image g s, f j) = (∏ i ∈ s, f (g i)) := + begin + have H' : inj_on g (finset.to_set (set.to_finset s)), by rewrite to_set_to_finset; exact H, + rewrite [↑Prod, to_finset_image g s, finset.Prod_image f H'] + end + + theorem Prod_eq_of_bij_on {C : Type} {s : set A} {t : set C} (f : C → B) + {g : A → C} (H : bij_on g s t) : + (∏ j ∈ t, f j) = (∏ i ∈ s, f (g i)) := + by_cases + (suppose finite s, + have g '[s] = t, from image_eq_of_bij_on H, + using this, by rewrite [-this, Prod_image f (and.left (and.right H))]) + (assume nfins : ¬ finite s, + have nfint : ¬ finite t, from + suppose finite t, + have finite s, from finite_of_bij_on' H, + show false, from nfins this, + by+ rewrite [Prod_of_not_finite nfins, Prod_of_not_finite nfint]) end Prod /- Sum: sum indexed by a set -/ @@ -318,13 +384,14 @@ section Sum proposition Sum_def (s : set A) (f : A → B) : Sum s f = finset.Sum (to_finset s) f := rfl -- ∑ x ∈ s, f x - notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r + notation `∑` binders `∈` s `, ` r:(scoped f, Sum s f) := r theorem Sum_empty (f : A → B) : Sum ∅ f = 0 := Prod_empty f theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → B) : Sum s f = 0 := Prod_of_not_finite nfins f theorem Sum_add (s : set A) (f g : A → B) : Sum s (λx, f x + g x) = Sum s f + Sum s g := Prod_mul s f g + theorem Sum_zero (s : set A) : Sum s (λ x, 0) = (0:B) := Prod_one s theorem Sum_insert_of_mem (f : A → B) {a : A} {s : set A} (H : a ∈ s) : Sum (insert a s) f = Sum s f := Prod_insert_of_mem f H @@ -336,7 +403,15 @@ section Sum theorem Sum_ext {s : set A} {f g : A → B} (H : ∀x, x ∈ s → f x = g x) : Sum s f = Sum s g := Prod_ext H - theorem Sum_zero (s : set A) : Sum s (λ x, 0) = (0:B) := Prod_one s + theorem Sum_singleton (a : A) (f : A → B) : Sum '{a} f = f a := + Prod_singleton a f + + theorem Sum_image {C : Type} {s : set A} [fins : finite s] (f : C → B) {g : A → C} + (H : inj_on g s) : + (∑ j ∈ image g s, f j) = (∑ i ∈ s, f (g i)) := Prod_image f H + theorem Sum_eq_of_bij_on {C : Type} {s : set A} {t : set C} (f : C → B) {g : A → C} + (H : bij_on g s t) : + (∑ j ∈ t, f j) = (∑ i ∈ s, f (g i)) := Prod_eq_of_bij_on f H end Sum end set diff --git a/library/algebra/intervals.lean b/library/algebra/intervals.lean index 0d083eed50..84e130e5c5 100644 --- a/library/algebra/intervals.lean +++ b/library/algebra/intervals.lean @@ -10,8 +10,17 @@ The mnemonic: o = open, c = closed, u = unbounded. For example, Iou a b is '(a, import .order data.set open set +-- TODO: move +section + open set + + theorem mem_singleton_of_eq {A : Type} {x a : A} (H : x = a) : x ∈ '{a} := + eq.subst (eq.symm H) (mem_singleton a) +end + namespace intervals +section order_pair variables {A : Type} [order_pair A] definition Ioo (a b : A) : set A := {x | a < x ∧ x < b} @@ -26,31 +35,108 @@ definition Iuc (b : A) : set A := {x | x ≤ b} notation `'` `(` a `, ` b `)` := Ioo a b notation `'` `(` a `, ` b `]` := Ioc a b notation `'[` a `, ` b `)` := Ico a b -notation `'[` a `, ` b `]` := Icc a b +notation `'[` a `, ` b `]` := Icc a b notation `'` `(` a `, ` `∞` `)` := Iou a notation `'[` a `, ` `∞` `)` := Icu a notation `'` `(` `-∞` `, ` b `)` := Iuo b notation `'` `(` `-∞` `, ` b `]` := Iuc b -variables a b c d e f : A - -/- some examples: - - check '(a, b) - check '(a, b] - check '[a, b) - check '[a, b] - check '(a, ∞) - check '[a, ∞) - check '(-∞, b) - check '(-∞, b] - - check '{a, b, c} - - check '(a, b] ∩ '(c, ∞) - check '(-∞, b) \ ('(c, d) ∪ '[e, ∞)) --/ +variables a b : A proposition Iou_inter_Iuo : '(a, ∞) ∩ '(-∞, b) = '(a, b) := rfl +proposition Icu_inter_Iuo : '[a, ∞) ∩ '(-∞, b) = '[a, b) := rfl +proposition Iou_inter_Iuc : '(a, ∞) ∩ '(-∞, b] = '(a, b] := rfl +proposition Ioc_inter_Iuc : '[a, ∞) ∩ '(-∞, b] = '[a, b] := rfl + +proposition Icc_self : '[a, a] = '{a} := +set.ext (take x, iff.intro + (suppose x ∈ '[a, a], + have x = a, from le.antisymm (and.right this) (and.left this), + show x ∈ '{a}, from mem_singleton_of_eq this) + (suppose x ∈ '{a}, + have x = a, from eq_of_mem_singleton this, + show a ≤ x ∧ x ≤ a, from and.intro (eq.subst this !le.refl) (eq.subst this !le.refl))) + +end order_pair + +section decidable_linear_order + +variables {A : Type} [decidable_linear_order A] + +proposition Icc_eq_Icc_union_Ioc {a b c : A} (H1 : a ≤ b) (H2 : b ≤ c) : + '[a, c] = '[a, b] ∪ '(b, c] := +set.ext (take x, iff.intro + (assume H3 : x ∈ '[a, c], + decidable.by_cases + (suppose x ≤ b, + or.inl (and.intro (and.left H3) this)) + (suppose ¬ x ≤ b, + or.inr (and.intro (lt_of_not_ge this) (and.right H3)))) + (suppose x ∈ '[a, b] ∪ '(b, c], + or.elim this + (suppose x ∈ '[a, b], + and.intro (and.left this) (le.trans (and.right this) H2)) + (suppose x ∈ '(b, c], + and.intro (le_of_lt (lt_of_le_of_lt H1 (and.left this))) (and.right this)))) + +end decidable_linear_order + +/- intervals of natural numbers -/ + +namespace nat +open nat eq.ops + variables m n : ℕ + + proposition Ioc_eq_Icc_succ : '(m, n] = '[succ m, n] := rfl + + proposition Ioo_eq_Ico_succ : '(m, n) = '[succ m, n) := rfl + + proposition Ico_succ_eq_Icc : '[m, succ n) = '[m, n] := + set.ext (take x, iff.intro + (assume H, and.intro (and.left H) (le_of_lt_succ (and.right H))) + (assume H, and.intro (and.left H) (lt_succ_of_le (and.right H)))) + + proposition Ioo_succ_eq_Ioc : '(m, succ n) = '(m, n] := + set.ext (take x, iff.intro + (assume H, and.intro (and.left H) (le_of_lt_succ (and.right H))) + (assume H, and.intro (and.left H) (lt_succ_of_le (and.right H)))) + + proposition Icu_zero : '[(0 : nat), ∞) = univ := + eq_univ_of_forall (take x, zero_le x) + + proposition Icc_zero (n : ℕ) : '[0, n] = '(-∞, n] := + have '[0, n] = '[0, ∞) ∩ '(-∞, n], from rfl, + by+ rewrite [this, Icu_zero, univ_inter] +end nat + +section nat -- put the instances in the intervals namespace +open nat eq.ops + variables m n : ℕ + + proposition nat.Iuc_finite [instance] (n : ℕ) : finite '(-∞, n] := + nat.induction_on n + (have '(-∞, 0] ⊆ '{0}, from λ x H, mem_singleton_of_eq (le.antisymm H !zero_le), + finite_subset this) + (take n, assume ih : finite '(-∞, n], + have '(-∞, succ n] ⊆ '(-∞, n] ∪ '{succ n}, + by intro x H; rewrite [mem_union_iff, mem_singleton_iff]; apply le_or_eq_succ_of_le_succ H, + finite_subset this) + + proposition nat.Iuo_finite [instance] (n : ℕ) : finite '(-∞, n) := + have '(-∞, n) ⊆ '(-∞, n], from λ x, le_of_lt, + finite_subset this + + proposition nat.Icc_finite [instance] (m n : ℕ) : finite ('[m, n]) := + have '[m, n] ⊆ '(-∞, n], from λ x H, and.right H, + finite_subset this + + proposition nat.Ico_finite [instance] (m n : ℕ) : finite ('[m, n)) := + have '[m, n) ⊆ '(-∞, n), from λ x H, and.right H, + finite_subset this + + proposition nat.Ioc_finite [instance] (m n : ℕ) : finite '(m, n] := + have '(m, n] ⊆ '(-∞, n], from λ x H, and.right H, + finite_subset this +end nat end intervals diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index 6bacb0425f..cb2abb34d8 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -191,6 +191,9 @@ propext (iff.intro !eq_or_mem_of_mem_insert theorem insert_empty_eq (a : A) : '{a} = singleton a := rfl +theorem mem_singleton_eq' (x a : A) : x ∈ '{a} = (x = a) := +by rewrite [mem_insert_eq, mem_empty_eq, or_false] + theorem insert_eq_of_mem {a : A} {s : finset A} (H : a ∈ s) : insert a s = s := ext (λ x, eq.substr (mem_insert_eq x a s) (or_iff_right_of_imp (λH1, eq.substr H1 H))) @@ -668,6 +671,14 @@ theorem mem_upto_eq (a n : nat) : a ∈ upto n = (a < n) := propext !mem_upto_iff end upto +theorem upto_zero : upto 0 = ∅ := rfl + +theorem upto_succ (n : ℕ) : upto (succ n) = upto n ∪ '{n} := +begin + apply ext, intro x, + rewrite [mem_union_iff, *mem_upto_iff, mem_singleton_eq', lt_succ_iff_le, nat.le_iff_lt_or_eq], +end + /- useful rules for calculations with quantifiers -/ theorem exists_mem_empty_iff {A : Type} (P : A → Prop) : (∃ x, x ∈ ∅ ∧ P x) ↔ false := iff.intro diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean index 14f22cbabb..f1df4607ea 100644 --- a/library/data/finset/comb.lean +++ b/library/data/finset/comb.lean @@ -167,9 +167,6 @@ ext (take x, iff.intro (suppose x ∈ s, mem_sep_of_mem (mem_of_subset_of_mem ssubt this) this) (suppose x ∈ {x ∈ t | x ∈ s}, of_mem_sep this)) -theorem mem_singleton_eq' (x a : A) : x ∈ '{a} = (x = a) := -by rewrite [mem_insert_eq, mem_empty_eq, or_false] - end /- set difference -/ diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 0d346ffd10..637fbd3fb8 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -79,6 +79,13 @@ ext (take x, iff.intro (assume xs, absurd xs (H x)) (assume xe, absurd xe !not_mem_empty)) +section + open classical + + theorem exists_mem_of_ne_empty {s : set X} (H : s ≠ ∅) : ∃ x, x ∈ s := + by_contradiction (assume H', H (eq_empty_of_forall_not_mem (forall_not_of_not_exists H'))) +end + theorem empty_subset (s : set X) : ∅ ⊆ s := take x, assume H, false.elim H diff --git a/library/data/set/classical_inverse.lean b/library/data/set/classical_inverse.lean index c12e8498e7..292f15ab67 100644 --- a/library/data/set/classical_inverse.lean +++ b/library/data/set/classical_inverse.lean @@ -47,6 +47,10 @@ have H1 : ∃₀ x' ∈ a, f x' = f x, from exists.intro x (and.intro xa rfl), have H2 : f' (f x) ∈ a ∧ f (f' (f x)) = f x, from inv_fun_pos H1, show f' (f x) = x, from H (and.left H2) xa (and.right H2) +theorem surj_on_inv_fun_of_inj_on (dflt : X) (mapsto : maps_to f a b) (H : inj_on f a) : + surj_on (inv_fun f a dflt) b a := +surj_on_of_right_inv_on mapsto (left_inv_on_inv_fun_of_inj_on dflt H) + theorem right_inv_on_inv_fun_of_surj_on (dflt : X) (H : surj_on f a b) : right_inv_on (inv_fun f a dflt) f b := let f' := inv_fun f a dflt in @@ -56,6 +60,10 @@ obtain x (Hx : x ∈ a ∧ f x = y), from H yb, have Hy : f' y ∈ a ∧ f (f' y) = y, from inv_fun_pos (exists.intro x Hx), and.right Hy +theorem inj_on_inv_fun (dflt : X) (H : surj_on f a b) : + inj_on (inv_fun f a dflt) b := +inj_on_of_left_inv_on (right_inv_on_inv_fun_of_surj_on dflt H) + end set open set diff --git a/library/data/set/equinumerosity.lean b/library/data/set/equinumerosity.lean index 405f40516a..43f2f57d13 100644 --- a/library/data/set/equinumerosity.lean +++ b/library/data/set/equinumerosity.lean @@ -31,7 +31,7 @@ show false, from `x ∉ f x` this theorem not_inj_on_pow {f : set X → X} (H : maps_to f (𝒫 A) A) : ¬ inj_on f (𝒫 A) := let diag := f '[{x ∈ 𝒫 A | f x ∉ x}] in -have diag ⊆ A, from image_subset_of_maps_to H (sep_subset _ _), +have diag ⊆ A, from image_subset_of_maps_to_of_subset H (sep_subset _ _), assume H₁ : inj_on f (𝒫 A), have f diag ∈ diag, from by_contradiction (suppose f diag ∉ diag, @@ -90,9 +90,9 @@ open set | 0 := show U 0 ⊆ A, from diff_subset _ _ | (n + 1) := have f '[U n] ⊆ B, - from image_subset_of_maps_to f_maps_to (U_subset_A n), + from image_subset_of_maps_to_of_subset f_maps_to (U_subset_A n), show U (n + 1) ⊆ A, - from image_subset_of_maps_to g_maps_to this + from image_subset_of_maps_to_of_subset g_maps_to this lemma g_ginv_eq {a : X} (aA : a ∈ A) (anU : a ∉ Union U) : g (ginv a) = a := have a ∈ g '[B], from by_contradiction diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean index b5a791cff4..b47cd1fe05 100644 --- a/library/data/set/finite.lean +++ b/library/data/set/finite.lean @@ -7,7 +7,7 @@ The notion of "finiteness" for sets. This approach is not computational: for exa an element s : set A satsifies finite s doesn't mean that we can compute the cardinality. For a computational representation, use the finset type. -/ -import data.set.function data.finset.to_set +import data.finset.to_set .classical_inverse open nat classical variable {A : Type} @@ -83,21 +83,21 @@ theorem to_finset_inter (s t : set A) [finite s] [finite t] : to_finset (s ∩ t) = (#finset to_finset s ∩ to_finset t) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_inter, *to_set_to_finset] -theorem finite_sep [instance] (s : set A) (p : A → Prop) [decidable_pred p] [finite s] : +theorem finite_sep [instance] (s : set A) (p : A → Prop) [finite s] : finite {x ∈ s | p x} := exists.intro (finset.sep p (to_finset s)) (by rewrite [finset.to_set_sep, *to_set_to_finset]) -theorem to_finset_sep (s : set A) (p : A → Prop) [decidable_pred p] [finite s] : +theorem to_finset_sep (s : set A) (p : A → Prop) [finite s] : to_finset {x ∈ s | p x} = (#finset {x ∈ to_finset s | p x}) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_sep, to_set_to_finset] -theorem finite_image [instance] {B : Type} [decidable_eq B] (f : A → B) (s : set A) [finite s] : +theorem finite_image [instance] {B : Type} (f : A → B) (s : set A) [finite s] : finite (f '[s]) := exists.intro (finset.image f (to_finset s)) (by rewrite [finset.to_set_image, *to_set_to_finset]) -theorem to_finset_image {B : Type} [decidable_eq B] (f : A → B) (s : set A) +theorem to_finset_image {B : Type} (f : A → B) (s : set A) [fins : finite s] : to_finset (f '[s]) = (#finset f '[to_finset s]) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_image, to_set_to_finset] @@ -105,7 +105,8 @@ by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_image, to_set_to_fins theorem finite_diff [instance] (s t : set A) [finite s] : finite (s \ t) := !finite_sep -theorem to_finset_diff (s t : set A) [finite s] [finite t] : to_finset (s \ t) = (#finset to_finset s \ to_finset t) := +theorem to_finset_diff (s t : set A) [finite s] [finite t] : + to_finset (s \ t) = (#finset to_finset s \ to_finset t) := by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_diff, *to_set_to_finset] theorem finite_subset {s t : set A} [finite t] (ssubt : s ⊆ t) : finite s := @@ -124,6 +125,37 @@ by rewrite [-finset.to_set_upto n]; apply finite_finset theorem to_finset_upto (n : ℕ) : to_finset {i | i < n} = finset.upto n := by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto) +theorem finite_of_surj_on {B : Type} {f : A → B} {s : set A} [finite s] {t : set B} + (H : surj_on f s t) : + finite t := +finite_subset H + +theorem finite_of_inj_on {B : Type} {f : A → B} {s : set A} {t : set B} [finite t] + (mapsto : maps_to f s t) (injf : inj_on f s) : + finite s := +if H : s = ∅ then + by rewrite H; apply _ +else + obtain (dflt : A) (xs : dflt ∈ s), from exists_mem_of_ne_empty H, + let finv := inv_fun f s dflt in + have surj_on finv t s, from surj_on_inv_fun_of_inj_on dflt mapsto injf, + finite_of_surj_on this + +theorem finite_of_bij_on {B : Type} {f : A → B} {s : set A} {t : set B} [finite s] + (bijf : bij_on f s t) : + finite t := +finite_of_surj_on (surj_on_of_bij_on bijf) + +theorem finite_of_bij_on' {B : Type} {f : A → B} {s : set A} {t : set B} [finite t] + (bijf : bij_on f s t) : + finite s := +finite_of_inj_on (maps_to_of_bij_on bijf) (inj_on_of_bij_on bijf) + +theorem finite_iff_finite_of_bij_on {B : Type} {f : A → B} {s : set A} {t : set B} + (bijf : bij_on f s t) : + finite s ↔ finite t := +iff.intro (assume fs, finite_of_bij_on bijf) (assume ft, finite_of_bij_on' bijf) + theorem finite_powerset (s : set A) [finite s] : finite 𝒫 s := assert H : 𝒫 s = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))], from ext (take t, iff.intro diff --git a/library/data/set/function.lean b/library/data/set/function.lean index bc718d1f80..7a88199676 100644 --- a/library/data/set/function.lean +++ b/library/data/set/function.lean @@ -31,7 +31,7 @@ take x, assume H : x ∈ a, H1 (H2 H) theorem maps_to_univ_univ (f : X → Y) : maps_to f univ univ := take x, assume H, trivial -theorem image_subset_of_maps_to {f : X → Y} {a : set X} {b : set Y} (mfab : maps_to f a b) +theorem image_subset_of_maps_to_of_subset {f : X → Y} {a : set X} {b : set Y} (mfab : maps_to f a b) {c : set X} (csuba : c ⊆ a) : f '[c] ⊆ b := take y, @@ -41,6 +41,10 @@ have x ∈ a, from csuba `x ∈ c`, have f x ∈ b, from mfab this, show y ∈ b, from yeq ▸ this +theorem image_subset_of_maps_to {f : X → Y} {a : set X} {b : set Y} (mfab : maps_to f a b) : + f '[a] ⊆ b := +image_subset_of_maps_to_of_subset mfab (subset.refl a) + /- injectivity -/ definition inj_on [reducible] (f : X → Y) (a : set X) : Prop := @@ -121,11 +125,33 @@ iff.intro obtain x H1x H2x, from H y trivial, exists.intro x H2x) +lemma image_eq_of_maps_to_of_surj_on {f : X → Y} {a : set X} {b : set Y} + (H1 : maps_to f a b) (H2 : surj_on f a b) : + f '[a] = b := +eq_of_subset_of_subset (image_subset_of_maps_to H1) H2 + /- bijectivity -/ definition bij_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := maps_to f a b ∧ inj_on f a ∧ surj_on f a b +lemma maps_to_of_bij_on {f : X → Y} {a : set X} {b : set Y} (H : bij_on f a b) : + maps_to f a b := +and.left H + +lemma inj_on_of_bij_on {f : X → Y} {a : set X} {b : set Y} (H : bij_on f a b) : + inj_on f a := +and.left (and.right H) + +lemma surj_on_of_bij_on {f : X → Y} {a : set X} {b : set Y} (H : bij_on f a b) : + surj_on f a b := +and.right (and.right H) + +lemma bij_on.mk {f : X → Y} {a : set X} {b : set Y} + (H₁ : maps_to f a b) (H₂ : inj_on f a) (H₃ : surj_on f a b) : + bij_on f a b := +and.intro H₁ (and.intro H₂ H₃) + theorem bij_on_of_eq_on {f1 f2 : X → Y} {a : set X} {b : set Y} (eqf : eq_on f1 f2 a) (H : bij_on f1 a b) : bij_on f2 a b := match H with and.intro Hmap (and.intro Hinj Hsurj) := @@ -136,6 +162,10 @@ match H with and.intro Hmap (and.intro Hinj Hsurj) := (surj_on_of_eq_on eqf Hsurj)) end +lemma image_eq_of_bij_on {f : X → Y} {a : set X} {b : set Y} (bfab : bij_on f a b) : + f '[a] = b := +image_eq_of_maps_to_of_surj_on (and.left bfab) (and.right (and.right bfab)) + theorem bij_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z} (Hg : bij_on g b c) (Hf: bij_on f a b) : bij_on (g ∘ f) a c := diff --git a/library/data/set/map.lean b/library/data/set/map.lean index e39bccdcd9..b21629b8c1 100644 --- a/library/data/set/map.lean +++ b/library/data/set/map.lean @@ -81,6 +81,9 @@ theorem surjective_compose {g : map b c} {f : map a b} (Hg : map.surjective g) map.surjective (g ∘ f) := surj_on_compose Hg Hf +theorem image_eq_of_surjective {f : map a b} (H : map.surjective f) : f '[a] = b := +image_eq_of_maps_to_of_surj_on (map.mapsto f) H + /- bijective -/ protected definition bijective (f : map a b) : Prop := map.injective f ∧ map.surjective f @@ -95,6 +98,9 @@ obtain Hg₁ Hg₂, from Hg, obtain Hf₁ Hf₂, from Hf, and.intro (injective_compose Hg₁ Hf₁) (surjective_compose Hg₂ Hf₂) +theorem image_eq_of_bijective {f : map a b} (H : map.bijective f) : f '[a] = b := +image_eq_of_surjective (proof and.right H qed) + /- left inverse -/ -- g is a left inverse to f diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean index 9b490220fd..4a1130fd95 100644 --- a/library/theories/group_theory/cyclic.lean +++ b/library/theories/group_theory/cyclic.lean @@ -305,7 +305,7 @@ lemma rotl_map {A B : Type} {f : A → B} : ∀ {l : list A}, list.rotl (map f l lemma rotl_eq_rotl : ∀ {n : nat}, map (rotl 1) (upto n) = list.rotl (upto n) | 0 := rfl | (succ n) := begin - rewrite [upto_step at {1}, upto_succ, rotl_cons, map_append], + rewrite [upto_step at {1}, fin.upto_succ, rotl_cons, map_append], congruence, rewrite [map_map], congruence, exact rotl_succ, rewrite [map_singleton], congruence, rewrite [↑rotl, mul_one n, ↑mk_mod, ↑maxi, ↑madd],