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

refactor(library/data): "union." ==> "union_", "inter." ==> "inter_"

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-01 16:13:44 -08:00
parent 4e2494f12e
commit 4f1415174e
9 changed files with 81 additions and 81 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
library/data/bag.lean
View file

@ -476,14 +476,14 @@ quot.induction_on₂ b₁ b₂ (λ l₁ l₂, by_cases
rewrite [count_eq_zero_of_not_mem n] rewrite [count_eq_zero_of_not_mem n]
end)) end))
lemma union.comm (b₁ b₂ : bag A) : b₁ ∪ b₂ = b₂ ∪ b₁ := lemma union_comm (b₁ b₂ : bag A) : b₁ ∪ b₂ = b₂ ∪ b₁ :=
bag.ext (λ a, by rewrite [*count_union, max.comm]) bag.ext (λ a, by rewrite [*count_union, max.comm])
lemma union.assoc (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∪ b₃ = b₁ ∪ (b₂ ∪ b₃) := lemma union_assoc (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∪ b₃ = b₁ ∪ (b₂ ∪ b₃) :=
bag.ext (λ a, by rewrite [*count_union, max.assoc]) bag.ext (λ a, by rewrite [*count_union, max.assoc])
theorem union.left_comm (s₁ s₂ s₃ : bag A) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) := theorem union_left_comm (s₁ s₂ s₃ : bag A) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
!left_comm union.comm union.assoc s₁ s₂ s₃ !left_comm union_comm union_assoc s₁ s₂ s₃
lemma union_self (b : bag A) : b ∪ b = b := lemma union_self (b : bag A) : b ∪ b = b :=
bag.ext (λ a, by rewrite [*count_union, max_self]) bag.ext (λ a, by rewrite [*count_union, max_self])
@ -492,17 +492,17 @@ lemma union_empty (b : bag A) : b ∪ empty = b :=
bag.ext (λ a, by rewrite [*count_union, count_empty, max_zero]) bag.ext (λ a, by rewrite [*count_union, count_empty, max_zero])
lemma empty_union (b : bag A) : empty ∪ b = b := lemma empty_union (b : bag A) : empty ∪ b = b :=
calc empty ∪ b = b ∪ empty : union.comm calc empty ∪ b = b ∪ empty : union_comm
... = b : union_empty ... = b : union_empty
lemma inter.comm (b₁ b₂ : bag A) : b₁ ∩ b₂ = b₂ ∩ b₁ := lemma inter_comm (b₁ b₂ : bag A) : b₁ ∩ b₂ = b₂ ∩ b₁ :=
bag.ext (λ a, by rewrite [*count_inter, min.comm]) bag.ext (λ a, by rewrite [*count_inter, min.comm])
lemma inter.assoc (b₁ b₂ b₃ : bag A) : (b₁ ∩ b₂) ∩ b₃ = b₁ ∩ (b₂ ∩ b₃) := lemma inter_assoc (b₁ b₂ b₃ : bag A) : (b₁ ∩ b₂) ∩ b₃ = b₁ ∩ (b₂ ∩ b₃) :=
bag.ext (λ a, by rewrite [*count_inter, min.assoc]) bag.ext (λ a, by rewrite [*count_inter, min.assoc])
theorem inter.left_comm (s₁ s₂ s₃ : bag A) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) := theorem inter_left_comm (s₁ s₂ s₃ : bag A) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
!left_comm inter.comm inter.assoc s₁ s₂ s₃ !left_comm inter_comm inter_assoc s₁ s₂ s₃
lemma inter_self (b : bag A) : b ∩ b = b := lemma inter_self (b : bag A) : b ∩ b = b :=
bag.ext (λ a, by rewrite [*count_inter, min_self]) bag.ext (λ a, by rewrite [*count_inter, min_self])
@ -511,7 +511,7 @@ lemma inter_empty (b : bag A) : b ∩ empty = empty :=
bag.ext (λ a, by rewrite [*count_inter, count_empty, min_zero]) bag.ext (λ a, by rewrite [*count_inter, count_empty, min_zero])
lemma empty_inter (b : bag A) : empty ∩ b = empty := lemma empty_inter (b : bag A) : empty ∩ b = empty :=
calc empty ∩ b = b ∩ empty : inter.comm calc empty ∩ b = b ∩ empty : inter_comm
... = empty : inter_empty ... = empty : inter_empty
lemma append_union_inter (b₁ b₂ : bag A) : (b₁ ∪ b₂) ++ (b₁ ∩ b₂) = b₁ ++ b₂ := lemma append_union_inter (b₁ b₂ : bag A) : (b₁ ∪ b₂) ++ (b₁ ∩ b₂) = b₁ ++ b₂ :=
@ -522,7 +522,7 @@ bag.ext (λ a, begin
{ intro H, rewrite [min_eq_right H, max_eq_left H, add.comm] } { intro H, rewrite [min_eq_right H, max_eq_left H, add.comm] }
end) end)
lemma inter.left_distrib (b₁ b₂ b₃ : bag A) : b₁ ∩ (b₂ ∪ b₃) = (b₁ ∩ b₂) ∪ (b₁ ∩ b₃) := lemma inter_left_distrib (b₁ b₂ b₃ : bag A) : b₁ ∩ (b₂ ∪ b₃) = (b₁ ∩ b₂) ∪ (b₁ ∩ b₃) :=
bag.ext (λ a, begin bag.ext (λ a, begin
rewrite [*count_inter, *count_union, *count_inter], rewrite [*count_inter, *count_union, *count_inter],
apply (@by_cases (count a b₁ ≤ count a b₂)), apply (@by_cases (count a b₁ ≤ count a b₂)),
@ -549,11 +549,11 @@ bag.ext (λ a, begin
rewrite [min.comm, min_eq_left_of_lt H₁₃, max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃)] } } rewrite [min.comm, min_eq_left_of_lt H₁₃, max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃)] } }
end) end)
lemma inter.right_distrib (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∩ b₃ = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) := lemma inter_right_distrib (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∩ b₃ = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) :=
calc (b₁ ∪ b₂) ∩ b₃ = b₃ ∩ (b₁ ∪ b₂) : inter.comm calc (b₁ ∪ b₂) ∩ b₃ = b₃ ∩ (b₁ ∪ b₂) : inter_comm
... = (b₃ ∩ b₁) ∪ (b₃ ∩ b₂) : inter.left_distrib ... = (b₃ ∩ b₁) ∪ (b₃ ∩ b₂) : inter_left_distrib
... = (b₁ ∩ b₃) ∪ (b₃ ∩ b₂) : inter.comm ... = (b₁ ∩ b₃) ∪ (b₃ ∩ b₂) : inter_comm
... = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) : inter.comm ... = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) : inter_comm
end union_inter end union_inter
section subbag section subbag

