michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/set/*): rename setext to ext

Browse source
This commit is contained in:
Jeremy Avigad 2015-08-09 21:33:10 -04:00
parent d77bdaabc2
commit 244052b413
3 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/set/finite.lean
View file

@ -134,7 +134,7 @@ by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto)
theorem finite_powerset (s : set A) [fins : finite s] : finite (𝒫 s) := theorem finite_powerset (s : set A) [fins : 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 setext (take t, iff.intro from ext (take t, iff.intro
(suppose t ∈ 𝒫 s, (suppose t ∈ 𝒫 s,
assert t ⊆ s, from this, assert t ⊆ s, from this,
assert finite t, from finite_subset this, assert finite t, from finite_subset this,

6
library/data/set/function.lean
View file

@ -22,7 +22,7 @@ notation f `'[`:max a `]` := image f a
theorem image_eq_image_of_eq_on {f1 f2 : X → Y} {a : set X} (H1 : eq_on f1 f2 a) : 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] :=
setext (take y, iff.intro ext (take y, iff.intro
(assume H2, (assume H2,
obtain x (H3 : x ∈ a ∧ f1 x = y), from H2, obtain x (H3 : x ∈ a ∧ f1 x = y), from H2,
have H4 : x ∈ a, from and.left H3, have H4 : x ∈ a, from and.left H3,
@ -42,7 +42,7 @@ theorem mem_image_of_mem (f : X → Y) {x : X} {a : set X} (H : x ∈ a) : f x
mem_image H rfl 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]] :=
setext (take z, ext (take z,
iff.intro 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, obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
@ -60,7 +60,7 @@ mem_image (H Hx₁) Hx₂
theorem image_union (f : X → Y) (s t : set X) : theorem image_union (f : X → Y) (s t : set X) :
image f (s ∪ t) = image f s ∪ image f t := image f (s ∪ t) = image f s ∪ image f t :=
setext (take y, iff.intro ext (take y, iff.intro
(assume H : y ∈ image f (s ∪ t), (assume H : y ∈ image f (s ∪ t),
obtain x [(xst : x ∈ s ∪ t) (fxy : f x = y)], from H, obtain x [(xst : x ∈ s ∪ t) (fxy : f x = y)], from H,
or.elim xst or.elim xst

8
library/theories/group_theory/subgroup.lean
View file

@ -84,7 +84,7 @@ lemma lmul_inj_on (a : A) (H : set A) : inj_on (lmul_by a) H :=
inj_on_of_left_inv_on (lmul_inv_on a H) inj_on_of_left_inv_on (lmul_inv_on a H)
lemma glcoset_eq_lcoset a (H : set A) : a ∘> H = coset.l a H := lemma glcoset_eq_lcoset a (H : set A) : a ∘> H = coset.l a H :=
setext ext
begin begin
intro x, intro x,
rewrite [↑glcoset, ↑coset.l, ↑image, ↑set_of, ↑mem, ↑coset.lmul], rewrite [↑glcoset, ↑coset.l, ↑image, ↑set_of, ↑mem, ↑coset.lmul],
@ -103,7 +103,7 @@ lemma glcoset_eq_lcoset a (H : set A) : a ∘> H = coset.l a H :=
lemma grcoset_eq_rcoset a (H : set A) : H <∘ a = coset.r a H := lemma grcoset_eq_rcoset a (H : set A) : H <∘ a = coset.r a H :=
begin begin
rewrite [↑grcoset, ↑coset.r, ↑image, ↑coset.rmul, ↑set_of], rewrite [↑grcoset, ↑coset.r, ↑image, ↑coset.rmul, ↑set_of],
apply setext, rewrite ↑mem, apply ext, rewrite ↑mem,
intro x, intro x,
apply iff.intro, apply iff.intro,
show H (x * a⁻¹) → (∃ (x_1 : A), H x_1 ∧ x_1 * a = x), from show H (x * a⁻¹) → (∃ (x_1 : A), H x_1 ∧ x_1 * a = x), from
@ -215,14 +215,14 @@ lemma subgroup_coset_id : ∀ a, a ∈ H → (a ∘> H = H ∧ H <∘ a = H) :=
assert Pr : H <∘ a ⊆ H, from closed_rcontract a H subg_mul_closed PHa, assert Pr : H <∘ a ⊆ H, from closed_rcontract a H subg_mul_closed PHa,
assert PHainv : H a⁻¹, from subg_has_inv a PHa, assert PHainv : H a⁻¹, from subg_has_inv a PHa,
and.intro and.intro
(setext (assume x, (ext (assume x,
begin begin
esimp [glcoset, mem], esimp [glcoset, mem],
apply iff.intro, apply iff.intro,
apply Pl, apply Pl,
intro PHx, exact (subg_mul_closed a⁻¹ x PHainv PHx) intro PHx, exact (subg_mul_closed a⁻¹ x PHainv PHx)
end)) end))
(setext (assume x, (ext (assume x,
begin begin
esimp [grcoset, mem], esimp [grcoset, mem],
apply iff.intro, apply iff.intro,