feat(library/data/set/*,library/algebra/group_bigops): better finiteness lemmas, reindexing for big operations
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
c3dfabf741
commit
86b64cf43b
11 changed files with 301 additions and 49 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 -/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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],
|
||||
|
|
|
|||
Loading…
Reference in a new issue