38
library/data/finset/basic.lean
View file

@ -363,17 +363,17 @@ iff.intro
theorem mem_union_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∪ s₂) = (a ∈ s₁ ∨ a ∈ s₂) := theorem mem_union_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∪ s₂) = (a ∈ s₁ ∨ a ∈ s₂) :=
propext !mem_union_iff propext !mem_union_iff
theorem union.comm (s₁ s₂ : finset A) : s₁ ∪ s₂ = s₂ ∪ s₁ := theorem union_comm (s₁ s₂ : finset A) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
ext (λ a, by rewrite [*mem_union_eq]; exact or.comm) ext (λ a, by rewrite [*mem_union_eq]; exact or.comm)
theorem union.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) := theorem union_assoc (s₁ s₂ s₃ : finset A) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
ext (λ a, by rewrite [*mem_union_eq]; exact or.assoc) ext (λ a, by rewrite [*mem_union_eq]; exact or.assoc)
theorem union.left_comm (s₁ s₂ s₃ : finset A) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) := theorem union_left_comm (s₁ s₂ s₃ : finset A) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
!left_comm union.comm union.assoc s₁ s₂ s₃ !left_comm union_comm union_assoc s₁ s₂ s₃
theorem union.right_comm (s₁ s₂ s₃ : finset A) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ := theorem union_right_comm (s₁ s₂ s₃ : finset A) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
!right_comm union.comm union.assoc s₁ s₂ s₃ !right_comm union_comm union_assoc s₁ s₂ s₃
theorem union_self (s : finset A) : s ∪ s = s := theorem union_self (s : finset A) : s ∪ s = s :=
ext (λ a, iff.intro ext (λ a, iff.intro
@ -386,14 +386,14 @@ ext (λ a, iff.intro
(suppose a ∈ s, mem_union_left _ this)) (suppose a ∈ s, mem_union_left _ this))
theorem empty_union (s : finset A) : ∅ ∪ s = s := theorem empty_union (s : finset A) : ∅ ∪ s = s :=
calc ∅ ∪ s = s ∪ ∅ : union.comm calc ∅ ∪ s = s ∪ ∅ : union_comm
... = s : union_empty ... = s : union_empty
theorem insert_eq (a : A) (s : finset A) : insert a s = '{a} ∪ s := theorem insert_eq (a : A) (s : finset A) : insert a s = '{a} ∪ s :=
ext (take x, by rewrite [mem_insert_iff, mem_union_iff, mem_singleton_iff]) ext (take x, by rewrite [mem_insert_iff, mem_union_iff, mem_singleton_iff])
theorem insert_union (a : A) (s t : finset A) : insert a (s ∪ t) = insert a s ∪ t := theorem insert_union (a : A) (s t : finset A) : insert a (s ∪ t) = insert a s ∪ t :=
by rewrite [insert_eq, insert_eq a s, union.assoc] by rewrite [insert_eq, insert_eq a s, union_assoc]
end union end union
/- inter -/ /- inter -/
@ -427,17 +427,17 @@ iff.intro
theorem mem_inter_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) := theorem mem_inter_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) :=
propext !mem_inter_iff propext !mem_inter_iff
theorem inter.comm (s₁ s₂ : finset A) : s₁ ∩ s₂ = s₂ ∩ s₁ := theorem inter_comm (s₁ s₂ : finset A) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm) ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm)
theorem inter.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) := theorem inter_assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc) ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc)
theorem inter.left_comm (s₁ s₂ s₃ : finset A) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) := theorem inter_left_comm (s₁ s₂ s₃ : finset A) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
!left_comm inter.comm inter.assoc s₁ s₂ s₃ !left_comm inter_comm inter_assoc s₁ s₂ s₃
theorem inter.right_comm (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ := theorem inter_right_comm (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
!right_comm inter.comm inter.assoc s₁ s₂ s₃ !right_comm inter_comm inter_assoc s₁ s₂ s₃
theorem inter_self (s : finset A) : s ∩ s = s := theorem inter_self (s : finset A) : s ∩ s = s :=
ext (λ a, iff.intro ext (λ a, iff.intro
@ -450,7 +450,7 @@ ext (λ a, iff.intro
(suppose a ∈ ∅, absurd this !not_mem_empty)) (suppose a ∈ ∅, absurd this !not_mem_empty))
theorem empty_inter (s : finset A) : ∅ ∩ s = ∅ := theorem empty_inter (s : finset A) : ∅ ∩ s = ∅ :=
calc ∅ ∩ s = s ∩ ∅ : inter.comm calc ∅ ∩ s = s ∩ ∅ : inter_comm
... = ∅ : inter_empty ... = ∅ : inter_empty
theorem singleton_inter_of_mem {a : A} {s : finset A} (H : a ∈ s) : theorem singleton_inter_of_mem {a : A} {s : finset A} (H : a ∈ s) :
@ -479,16 +479,16 @@ section inter
variable [h : decidable_eq A] variable [h : decidable_eq A]
include h include h
theorem inter.distrib_left (s t u : finset A) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) := theorem inter_distrib_left (s t u : finset A) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) :=
ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.left_distrib) ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.left_distrib)
theorem inter.distrib_right (s t u : finset A) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) := theorem inter_distrib_right (s t u : finset A) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) :=
ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.right_distrib) ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.right_distrib)
theorem union.distrib_left (s t u : finset A) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) := theorem union_distrib_left (s t u : finset A) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) :=
ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.left_distrib) ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.left_distrib)
theorem union.distrib_right (s t u : finset A) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) := theorem union_distrib_right (s t u : finset A) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) :=
ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.right_distrib) ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.right_distrib)
end inter end inter

