refactor(library/data/{set,finset}/basic,library/*): change notation for image to tick mark
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
17f6ab3a71
commit
4289daddcb
13 changed files with 101 additions and 99 deletions
|
|
@ -225,8 +225,8 @@ namespace finset
|
|||
{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],
|
||||
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,
|
||||
|
|
@ -240,7 +240,7 @@ namespace finset
|
|||
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,
|
||||
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
|
||||
|
|
@ -362,7 +362,7 @@ section Prod
|
|||
(∏ 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,
|
||||
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
|
||||
|
|
|
|||
|
|
@ -20,7 +20,8 @@ definition image (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)))
|
||||
notation [priority finset.prio] f `'[`:max a `]` := image f a
|
||||
|
||||
infix [priority finset.prio] `'` := image
|
||||
|
||||
theorem image_empty (f : A → B) : image f ∅ = ∅ :=
|
||||
rfl
|
||||
|
|
@ -87,9 +88,9 @@ ext (take z, iff.intro
|
|||
obtain x (Hx : x ∈ s) (Hgx : g x = y), from exists_of_mem_image Hy,
|
||||
mem_image Hx (by esimp; rewrite [Hgx, Hfy])))
|
||||
|
||||
lemma image_subset {a b : finset A} (f : A → B) (H : a ⊆ b) : f '[a] ⊆ f '[b] :=
|
||||
lemma image_subset {a b : finset A} (f : A → B) (H : a ⊆ b) : f ' a ⊆ f ' b :=
|
||||
subset_of_forall
|
||||
(take y, assume Hy : y ∈ f '[a],
|
||||
(take y, assume Hy : y ∈ f ' a,
|
||||
obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from exists_of_mem_image Hy,
|
||||
mem_image (mem_of_subset_of_mem H Hx₁) Hx₂)
|
||||
|
||||
|
|
|
|||
|
|
@ -437,10 +437,10 @@ abbreviation eq_on (f1 f2 : X → Y) (a : set X) : Prop :=
|
|||
∀₀ x ∈ a, f1 x = f2 x
|
||||
|
||||
definition image (f : X → Y) (a : set X) : set Y := {y : Y | ∃x, x ∈ a ∧ f x = y}
|
||||
notation f `'[`:max a `]` := image f a
|
||||
infix `'` := image
|
||||
|
||||
theorem image_eq_image_of_eq_on {f1 f2 : X → Y} {a : set X} (H1 : eq_on f1 f2 a) :
|
||||
f1 '[a] = f2 '[a] :=
|
||||
f1 ' a = f2 ' a :=
|
||||
ext (take y, iff.intro
|
||||
(assume H2,
|
||||
obtain x (H3 : x ∈ a ∧ f1 x = y), from H2,
|
||||
|
|
@ -454,26 +454,26 @@ ext (take y, iff.intro
|
|||
exists.intro x (and.intro H4 H5)))
|
||||
|
||||
theorem mem_image {f : X → Y} {a : set X} {x : X} {y : Y}
|
||||
(H1 : x ∈ a) (H2 : f x = y) : y ∈ f '[a] :=
|
||||
(H1 : x ∈ a) (H2 : f x = y) : y ∈ f ' a :=
|
||||
exists.intro x (and.intro H1 H2)
|
||||
|
||||
theorem mem_image_of_mem (f : X → Y) {x : X} {a : set X} (H : x ∈ a) : f x ∈ image f a :=
|
||||
mem_image H rfl
|
||||
|
||||
lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
|
||||
lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
|
||||
ext (take z,
|
||||
iff.intro
|
||||
(assume Hz : z ∈ (f ∘ g) '[a],
|
||||
(assume Hz : z ∈ (f ∘ g) ' a,
|
||||
obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
|
||||
have Hgx : g x ∈ g '[a], from mem_image Hx₁ rfl,
|
||||
show z ∈ f '[g '[a]], from mem_image Hgx Hx₂)
|
||||
(assume Hz : z ∈ f '[g '[a]],
|
||||
obtain y (Hy₁ : y ∈ g '[a]) (Hy₂ : f y = z), from Hz,
|
||||
have Hgx : g x ∈ g ' a, from mem_image Hx₁ rfl,
|
||||
show z ∈ f ' (g ' a), from mem_image Hgx Hx₂)
|
||||
(assume Hz : z ∈ f ' (g 'a),
|
||||
obtain y (Hy₁ : y ∈ g ' a) (Hy₂ : f y = z), from Hz,
|
||||
obtain x (Hz₁ : x ∈ a) (Hz₂ : g x = y), from Hy₁,
|
||||
show z ∈ (f ∘ g) '[a], from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
|
||||
show z ∈ (f ∘ g) ' a, from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
|
||||
|
||||
lemma image_subset {a b : set X} (f : X → Y) (H : a ⊆ b) : f '[a] ⊆ f '[b] :=
|
||||
take y, assume Hy : y ∈ f '[a],
|
||||
lemma image_subset {a b : set X} (f : X → Y) (H : a ⊆ b) : f ' a ⊆ f ' b :=
|
||||
take y, assume Hy : y ∈ f ' a,
|
||||
obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from Hy,
|
||||
mem_image (H Hx₁) Hx₂
|
||||
|
||||
|
|
@ -501,24 +501,24 @@ eq_empty_of_forall_not_mem
|
|||
H)
|
||||
|
||||
theorem mem_image_complement (t : set X) (S : set (set X)) :
|
||||
t ∈ complement '[S] ↔ -t ∈ S :=
|
||||
t ∈ complement ' S ↔ -t ∈ S :=
|
||||
iff.intro
|
||||
(suppose t ∈ complement '[S],
|
||||
(suppose t ∈ complement ' S,
|
||||
obtain t' [(Ht' : t' ∈ S) (Ht : -t' = t)], from this,
|
||||
show -t ∈ S, by rewrite [-Ht, comp_comp]; exact Ht')
|
||||
(suppose -t ∈ S,
|
||||
have -(-t) ∈ complement '[S], from mem_image_of_mem complement this,
|
||||
show t ∈ complement '[S], from comp_comp t ▸ this)
|
||||
have -(-t) ∈ complement 'S, from mem_image_of_mem complement this,
|
||||
show t ∈ complement 'S, from comp_comp t ▸ this)
|
||||
|
||||
theorem image_id (s : set X) : id '[s] = s :=
|
||||
theorem image_id (s : set X) : id ' s = s :=
|
||||
ext (take x, iff.intro
|
||||
(suppose x ∈ id '[s],
|
||||
(suppose x ∈ id ' s,
|
||||
obtain x' [(Hx' : x' ∈ s) (x'eq : x' = x)], from this,
|
||||
show x ∈ s, by rewrite [-x'eq]; apply Hx')
|
||||
(suppose x ∈ s, mem_image_of_mem id this))
|
||||
|
||||
theorem complement_complement_image (S : set (set X)) :
|
||||
complement '[complement '[S]] = S :=
|
||||
complement ' (complement ' S) = S :=
|
||||
by rewrite [-image_compose, complement_compose_complement, image_id]
|
||||
|
||||
end image
|
||||
|
|
@ -648,30 +648,30 @@ theorem sInter_insert (s : set X) (T : set (set X)) :
|
|||
by rewrite [insert_eq, sInter_union, sInter_singleton]
|
||||
|
||||
theorem comp_sUnion (S : set (set X)) :
|
||||
- ⋃₀ S = ⋂₀ (complement '[S]) :=
|
||||
- ⋃₀ S = ⋂₀ (complement ' S) :=
|
||||
ext (take x, iff.intro
|
||||
(assume H : x ∈ -(⋃₀ S),
|
||||
take t, suppose t ∈ complement '[S],
|
||||
take t, suppose t ∈ complement ' S,
|
||||
obtain t' [(Ht' : t' ∈ S) (Ht : -t' = t)], from this,
|
||||
have x ∈ -t', from suppose x ∈ t', H (mem_sUnion this Ht'),
|
||||
show x ∈ t, using this, by rewrite -Ht; apply this)
|
||||
(assume H : x ∈ ⋂₀ (complement '[S]),
|
||||
(assume H : x ∈ ⋂₀ (complement ' S),
|
||||
suppose x ∈ ⋃₀ S,
|
||||
obtain t [(tS : t ∈ S) (xt : x ∈ t)], from this,
|
||||
have -t ∈ complement '[S], from mem_image_of_mem complement tS,
|
||||
have -t ∈ complement ' S, from mem_image_of_mem complement tS,
|
||||
have x ∈ -t, from H this,
|
||||
show false, proof this xt qed))
|
||||
|
||||
theorem sUnion_eq_comp_sInter_comp (S : set (set X)) :
|
||||
⋃₀ S = - ⋂₀ (complement '[S]) :=
|
||||
⋃₀ S = - ⋂₀ (complement ' S) :=
|
||||
by rewrite [-comp_comp, comp_sUnion]
|
||||
|
||||
theorem comp_sInter (S : set (set X)) :
|
||||
- ⋂₀ S = ⋃₀ (complement '[S]) :=
|
||||
- ⋂₀ S = ⋃₀ (complement ' S) :=
|
||||
by rewrite [sUnion_eq_comp_sInter_comp, complement_complement_image]
|
||||
|
||||
theorem sInter_eq_comp_sUnion_comp (S : set (set X)) :
|
||||
⋂₀ S = -(⋃₀ (complement '[S])) :=
|
||||
⋂₀ S = -(⋃₀ (complement ' S)) :=
|
||||
by rewrite [-comp_comp, comp_sInter]
|
||||
|
||||
-- Union and Inter: a family of sets indexed by a type
|
||||
|
|
@ -685,26 +685,26 @@ show x ∈ c, from H i Hi
|
|||
theorem subset_Inter {I : Type} {b : I → set X} {c : set X} (H : ∀ i, c ⊆ b i) : c ⊆ ⋂ i, b i :=
|
||||
λ x cx i, H i cx
|
||||
|
||||
theorem Union_eq_sUnion_image {X I : Type} (s : I → set X) : (⋃ i, s i) = ⋃₀ (s '[univ]) :=
|
||||
theorem Union_eq_sUnion_image {X I : Type} (s : I → set X) : (⋃ i, s i) = ⋃₀ (s ' univ) :=
|
||||
ext (take x, iff.intro
|
||||
(suppose x ∈ Union s,
|
||||
obtain i (Hi : x ∈ s i), from this,
|
||||
mem_sUnion Hi (mem_image_of_mem s trivial))
|
||||
(suppose x ∈ sUnion (s '[univ]),
|
||||
obtain t [(Ht : t ∈ s '[univ]) (Hx : x ∈ t)], from this,
|
||||
(suppose x ∈ sUnion (s ' univ),
|
||||
obtain t [(Ht : t ∈ s ' univ) (Hx : x ∈ t)], from this,
|
||||
obtain i [univi (Hi : s i = t)], from Ht,
|
||||
exists.intro i (show x ∈ s i, by rewrite Hi; apply Hx)))
|
||||
|
||||
theorem Inter_eq_sInter_image {X I : Type} (s : I → set X) : (⋂ i, s i) = ⋂₀ (s '[univ]) :=
|
||||
theorem Inter_eq_sInter_image {X I : Type} (s : I → set X) : (⋂ i, s i) = ⋂₀ (s ' univ) :=
|
||||
ext (take x, iff.intro
|
||||
(assume H : x ∈ Inter s,
|
||||
take t,
|
||||
suppose t ∈ s '[univ],
|
||||
suppose t ∈ s 'univ,
|
||||
obtain i [univi (Hi : s i = t)], from this,
|
||||
show x ∈ t, by rewrite -Hi; exact H i)
|
||||
(assume H : x ∈ ⋂₀ (s '[univ]),
|
||||
(assume H : x ∈ ⋂₀ (s ' univ),
|
||||
take i,
|
||||
have s i ∈ s '[univ], from mem_image_of_mem s trivial,
|
||||
have s i ∈ s ' univ, from mem_image_of_mem s trivial,
|
||||
show x ∈ s i, from H this))
|
||||
|
||||
theorem comp_Union {X I : Type} (s : I → set X) : - (⋃ i, s i) = (⋂ i, - s i) :=
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ have x ∈ f x, from Hx⁻¹ ▸ this,
|
|||
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
|
||||
let diag := f ' {x ∈ 𝒫 A | f x ∉ x} in
|
||||
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
|
||||
|
|
@ -83,20 +83,20 @@ open set
|
|||
/- define a sequence of sets U -/
|
||||
|
||||
definition U : ℕ → set X
|
||||
| U 0 := A \ g '[B]
|
||||
| U (n + 1) := g '[f '[U n]]
|
||||
| U 0 := A \ (g ' B)
|
||||
| U (n + 1) := g ' (f ' (U n))
|
||||
|
||||
lemma U_subset_A : ∀ n, U n ⊆ A
|
||||
| 0 := show U 0 ⊆ A,
|
||||
from diff_subset _ _
|
||||
| (n + 1) := have f '[U n] ⊆ B,
|
||||
| (n + 1) := have f ' (U n) ⊆ B,
|
||||
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_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
|
||||
(suppose a ∉ g '[B],
|
||||
have a ∈ g ' B, from by_contradiction
|
||||
(suppose a ∉ g ' B,
|
||||
have a ∈ U 0, from and.intro aA this,
|
||||
have a ∈ Union U, from exists.intro 0 this,
|
||||
show false, from anU this),
|
||||
|
|
@ -135,7 +135,7 @@ open set
|
|||
... = g (h a₂) : heq
|
||||
... = g (ginv a₂) : ha₂eq
|
||||
... = a₂ : g_ginv_eq a₂A `a₂ ∉ Union U`,
|
||||
have g (f a₁) ∈ g '[f '[U n]],
|
||||
have g (f a₁) ∈ g ' (f ' (U n)),
|
||||
from mem_image_of_mem g (mem_image_of_mem f a₁Un),
|
||||
have a₂ ∈ U (n + 1),
|
||||
from `g (f a₁) = a₂` ▸ this,
|
||||
|
|
@ -186,12 +186,12 @@ open set
|
|||
begin
|
||||
cases n with n,
|
||||
{have g b ∈ U 0, from gbUn,
|
||||
have g b ∉ g '[B], from and.right this,
|
||||
have g b ∈ g '[B], from mem_image_of_mem g `b ∈ B`,
|
||||
show b ∈ h '[A], from absurd `g b ∈ g '[B]` `g b ∉ g '[B]`},
|
||||
have g b ∉ g ' B, from and.right this,
|
||||
have g b ∈ g ' B, from mem_image_of_mem g `b ∈ B`,
|
||||
show b ∈ h ' A, from absurd `g b ∈ g ' B` `g b ∉ g ' B`},
|
||||
{have g b ∈ U (succ n), from gbUn,
|
||||
have g b ∈ g '[f '[U n]], from this,
|
||||
obtain b' [(b'fUn : b' ∈ f '[U n]) (geq : g b' = g b)], from this,
|
||||
have g b ∈ g ' (f ' (U n)), from this,
|
||||
obtain b' [(b'fUn : b' ∈ f ' (U n)) (geq : g b' = g b)], from this,
|
||||
obtain a [(aUn : a ∈ U n) (faeq : f a = b')], from b'fUn,
|
||||
have g (f a) = g b, by rewrite [faeq, geq],
|
||||
have a ∈ A, from U_subset_A n aUn,
|
||||
|
|
@ -199,12 +199,12 @@ open set
|
|||
have f a = b, from ginj `f a ∈ B` `b ∈ B` `g (f a) = g b`,
|
||||
have a ∈ Union U, from exists.intro n aUn,
|
||||
have h a = f a, from dif_pos this,
|
||||
show b ∈ h '[A], from mem_image `a ∈ A` (`h a = f a` ⬝ `f a = b`)}
|
||||
show b ∈ h ' A, from mem_image `a ∈ A` (`h a = f a` ⬝ `f a = b`)}
|
||||
end)
|
||||
(suppose g b ∉ Union U,
|
||||
have eq₁ : h (g b) = ginv (g b), from dif_neg this,
|
||||
have eq₂ : ginv (g b) = b, from ginv_g_eq `b ∈ B`,
|
||||
show b ∈ h '[A], from mem_image `g b ∈ A` (eq₁ ⬝ eq₂))
|
||||
show b ∈ h ' A, from mem_image `g b ∈ A` (eq₁ ⬝ eq₂))
|
||||
end
|
||||
end schroeder_bernstein
|
||||
|
||||
|
|
|
|||
|
|
@ -93,13 +93,13 @@ theorem to_finset_sep (s : set A) (p : A → Prop) [finite s] :
|
|||
by apply to_finset_eq_of_to_set_eq; rewrite [finset.to_set_sep, to_set_to_finset]
|
||||
|
||||
theorem finite_image [instance] {B : Type} (f : A → B) (s : set A) [finite s] :
|
||||
finite (f '[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} (f : A → B) (s : set A)
|
||||
[fins : finite s] :
|
||||
to_finset (f '[s]) = (#finset f '[to_finset 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]
|
||||
|
||||
theorem finite_diff [instance] (s t : set A) [finite s] : finite (s \ t) :=
|
||||
|
|
@ -157,7 +157,7 @@ theorem finite_iff_finite_of_bij_on {B : Type} {f : A → B} {s : set A} {t : se
|
|||
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))],
|
||||
assert H : 𝒫 s = finset.to_set ' (finset.to_set (#finset 𝒫 (to_finset s))),
|
||||
from ext (take t, iff.intro
|
||||
(suppose t ∈ 𝒫 s,
|
||||
assert t ⊆ s, from this,
|
||||
|
|
|
|||
|
|
@ -33,16 +33,16 @@ take x, assume H, trivial
|
|||
|
||||
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 :=
|
||||
f ' c ⊆ b :=
|
||||
take y,
|
||||
suppose y ∈ f '[c],
|
||||
suppose y ∈ f ' c,
|
||||
obtain x [(xc : x ∈ c) (yeq : f x = y)], from this,
|
||||
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 :=
|
||||
f ' a ⊆ b :=
|
||||
image_subset_of_maps_to_of_subset mfab (subset.refl a)
|
||||
|
||||
/- injectivity -/
|
||||
|
|
@ -90,7 +90,7 @@ iff.intro
|
|||
|
||||
/- surjectivity -/
|
||||
|
||||
definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f '[a]
|
||||
definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f ' a
|
||||
|
||||
theorem surj_on_of_eq_on {f1 f2 : X → Y} {a : set X} {b : set Y} (eq_f1_f2 : eq_on f1 f2 a)
|
||||
(surj_f1 : surj_on f1 a b) :
|
||||
|
|
@ -127,7 +127,7 @@ iff.intro
|
|||
|
||||
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 :=
|
||||
f ' a = b :=
|
||||
eq_of_subset_of_subset (image_subset_of_maps_to H1) H2
|
||||
|
||||
/- bijectivity -/
|
||||
|
|
@ -163,7 +163,7 @@ match H with and.intro Hmap (and.intro Hinj 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 :=
|
||||
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}
|
||||
|
|
|
|||
|
|
@ -81,7 +81,7 @@ 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 :=
|
||||
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 -/
|
||||
|
|
@ -98,7 +98,7 @@ 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 :=
|
||||
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 -/
|
||||
|
|
|
|||
|
|
@ -188,6 +188,7 @@ reserve infixl ` ∩ `:70
|
|||
reserve infixl ` ∪ `:65
|
||||
reserve infix ` ⊆ `:50
|
||||
reserve infix ` ⊇ `:50
|
||||
reserve infix ` ' `:75 -- for the image of a set under a function
|
||||
|
||||
/- other symbols -/
|
||||
|
||||
|
|
|
|||
|
|
@ -250,7 +250,7 @@ exists.intro x
|
|||
section
|
||||
local attribute mem [quasireducible]
|
||||
-- TODO: is there a better place to put this?
|
||||
proposition image_neg_eq (X : set ℝ) : (λ x, -x) '[X] = {x | -x ∈ X} :=
|
||||
proposition image_neg_eq (X : set ℝ) : (λ x, -x) ' X = {x | -x ∈ X} :=
|
||||
set.ext (take x, iff.intro
|
||||
(assume H, obtain y [(Hy₁ : y ∈ X) (Hy₂ : -y = x)], from H,
|
||||
show -x ∈ X, by rewrite [-Hy₂, neg_neg]; exact Hy₁)
|
||||
|
|
@ -425,20 +425,20 @@ have X i ≤ X (i + (j - i)), from !this,
|
|||
by+ rewrite [add_sub_of_le `i ≤ j` at this]; exact this
|
||||
|
||||
proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ}
|
||||
(Hb : ∀ i, X i ≤ b) : X ⟶ sup (X '[univ]) in ℕ :=
|
||||
let sX := sup (X '[univ]) in
|
||||
(Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) in ℕ :=
|
||||
let sX := sup (X ' univ) in
|
||||
have Xle : ∀ i, X i ≤ sX, from
|
||||
take i,
|
||||
have ∀ x, x ∈ X '[univ] → x ≤ b, from
|
||||
have ∀ x, x ∈ X ' univ → x ≤ b, from
|
||||
(take x, assume H,
|
||||
obtain i [H' (Hi : X i = x)], from H,
|
||||
by rewrite -Hi; exact Hb i),
|
||||
show X i ≤ sX, from le_sup (mem_image_of_mem X !mem_univ) this,
|
||||
have exX : ∃ x, x ∈ X '[univ],
|
||||
have exX : ∃ x, x ∈ X ' univ,
|
||||
from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
|
||||
take ε, assume epos : ε > 0,
|
||||
have sX - ε < sX, from !sub_lt_of_pos epos,
|
||||
obtain x' [(H₁x' : x' ∈ X '[univ]) (H₂x' : sX - ε < x')],
|
||||
obtain x' [(H₁x' : x' ∈ X ' univ) (H₂x' : sX - ε < x')],
|
||||
from exists_mem_and_lt_of_lt_sup exX this,
|
||||
obtain i [H' (Hi : X i = x')], from H₁x',
|
||||
have Hi' : ∀ j, j ≥ i → sX - ε < X j, from
|
||||
|
|
@ -488,15 +488,15 @@ begin
|
|||
end
|
||||
|
||||
proposition converges_to_seq_inf_of_nonincreasing (nonincX : nonincreasing X) {b : ℝ}
|
||||
(Hb : ∀ i, b ≤ X i) : X ⟶ inf (X '[univ]) in ℕ :=
|
||||
have H₁ : ∃ x, x ∈ X '[univ], from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
|
||||
have H₂ : ∀ x, x ∈ X '[univ] → b ≤ x, from
|
||||
(Hb : ∀ i, b ≤ X i) : X ⟶ inf (X ' univ) in ℕ :=
|
||||
have H₁ : ∃ x, x ∈ X ' univ, from exists.intro (X 0) (mem_image_of_mem X !mem_univ),
|
||||
have H₂ : ∀ x, x ∈ X ' univ → b ≤ x, from
|
||||
(take x, assume H,
|
||||
obtain i [Hi₁ (Hi₂ : X i = x)], from H,
|
||||
show b ≤ x, by rewrite -Hi₂; apply Hb i),
|
||||
have H₃ : {x : ℝ | -x ∈ X '[univ]} = {x : ℝ | x ∈ (λ n, -X n) '[univ]}, from calc
|
||||
{x : ℝ | -x ∈ X '[univ]} = (λ y, -y) '[X '[univ]] : by rewrite image_neg_eq
|
||||
... = {x : ℝ | x ∈ (λ n, -X n) '[univ]} : image_compose,
|
||||
have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, from calc
|
||||
{x : ℝ | -x ∈ X ' univ} = (λ y, -y) ' (X ' univ) : by rewrite image_neg_eq
|
||||
... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_compose,
|
||||
have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i),
|
||||
begin+
|
||||
rewrite [-neg_converges_to_seq_iff, -sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX],
|
||||
|
|
@ -515,7 +515,7 @@ suffices H' : (λ n, (abs x)^n) ⟶ 0 in ℕ, from
|
|||
using this,
|
||||
by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H',
|
||||
let aX := (λ n, (abs x)^n),
|
||||
iaX := inf (aX '[univ]),
|
||||
iaX := inf (aX ' univ),
|
||||
asX := (λ n, (abs x)^(succ n)) in
|
||||
have noninc_aX : nonincreasing aX, from
|
||||
nonincreasing_of_forall_succ_le
|
||||
|
|
|
|||
|
|
@ -148,8 +148,8 @@ have a ∈ s, from mem_of_subset_of_mem (subset_of_mem_powerset tpows) this,
|
|||
anins this
|
||||
|
||||
private theorem aux₃ {a : A} {s t : finset A} (anins : a ∉ s) (k : ℕ) :
|
||||
t ∈ (insert a) '[powerset s] ∧ card t = succ k ↔
|
||||
t ∈ (insert a) '[{t' ∈ powerset s | card t' = k}] :=
|
||||
t ∈ (insert a) ' (powerset s) ∧ card t = succ k ↔
|
||||
t ∈ (insert a) ' {t' ∈ powerset s | card t' = k} :=
|
||||
iff.intro
|
||||
(assume H,
|
||||
obtain H' cardt, from H,
|
||||
|
|
@ -167,13 +167,13 @@ iff.intro
|
|||
assert t'pows : t' ∈ powerset s, from mem_of_mem_sep Ht',
|
||||
assert cardt' : card t' = k, from of_mem_sep Ht',
|
||||
and.intro
|
||||
(show t ∈ (insert a) '[powerset s], from mem_image t'pows teq)
|
||||
(show t ∈ (insert a) ' (powerset s), from mem_image t'pows teq)
|
||||
(show card t = succ k,
|
||||
by rewrite [-teq, card_insert_of_not_mem (aux₂ anins t'pows), cardt']))
|
||||
|
||||
private theorem aux₄ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
|
||||
{t ∈ powerset (insert a s)| card t = succ k} =
|
||||
{t ∈ powerset s | card t = succ k} ∪ (insert a) '[{t ∈ powerset s | card t = k}] :=
|
||||
{t ∈ powerset s | card t = succ k} ∪ (insert a) ' {t ∈ powerset s | card t = k} :=
|
||||
begin
|
||||
apply ext, intro t,
|
||||
rewrite [powerset_insert anins, mem_union_iff, *mem_sep_iff, mem_union_iff, and.right_distrib,
|
||||
|
|
@ -181,7 +181,7 @@ begin
|
|||
end
|
||||
|
||||
private theorem aux₅ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
|
||||
{t ∈ powerset s | card t = succ k} ∩ (insert a) '[{t ∈ powerset s | card t = k}] = ∅ :=
|
||||
{t ∈ powerset s | card t = succ k} ∩ (insert a) ' {t ∈ powerset s | card t = k} = ∅ :=
|
||||
inter_eq_empty
|
||||
(take t, assume Ht₁ Ht₂,
|
||||
have tpows : t ∈ powerset s, from mem_of_mem_sep Ht₁,
|
||||
|
|
@ -191,7 +191,7 @@ inter_eq_empty
|
|||
show false, from anint aint)
|
||||
|
||||
private theorem aux₆ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
|
||||
card ((insert a) '[{t ∈ powerset s | card t = k}]) = card {t ∈ powerset s | card t = k} :=
|
||||
card ((insert a) ' {t ∈ powerset s | card t = k}) = card {t ∈ powerset s | card t = k} :=
|
||||
have set.inj_on (insert a) (ts {t ∈ powerset s| card t = k}), from
|
||||
take t₁ t₂, assume Ht₁ Ht₂,
|
||||
assume Heq : insert a t₁ = insert a t₂,
|
||||
|
|
|
|||
|
|
@ -75,9 +75,9 @@ theorem hom_map_inv (a : A) : f a⁻¹ = (f a)⁻¹ :=
|
|||
assert P3 : (f a⁻¹) * (f a) = (f a)⁻¹ * (f a), from eq.symm (mul.left_inv (f a)) ▸ P2,
|
||||
mul_right_cancel P3
|
||||
|
||||
theorem hom_map_mul_closed (H : set A) : mul_closed_on H → mul_closed_on (f '[H]) :=
|
||||
theorem hom_map_mul_closed (H : set A) : mul_closed_on H → mul_closed_on (f ' H) :=
|
||||
assume Pclosed, assume b1, assume b2,
|
||||
assume Pb1 : b1 ∈ f '[ H], assume Pb2 : b2 ∈ f '[ H],
|
||||
assume Pb1 : b1 ∈ f ' H, assume Pb2 : b2 ∈ f ' H,
|
||||
obtain a1 (Pa1 : a1 ∈ H ∧ f a1 = b1), from Pb1,
|
||||
obtain a2 (Pa2 : a2 ∈ H ∧ f a2 = b2), from Pb2,
|
||||
assert Pa1a2 : a1 * a2 ∈ H, from Pclosed a1 a2 (and.left Pa1) (and.left Pa2),
|
||||
|
|
@ -115,14 +115,14 @@ variable {H : set A}
|
|||
variable [is_subgH : is_subgroup H]
|
||||
include is_subgH
|
||||
|
||||
theorem hom_map_subgroup : is_subgroup (f '[H]) :=
|
||||
have Pone : 1 ∈ f '[H], from mem_image (@subg_has_one _ _ H _) (hom_map_one f),
|
||||
have Pclosed : mul_closed_on (f '[H]), from hom_map_mul_closed f H subg_mul_closed,
|
||||
assert Pinv : ∀ b, b ∈ f '[H] → b⁻¹ ∈ f '[H], from
|
||||
theorem hom_map_subgroup : is_subgroup (f ' H) :=
|
||||
have Pone : 1 ∈ f ' H, from mem_image (@subg_has_one _ _ H _) (hom_map_one f),
|
||||
have Pclosed : mul_closed_on (f ' H), from hom_map_mul_closed f H subg_mul_closed,
|
||||
assert Pinv : ∀ b, b ∈ f ' H → b⁻¹ ∈ f ' H, from
|
||||
assume b, assume Pimg,
|
||||
obtain a (Pa : a ∈ H ∧ f a = b), from Pimg,
|
||||
assert Painv : a⁻¹ ∈ H, from subg_has_inv a (and.left Pa),
|
||||
assert Pfainv : (f a)⁻¹ ∈ f '[H], from mem_image Painv (hom_map_inv f a),
|
||||
assert Pfainv : (f a)⁻¹ ∈ f ' H, from mem_image Painv (hom_map_inv f a),
|
||||
and.right Pa ▸ Pfainv,
|
||||
is_subgroup.mk Pone Pclosed Pinv
|
||||
end
|
||||
|
|
|
|||
|
|
@ -17,8 +17,8 @@ variable [s : semigroup A]
|
|||
include s
|
||||
definition lmul (a : A) := λ x, a * x
|
||||
definition rmul (a : A) := λ x, x * a
|
||||
definition l a (S : set A) := (lmul a) '[S]
|
||||
definition r a (S : set A) := (rmul a) '[S]
|
||||
definition l a (S : set A) := (lmul a) ' S
|
||||
definition r a (S : set A) := (rmul a) ' S
|
||||
lemma lmul_compose : ∀ (a b : A), (lmul a) ∘ (lmul b) = lmul (a*b) :=
|
||||
take a, take b,
|
||||
funext (assume x, by
|
||||
|
|
@ -28,11 +28,11 @@ lemma rmul_compose : ∀ (a b : A), (rmul a) ∘ (rmul b) = rmul (b*a) :=
|
|||
funext (assume x, by
|
||||
rewrite [↑function.compose, ↑rmul, mul.assoc])
|
||||
lemma lcompose a b (S : set A) : l a (l b S) = l (a*b) S :=
|
||||
calc (lmul a) '[(lmul b) '[S]] = ((lmul a) ∘ (lmul b)) '[S] : image_compose
|
||||
... = lmul (a*b) '[S] : lmul_compose
|
||||
calc (lmul a) ' ((lmul b) ' S) = ((lmul a) ∘ (lmul b)) ' S : image_compose
|
||||
... = lmul (a*b) ' S : lmul_compose
|
||||
lemma rcompose a b (S : set A) : r a (r b S) = r (b*a) S :=
|
||||
calc (rmul a) '[(rmul b) '[S]] = ((rmul a) ∘ (rmul b)) '[S] : image_compose
|
||||
... = rmul (b*a) '[S] : rmul_compose
|
||||
calc (rmul a) ' ((rmul b) ' S) = ((rmul a) ∘ (rmul b)) ' S : image_compose
|
||||
... = rmul (b*a) ' S : rmul_compose
|
||||
lemma l_sub a (S H : set A) : S ⊆ H → (l a S) ⊆ (l a H) := image_subset (lmul a)
|
||||
definition l_same S (a b : A) := l a S = l b S
|
||||
definition r_same S (a b : A) := r a S = r b S
|
||||
|
|
|
|||
|
|
@ -34,8 +34,8 @@ theorem Open_sUnion {S : set (set X)} (H : ∀₀ t ∈ S, Open t) : Open (⋃
|
|||
sUnion_mem_opens H
|
||||
|
||||
theorem Open_Union {I : Type} {s : I → set X} (H : ∀ i, Open (s i)) : Open (⋃ i, s i) :=
|
||||
have ∀₀ t ∈ s '[univ], Open t,
|
||||
from take t, suppose t ∈ s '[univ],
|
||||
have ∀₀ t ∈ s ' univ, Open t,
|
||||
from take t, suppose t ∈ s ' univ,
|
||||
obtain i [univi (Hi : s i = t)], from this,
|
||||
show Open t, by rewrite -Hi; exact H i,
|
||||
using this, by rewrite Union_eq_sUnion_image; apply Open_sUnion this
|
||||
|
|
|
|||
Loading…
Reference in a new issue