6
library/data/finset/bigops.lean
View file

@ -22,11 +22,11 @@ definition to_comm_monoid_Union (B : Type) [decidable_eq B] :
comm_monoid (finset B) := comm_monoid (finset B) :=
⦃ comm_monoid, ⦃ comm_monoid,
mul := union, mul := union,
mul_assoc := union.assoc, mul_assoc := union_assoc,
one := empty, one := empty,
mul_one := union_empty, mul_one := union_empty,
one_mul := empty_union, one_mul := empty_union,
mul_comm := union.comm mul_comm := union_comm
⦄ ⦄
local attribute finset.to_comm_monoid_Union [instance] local attribute finset.to_comm_monoid_Union [instance]
@ -77,7 +77,7 @@ section deceqA
begin begin
induction t with s' x H IH, induction t with s' x H IH,
rewrite [*Union_empty, inter_empty], rewrite [*Union_empty, inter_empty],
rewrite [*Union_insert_of_not_mem _ H, inter.distrib_left, IH], rewrite [*Union_insert_of_not_mem _ H, inter_distrib_left, IH],
end end
theorem mem_Union_iff (s : finset A) (f : A → finset B) (b : B) : theorem mem_Union_iff (s : finset A) (f : A → finset B) (b : B) :

8
library/data/finset/card.lean
View file

@ -24,8 +24,8 @@ begin
(assume as1 : a ∈ s₁, (assume as1 : a ∈ s₁,
assert H : a ∉ s₁ ∩ s₂, from assume H', ans2 (mem_of_mem_inter_right H'), assert H : a ∉ s₁ ∩ s₂, from assume H', ans2 (mem_of_mem_inter_right H'),
begin begin
rewrite [card_insert_of_not_mem ans2, union.comm, -insert_union, union.comm], rewrite [card_insert_of_not_mem ans2, union_comm, -insert_union, union_comm],
rewrite [insert_union, insert_eq_of_mem as1, insert_eq, inter.distrib_left, inter.comm], rewrite [insert_union, insert_eq_of_mem as1, insert_eq, inter_distrib_left, inter_comm],
rewrite [singleton_inter_of_mem as1, -insert_eq, card_insert_of_not_mem H, -*add.assoc], rewrite [singleton_inter_of_mem as1, -insert_eq, card_insert_of_not_mem H, -*add.assoc],
rewrite IH rewrite IH
end) end)
@ -33,8 +33,8 @@ begin
assert H : a ∉ s₁ ∪ s₂, from assume H', assert H : a ∉ s₁ ∪ s₂, from assume H',
or.elim (mem_or_mem_of_mem_union H') (assume as1, ans1 as1) (assume as2, ans2 as2), or.elim (mem_or_mem_of_mem_union H') (assume as1, ans1 as1) (assume as2, ans2 as2),
begin begin
rewrite [card_insert_of_not_mem ans2, union.comm, -insert_union, union.comm], rewrite [card_insert_of_not_mem ans2, union_comm, -insert_union, union_comm],
rewrite [card_insert_of_not_mem H, insert_eq, inter.distrib_left, inter.comm], rewrite [card_insert_of_not_mem H, insert_eq, inter_distrib_left, inter_comm],
rewrite [singleton_inter_of_not_mem ans1, empty_union, add.right_comm], rewrite [singleton_inter_of_not_mem ans1, empty_union, add.right_comm],
rewrite [-add.assoc, IH] rewrite [-add.assoc, IH]
end) end)

4
library/data/finset/comb.lean
View file

@ -206,7 +206,7 @@ ext (take x, iff.intro
(suppose x ∉ s, mem_union_right _ (mem_diff `x ∈ t` this)))) (suppose x ∉ s, mem_union_right _ (mem_diff `x ∈ t` this))))
theorem diff_union_cancel {s t : finset A} (H : s ⊆ t) : (t \ s) ∪ s = t := theorem diff_union_cancel {s t : finset A} (H : s ⊆ t) : (t \ s) ∪ s = t :=
eq.subst !union.comm (!union_diff_cancel H) eq.subst !union_comm (!union_diff_cancel H)
end diff end diff
/- set complement -/ /- set complement -/
@ -414,7 +414,7 @@ perm.induction_on p
rfl rfl
(λ x l₁ l₂ p ih, by rewrite [↑list_powerset, ih]) (λ x l₁ l₂ p ih, by rewrite [↑list_powerset, ih])
(λ x y l, by rewrite [↑list_powerset, ↑list_powerset, *image_union, image_insert_comm, (λ x y l, by rewrite [↑list_powerset, ↑list_powerset, *image_union, image_insert_comm,
*union.assoc, union.left_comm (finset.image (finset.insert x) _)]) *union_assoc, union_left_comm (finset.image (finset.insert x) _)])
(λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, eq.trans r₁ r₂) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, eq.trans r₁ r₂)
definition powerset (s : finset A) : finset (finset A) := definition powerset (s : finset A) : finset (finset A) :=

28
library/data/hf.lean
View file

@ -181,17 +181,17 @@ iff.intro
theorem mem_union_eq {a : hf} (s₁ s₂ : hf) : (a ∈ s₁ ∪ s₂) = (a ∈ s₁ ∨ a ∈ s₂) := theorem mem_union_eq {a : hf} (s₁ s₂ : hf) : (a ∈ s₁ ∪ s₂) = (a ∈ s₁ ∨ a ∈ s₂) :=
propext !mem_union_iff propext !mem_union_iff
theorem union.comm (s₁ s₂ : hf) : s₁ ∪ s₂ = s₂ ∪ s₁ := theorem union_comm (s₁ s₂ : hf) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
hf.ext (λ a, by rewrite [*mem_union_eq]; exact or.comm) hf.ext (λ a, by rewrite [*mem_union_eq]; exact or.comm)
theorem union.assoc (s₁ s₂ s₃ : hf) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) := theorem union_assoc (s₁ s₂ s₃ : hf) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
hf.ext (λ a, by rewrite [*mem_union_eq]; exact or.assoc) hf.ext (λ a, by rewrite [*mem_union_eq]; exact or.assoc)
theorem union.left_comm (s₁ s₂ s₃ : hf) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) := theorem union_left_comm (s₁ s₂ s₃ : hf) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
!left_comm union.comm union.assoc s₁ s₂ s₃ !left_comm union_comm union_assoc s₁ s₂ s₃
theorem union.right_comm (s₁ s₂ s₃ : hf) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ := theorem union_right_comm (s₁ s₂ s₃ : hf) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
!right_comm union.comm union.assoc s₁ s₂ s₃ !right_comm union_comm union_assoc s₁ s₂ s₃
theorem union_self (s : hf) : s ∪ s = s := theorem union_self (s : hf) : s ∪ s = s :=
hf.ext (λ a, iff.intro hf.ext (λ a, iff.intro
@ -204,7 +204,7 @@ hf.ext (λ a, iff.intro
(suppose a ∈ s, mem_union_left _ this)) (suppose a ∈ s, mem_union_left _ this))
theorem empty_union (s : hf) : ∅ ∪ s = s := theorem empty_union (s : hf) : ∅ ∪ s = s :=
calc ∅ ∪ s = s ∪ ∅ : union.comm calc ∅ ∪ s = s ∪ ∅ : union_comm
... = s : union_empty ... = s : union_empty
/- inter -/ /- inter -/
@ -230,17 +230,17 @@ iff.intro
theorem mem_inter_eq (a : hf) (s₁ s₂ : hf) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) := theorem mem_inter_eq (a : hf) (s₁ s₂ : hf) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) :=
propext !mem_inter_iff propext !mem_inter_iff
theorem inter.comm (s₁ s₂ : hf) : s₁ ∩ s₂ = s₂ ∩ s₁ := theorem inter_comm (s₁ s₂ : hf) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
hf.ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm) hf.ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm)
theorem inter.assoc (s₁ s₂ s₃ : hf) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) := theorem inter_assoc (s₁ s₂ s₃ : hf) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
hf.ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc) hf.ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc)
theorem inter.left_comm (s₁ s₂ s₃ : hf) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) := theorem inter_left_comm (s₁ s₂ s₃ : hf) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
!left_comm inter.comm inter.assoc s₁ s₂ s₃ !left_comm inter_comm inter_assoc s₁ s₂ s₃
theorem inter.right_comm (s₁ s₂ s₃ : hf) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ := theorem inter_right_comm (s₁ s₂ s₃ : hf) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
!right_comm inter.comm inter.assoc s₁ s₂ s₃ !right_comm inter_comm inter_assoc s₁ s₂ s₃
theorem inter_self (s : hf) : s ∩ s = s := theorem inter_self (s : hf) : s ∩ s = s :=
hf.ext (λ a, iff.intro hf.ext (λ a, iff.intro
@ -253,7 +253,7 @@ hf.ext (λ a, iff.intro
(suppose a ∈ ∅, absurd this !not_mem_empty)) (suppose a ∈ ∅, absurd this !not_mem_empty))
theorem empty_inter (s : hf) : ∅ ∩ s = ∅ := theorem empty_inter (s : hf) : ∅ ∩ s = ∅ :=
calc ∅ ∩ s = s ∩ ∅ : inter.comm calc ∅ ∩ s = s ∩ ∅ : inter_comm
... = ∅ : inter_empty ... = ∅ : inter_empty
/- card -/ /- card -/

32
library/data/set/basic.lean
View file

@ -153,17 +153,17 @@ ext (take x, !or_false)
theorem empty_union (a : set X) : ∅ ∪ a = a := theorem empty_union (a : set X) : ∅ ∪ a = a :=
ext (take x, !false_or) ext (take x, !false_or)
theorem union.comm (a b : set X) : a ∪ b = b ∪ a := theorem union_comm (a b : set X) : a ∪ b = b ∪ a :=
ext (take x, or.comm) ext (take x, or.comm)
theorem union.assoc (a b c : set X) : (a ∪ b) ∪ c = a ∪ (b ∪ c) := theorem union_assoc (a b c : set X) : (a ∪ b) ∪ c = a ∪ (b ∪ c) :=
ext (take x, or.assoc) ext (take x, or.assoc)
theorem union.left_comm (s₁ s₂ s₃ : set X) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) := theorem union_left_comm (s₁ s₂ s₃ : set X) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
!left_comm union.comm union.assoc s₁ s₂ s₃ !left_comm union_comm union_assoc s₁ s₂ s₃
theorem union.right_comm (s₁ s₂ s₃ : set X) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ := theorem union_right_comm (s₁ s₂ s₃ : set X) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
!right_comm union.comm union.assoc s₁ s₂ s₃ !right_comm union_comm union_assoc s₁ s₂ s₃
theorem subset_union_left (s t : set X) : s ⊆ s ∪ t := λ x H, or.inl H theorem subset_union_left (s t : set X) : s ⊆ s ∪ t := λ x H, or.inl H
@ -199,17 +199,17 @@ ext (take x, !and_false)
theorem empty_inter (a : set X) : ∅ ∩ a = ∅ := theorem empty_inter (a : set X) : ∅ ∩ a = ∅ :=
ext (take x, !false_and) ext (take x, !false_and)
theorem inter.comm (a b : set X) : a ∩ b = b ∩ a := theorem inter_comm (a b : set X) : a ∩ b = b ∩ a :=
ext (take x, !and.comm) ext (take x, !and.comm)
theorem inter.assoc (a b c : set X) : (a ∩ b) ∩ c = a ∩ (b ∩ c) := theorem inter_assoc (a b c : set X) : (a ∩ b) ∩ c = a ∩ (b ∩ c) :=
ext (take x, !and.assoc) ext (take x, !and.assoc)
theorem inter.left_comm (s₁ s₂ s₃ : set X) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) := theorem inter_left_comm (s₁ s₂ s₃ : set X) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
!left_comm inter.comm inter.assoc s₁ s₂ s₃ !left_comm inter_comm inter_assoc s₁ s₂ s₃
theorem inter.right_comm (s₁ s₂ s₃ : set X) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ := theorem inter_right_comm (s₁ s₂ s₃ : set X) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
!right_comm inter.comm inter.assoc s₁ s₂ s₃ !right_comm inter_comm inter_assoc s₁ s₂ s₃
theorem inter_univ (a : set X) : a ∩ univ = a := theorem inter_univ (a : set X) : a ∩ univ = a :=
ext (take x, !and_true) ext (take x, !and_true)
@ -226,16 +226,16 @@ theorem subset_inter {s t r : set X} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩
/- distributivity laws -/ /- distributivity laws -/
theorem inter.distrib_left (s t u : set X) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) := theorem inter_distrib_left (s t u : set X) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) :=
ext (take x, !and.left_distrib) ext (take x, !and.left_distrib)
theorem inter.distrib_right (s t u : set X) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) := theorem inter_distrib_right (s t u : set X) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) :=
ext (take x, !and.right_distrib) ext (take x, !and.right_distrib)
theorem union.distrib_left (s t u : set X) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) := theorem union_distrib_left (s t u : set X) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) :=
ext (take x, !or.left_distrib) ext (take x, !or.left_distrib)
theorem union.distrib_right (s t u : set X) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) := theorem union_distrib_right (s t u : set X) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) :=
ext (take x, !or.right_distrib) ext (take x, !or.right_distrib)
/- set-builder notation -/ /- set-builder notation -/

12
library/data/set/comm_semiring.lean
View file

@ -14,16 +14,16 @@ definition set_comm_semiring [instance] (A : Type) : comm_semiring (set A) :=
mul := inter, mul := inter,
zero := empty, zero := empty,
one := univ, one := univ,
add_assoc := union.assoc, add_assoc := union_assoc,
add_comm := union.comm, add_comm := union_comm,
zero_add := empty_union, zero_add := empty_union,
add_zero := union_empty, add_zero := union_empty,
mul_assoc := inter.assoc, mul_assoc := inter_assoc,
mul_comm := inter.comm, mul_comm := inter_comm,
zero_mul := empty_inter, zero_mul := empty_inter,
mul_zero := inter_empty, mul_zero := inter_empty,
one_mul := univ_inter, one_mul := univ_inter,
mul_one := inter_univ, mul_one := inter_univ,
left_distrib := inter.distrib_left, left_distrib := inter_distrib_left,
right_distrib := inter.distrib_right right_distrib := inter_distrib_right
⦄ ⦄

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

@ -169,7 +169,7 @@ definition inf (F₁ F₂ : filter A) : filter A :=
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Ha' : a ⊇ a₁ ∩ a₂)]]], from Ha, obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Ha' : a ⊇ a₁ ∩ a₂)]]], from Ha,
obtain b₁ [b₁F₁ [b₂ [b₂F₂ (Hb' : b ⊇ b₁ ∩ b₂)]]], from Hb, obtain b₁ [b₁F₁ [b₂ [b₂F₂ (Hb' : b ⊇ b₁ ∩ b₂)]]], from Hb,
assert a₁ ∩ b₁ ∩ (a₂ ∩ b₂) = a₁ ∩ a₂ ∩ (b₁ ∩ b₂), assert a₁ ∩ b₁ ∩ (a₂ ∩ b₂) = a₁ ∩ a₂ ∩ (b₁ ∩ b₂),
by rewrite [*inter.assoc, inter.left_comm b₁], by rewrite [*inter_assoc, inter_left_comm b₁],
have a ∩ b ⊇ a₁ ∩ b₁ ∩ (a₂ ∩ b₂), have a ∩ b ⊇ a₁ ∩ b₁ ∩ (a₂ ∩ b₂),
begin begin
rewrite this, rewrite this,