r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Enderton. Fix exercise names.

finite-set-exercises
Joshua Potter 2023-06-29 14:53:36 -06:00
parent 92b52ef1b8
commit c65e28888d
3 changed files with 1069 additions and 1087 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1982
Bookshelf/Enderton/Set.tex
View File

File diff suppressed because it is too large Load Diff

112
Bookshelf/Enderton/Set/Chapter_2.lean
View File

@ -13,13 +13,13 @@ Axioms and Operations
namespace Enderton.Set.Chapter_2 namespace Enderton.Set.Chapter_2
/-- ### Exercise 3.1 /-- ### Exercise 2.1
Assume that `A` is the set of integers divisible by `4`. Similarly assume that Assume that `A` is the set of integers divisible by `4`. Similarly assume that
`B` and `C` are the sets of integers divisible by `9` and `10`, respectively. `B` and `C` are the sets of integers divisible by `9` and `10`, respectively.
What is in `A ∩ B ∩ C`? What is in `A ∩ B ∩ C`?
-/ -/
theorem exercise_3_1 {A B C : Set ℤ} theorem exercise_2_1 {A B C : Set ℤ}
(hA : A = { x | Dvd.dvd 4 x }) (hA : A = { x | Dvd.dvd 4 x })
(hB : B = { x | Dvd.dvd 9 x }) (hB : B = { x | Dvd.dvd 9 x })
(hC : C = { x | Dvd.dvd 10 x }) (hC : C = { x | Dvd.dvd 10 x })
@ -35,11 +35,11 @@ theorem exercise_3_1 {A B C : Set ℤ}
· rw [hC] at hc · rw [hC] at hc
exact Set.mem_setOf.mp hc exact Set.mem_setOf.mp hc
/-- ### Exercise 3.2 /-- ### Exercise 2.2
Give an example of sets `A` and `B` for which `⋃ A = ⋃ B` but `A ≠ B`. Give an example of sets `A` and `B` for which `⋃ A = ⋃ B` but `A ≠ B`.
-/ -/
theorem exercise_3_2 {A B : Set (Set ℕ)} theorem exercise_2_2 {A B : Set (Set ℕ)}
(hA : A = {{1}, {2}}) (hB : B = {{1, 2}}) (hA : A = {{1}, {2}}) (hB : B = {{1, 2}})
: Set.sUnion A = Set.sUnion B ∧ A ≠ B := by : Set.sUnion A = Set.sUnion B ∧ A ≠ B := by
apply And.intro apply And.intro
@ -74,12 +74,12 @@ theorem exercise_3_2 {A B : Set (Set ℕ)}
have h₂ := h₁ 2 have h₂ := h₁ 2
simp at h₂ simp at h₂
/-- ### Exercise 3.3 /-- ### Exercise 2.3
Show that every member of a set `A` is a subset of `U A`. (This was stated as an Show that every member of a set `A` is a subset of `U A`. (This was stated as an
example in this section.) example in this section.)
-/ -/
theorem exercise_3_3 {A : Set (Set α)} theorem exercise_2_3 {A : Set (Set α)}
: ∀ x ∈ A, x ⊆ ⋃₀ A := by : ∀ x ∈ A, x ⊆ ⋃₀ A := by
intro x hx intro x hx
show ∀ y ∈ x, y ∈ { a | ∃ t, t ∈ A ∧ a ∈ t } show ∀ y ∈ x, y ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }
@ -87,11 +87,11 @@ theorem exercise_3_3 {A : Set (Set α)}
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact ⟨x, ⟨hx, hy⟩⟩ exact ⟨x, ⟨hx, hy⟩⟩
/-- ### Exercise 3.4 /-- ### Exercise 2.4
Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`. Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`.
-/ -/
theorem exercise_3_4 {A B : Set (Set α)} (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by theorem exercise_2_4 {A B : Set (Set α)} (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B := by
show ∀ x ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }, x ∈ { a | ∃ t, t ∈ B ∧ a ∈ t } show ∀ x ∈ { a | ∃ t, t ∈ A ∧ a ∈ t }, x ∈ { a | ∃ t, t ∈ B ∧ a ∈ t }
intro x hx intro x hx
rw [Set.mem_setOf_eq] at hx rw [Set.mem_setOf_eq] at hx
@ -99,11 +99,11 @@ theorem exercise_3_4 {A B : Set (Set α)} (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact ⟨t, ⟨h ht, hxt⟩⟩ exact ⟨t, ⟨h ht, hxt⟩⟩
/-- ### Exercise 3.5 /-- ### Exercise 2.5
Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`. Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`.
-/ -/
theorem exercise_3_5 {𝓐 : Set (Set α)} (h : ∀ x ∈ 𝓐, x ⊆ B) theorem exercise_2_5 {𝓐 : Set (Set α)} (h : ∀ x ∈ 𝓐, x ⊆ B)
: ⋃₀ 𝓐 ⊆ B := by : ⋃₀ 𝓐 ⊆ B := by
show ∀ y ∈ { a | ∃ t, t ∈ 𝓐 ∧ a ∈ t }, y ∈ B show ∀ y ∈ { a | ∃ t, t ∈ 𝓐 ∧ a ∈ t }, y ∈ B
intro y hy intro y hy
@ -111,11 +111,11 @@ theorem exercise_3_5 {𝓐 : Set (Set α)} (h : ∀ x ∈ 𝓐, x ⊆ B)
have ⟨t, ⟨ht𝓐, hyt⟩⟩ := hy have ⟨t, ⟨ht𝓐, hyt⟩⟩ := hy
exact (h t ht𝓐) hyt exact (h t ht𝓐) hyt
/-- ### Exercise 3.6a /-- ### Exercise 2.6a
Show that for any set `A`, `⋃ 𝓟 A = A`. Show that for any set `A`, `⋃ 𝓟 A = A`.
-/ -/
theorem exercise_3_6a : ⋃₀ (𝒫 A) = A := by theorem exercise_2_6a : ⋃₀ (𝒫 A) = A := by
show { a | ∃ t, t ∈ { t | t ⊆ A } ∧ a ∈ t } = A show { a | ∃ t, t ∈ { t | t ⊆ A } ∧ a ∈ t } = A
ext x ext x
apply Iff.intro apply Iff.intro
@ -128,30 +128,30 @@ theorem exercise_3_6a : ⋃₀ (𝒫 A) = A := by
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact ⟨A, ⟨by rw [Set.mem_setOf_eq], hx⟩⟩ exact ⟨A, ⟨by rw [Set.mem_setOf_eq], hx⟩⟩
/-- ### Exercise 3.6b /-- ### Exercise 2.6b
Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold? Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold?
-/ -/
theorem exercise_3_6b theorem exercise_2_6b
: A ⊆ 𝒫 (⋃₀ A) : A ⊆ 𝒫 (⋃₀ A)
∧ (A = 𝒫 (⋃₀ A) ↔ ∃ B, A = 𝒫 B) := by ∧ (A = 𝒫 (⋃₀ A) ↔ ∃ B, A = 𝒫 B) := by
apply And.intro apply And.intro
· show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A } · show ∀ x ∈ A, x ∈ { t | t ⊆ ⋃₀ A }
intro x hx intro x hx
rw [Set.mem_setOf] rw [Set.mem_setOf]
exact exercise_3_3 x hx exact exercise_2_3 x hx
· apply Iff.intro · apply Iff.intro
· intro hA · intro hA
exact ⟨⋃₀ A, hA⟩ exact ⟨⋃₀ A, hA⟩
· intro ⟨B, hB⟩ · intro ⟨B, hB⟩
conv => rhs; rw [hB, exercise_3_6a] conv => rhs; rw [hB, exercise_2_6a]
exact hB exact hB
/-- ### Exercise 3.7a /-- ### Exercise 2.7a
Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`. Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`.
-/ -/
theorem exercise_3_7A theorem exercise_2_7A
: 𝒫 A ∩ 𝒫 B = 𝒫 (A ∩ B) := by : 𝒫 A ∩ 𝒫 B = 𝒫 (A ∩ B) := by
suffices 𝒫 A ∩ 𝒫 B ⊆ 𝒫 (A ∩ B) ∧ 𝒫 (A ∩ B) ⊆ 𝒫 A ∩ 𝒫 B from suffices 𝒫 A ∩ 𝒫 B ⊆ 𝒫 (A ∩ B) ∧ 𝒫 (A ∩ B) ⊆ 𝒫 A ∩ 𝒫 B from
subset_antisymm this.left this.right subset_antisymm this.left this.right
@ -167,11 +167,11 @@ theorem exercise_3_7A
-- theorem false_of_false_iff_true : (false ↔ true) → false := by simp -- theorem false_of_false_iff_true : (false ↔ true) → false := by simp
/-- ### Exercise 3.7b (i) /-- ### Exercise 2.7b (i)
Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`. Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`.
-/ -/
theorem exercise_3_7b_i theorem exercise_2_7b_i
: 𝒫 A ∪ 𝒫 B ⊆ 𝒫 (A ∪ B) := by : 𝒫 A ∪ 𝒫 B ⊆ 𝒫 (A ∪ B) := by
unfold Set.powerset unfold Set.powerset
intro x hx intro x hx
@ -184,11 +184,11 @@ theorem exercise_3_7b_i
rw [Set.mem_setOf_eq] rw [Set.mem_setOf_eq]
exact Set.subset_union_of_subset_right hB A exact Set.subset_union_of_subset_right hB A
/-- ### Exercise 3.7b (ii) /-- ### Exercise 2.7b (ii)
Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.? Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.?
-/ -/
theorem exercise_3_7b_ii theorem exercise_2_7b_ii
: 𝒫 A ∪ 𝒫 B = 𝒫 (A ∪ B) ↔ A ⊆ B ∨ B ⊆ A := by : 𝒫 A ∪ 𝒫 B = 𝒫 (A ∪ B) ↔ A ⊆ B ∨ B ⊆ A := by
unfold Set.powerset unfold Set.powerset
apply Iff.intro apply Iff.intro
@ -236,11 +236,11 @@ theorem exercise_3_7b_ii
refine Or.inl (Set.Subset.trans hx ?_) refine Or.inl (Set.Subset.trans hx ?_)
exact subset_of_eq (Set.right_subset_union_eq_self hB) exact subset_of_eq (Set.right_subset_union_eq_self hB)
/-- ### Exercise 3.9 /-- ### Exercise 2.9
Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`. Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`.
-/ -/
theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}}) theorem exercise_2_9 (ha : a = {1}) (hB : B = {{1}})
: a ∈ B ∧ 𝒫 a ∉ 𝒫 B := by : a ∈ B ∧ 𝒫 a ∉ 𝒫 B := by
apply And.intro apply And.intro
· rw [ha, hB] · rw [ha, hB]
@ -264,24 +264,24 @@ theorem exercise_3_9 (ha : a = {1}) (hB : B = {{1}})
have := h 1 have := h 1
simp at this simp at this
/-- ### Exercise 3.10 /-- ### Exercise 2.10
Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`. Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`.
-/ -/
theorem exercise_3_10 {B : Set (Set α)} (ha : a ∈ B) theorem exercise_2_10 {B : Set (Set α)} (ha : a ∈ B)
: 𝒫 a ∈ 𝒫 (𝒫 (⋃₀ B)) := by : 𝒫 a ∈ 𝒫 (𝒫 (⋃₀ B)) := by
have h₁ := exercise_3_3 a ha have h₁ := exercise_2_3 a ha
have h₂ := Chapter_1.exercise_1_3 h₁ have h₂ := Chapter_1.exercise_1_3 h₁
generalize hb : 𝒫 (⋃₀ B) = b generalize hb : 𝒫 (⋃₀ B) = b
conv => rhs; unfold Set.powerset conv => rhs; unfold Set.powerset
rw [← hb, Set.mem_setOf_eq] rw [← hb, Set.mem_setOf_eq]
exact h₂ exact h₂
/-- ### Exercise 4.11 (i) /-- ### Exercise 2.11 (i)
Show that for any sets `A` and `B`, `A = (A ∩ B) ∪ (A - B)`. Show that for any sets `A` and `B`, `A = (A ∩ B) ∪ (A - B)`.
-/ -/
theorem exercise_4_11_i {A B : Set α} theorem exercise_2_11_i {A B : Set α}
: A = (A ∩ B) ∪ (A \ B) := by : A = (A ∩ B) ∪ (A \ B) := by
show A = fun a => A a ∧ B a ∨ A a ∧ ¬B a show A = fun a => A a ∧ B a ∨ A a ∧ ¬B a
suffices ∀ x, (A x ∧ (B x ∨ ¬B x)) = A x by suffices ∀ x, (A x ∧ (B x ∨ ¬B x)) = A x by
@ -294,11 +294,11 @@ theorem exercise_4_11_i {A B : Set α}
· intro hx · intro hx
exact ⟨hx, em (B x)⟩ exact ⟨hx, em (B x)⟩
/-- ### Exercise 4.11 (ii) /-- ### Exercise 2.11 (ii)
Show that for any sets `A` and `B`, `A ∪ (B - A) = A ∪ B`. Show that for any sets `A` and `B`, `A ∪ (B - A) = A ∪ B`.
-/ -/
theorem exercise_4_11_ii {A B : Set α} theorem exercise_2_11_ii {A B : Set α}
: A ∪ (B \ A) = A ∪ B := by : A ∪ (B \ A) = A ∪ B := by
show (fun a => A a ∨ B a ∧ ¬A a) = fun a => A a ∨ B a show (fun a => A a ∨ B a ∧ ¬A a) = fun a => A a ∨ B a
suffices ∀ x, ((A x ∨ B x) ∧ (A x ∨ ¬A x)) = (A x ∨ B x) by suffices ∀ x, ((A x ∨ B x) ∧ (A x ∨ ¬A x)) = (A x ∨ B x) by
@ -388,12 +388,12 @@ lemma left_diff_eq_singleton_one : (A \ B) \ C = {1} := by
| inl y => rw [hx] at y; simp at y | inl y => rw [hx] at y; simp at y
| inr y => rw [hx] at y; simp at y | inr y => rw [hx] at y; simp at y
/-- ### Exercise 4.14 /-- ### Exercise 2.14
Show by example that for some sets `A`, `B`, and `C`, the set `A - (B - C)` is Show by example that for some sets `A`, `B`, and `C`, the set `A - (B - C)` is
different from `(A - B) - C`. different from `(A - B) - C`.
-/ -/
theorem exercise_4_14 : A \ (B \ C) ≠ (A \ B) \ C := by theorem exercise_2_14 : A \ (B \ C) ≠ (A \ B) \ C := by
rw [ rw [
@right_diff_eq_insert_one_three A B C hA hB hC, @right_diff_eq_insert_one_three A B C hA hB hC,
@left_diff_eq_singleton_one A B C hA hB hC @left_diff_eq_singleton_one A B C hA hB hC
@ -405,19 +405,19 @@ theorem exercise_4_14 : A \ (B \ C) ≠ (A \ B) \ C := by
end end
/-- ### Exercise 4.16 /-- ### Exercise 2.16
Simplify: Simplify:
`[(A ∪ B ∪ C) ∩ (A ∪ B)] - [(A ∪ (B - C)) ∩ A]` `[(A ∪ B ∪ C) ∩ (A ∪ B)] - [(A ∪ (B - C)) ∩ A]`
-/ -/
theorem exercise_4_16 {A B C : Set α} theorem exercise_2_16 {A B C : Set α}
: ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A) = B \ A := by : ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A) = B \ A := by
calc ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A) calc ((A ∪ B ∪ C) ∩ (A ∪ B)) \ ((A ∪ (B \ C)) ∩ A)
_ = (A ∪ B) \ ((A ∪ (B \ C)) ∩ A) := by rw [Set.union_inter_cancel_left] _ = (A ∪ B) \ ((A ∪ (B \ C)) ∩ A) := by rw [Set.union_inter_cancel_left]
_ = (A ∪ B) \ A := by rw [Set.union_inter_cancel_left] _ = (A ∪ B) \ A := by rw [Set.union_inter_cancel_left]
_ = B \ A := by rw [Set.union_diff_left] _ = B \ A := by rw [Set.union_diff_left]
/-! ### Exercise 4.17 /-! ### Exercise 2.17
Show that the following four conditions are equivalent. Show that the following four conditions are equivalent.
@ -427,7 +427,7 @@ Show that the following four conditions are equivalent.
(d) `A ∩ B = A` (d) `A ∩ B = A`
-/ -/
theorem exercise_4_17_i {A B : Set α} (h : A ⊆ B) theorem exercise_2_17_i {A B : Set α} (h : A ⊆ B)
: A \ B = ∅ := by : A \ B = ∅ := by
ext x ext x
apply Iff.intro apply Iff.intro
@ -436,7 +436,7 @@ theorem exercise_4_17_i {A B : Set α} (h : A ⊆ B)
· intro hx · intro hx
exact False.elim hx exact False.elim hx
theorem exercise_4_17_ii {A B : Set α} (h : A \ B = ∅) theorem exercise_2_17_ii {A B : Set α} (h : A \ B = ∅)
: A ∪ B = B := by : A ∪ B = B := by
suffices A ⊆ B from Set.left_subset_union_eq_self this suffices A ⊆ B from Set.left_subset_union_eq_self this
show ∀ t, t ∈ A → t ∈ B show ∀ t, t ∈ A → t ∈ B
@ -445,19 +445,19 @@ theorem exercise_4_17_ii {A B : Set α} (h : A \ B = ∅)
by_contra nt by_contra nt
exact (h t).mp ⟨ht, nt⟩ exact (h t).mp ⟨ht, nt⟩
theorem exercise_4_17_iii {A B : Set α} (h : A ∪ B = B) theorem exercise_2_17_iii {A B : Set α} (h : A ∪ B = B)
: A ∩ B = A := by : A ∩ B = A := by
suffices A ⊆ B from Set.inter_eq_left_iff_subset.mpr this suffices A ⊆ B from Set.inter_eq_left_iff_subset.mpr this
exact Set.union_eq_right_iff_subset.mp h exact Set.union_eq_right_iff_subset.mp h
theorem exercise_4_17_iv {A B : Set α} (h : A ∩ B = A) theorem exercise_2_17_iv {A B : Set α} (h : A ∩ B = A)
: A ⊆ B := Set.inter_eq_left_iff_subset.mp h : A ⊆ B := Set.inter_eq_left_iff_subset.mp h
/-- ### Exercise 4.19 /-- ### Exercise 2.19
Is `𝒫 (A - B)` always equal to `𝒫 A - 𝒫 B`? Is it ever equal to `𝒫 A - 𝒫 B`? Is `𝒫 (A - B)` always equal to `𝒫 A - 𝒫 B`? Is it ever equal to `𝒫 A - 𝒫 B`?
-/ -/
theorem exercise_4_19 {A B : Set α} theorem exercise_2_19 {A B : Set α}
: 𝒫 (A \ B) ≠ (𝒫 A) \ (𝒫 B) := by : 𝒫 (A \ B) ≠ (𝒫 A) \ (𝒫 B) := by
intro h intro h
have he : ∅ ∈ 𝒫 (A \ B) := by simp have he : ∅ ∈ 𝒫 (A \ B) := by simp
@ -466,12 +466,12 @@ theorem exercise_4_19 {A B : Set α}
have := h ∅ have := h ∅
exact absurd (this.mp he) ne exact absurd (this.mp he) ne
/-- ### Exercise 4.20 /-- ### Exercise 2.20
Let `A`, `B`, and `C` be sets such that `A ∪ B = A ∪ C` and `A ∩ B = A ∩ C`. Let `A`, `B`, and `C` be sets such that `A ∪ B = A ∪ C` and `A ∩ B = A ∩ C`.
Show that `B = C`. Show that `B = C`.
-/ -/
theorem exercise_4_20 {A B C : Set α} theorem exercise_2_20 {A B C : Set α}
(hu : A ∪ B = A ∪ C) (hi : A ∩ B = A ∩ C) : B = C := by (hu : A ∪ B = A ∪ C) (hi : A ∩ B = A ∩ C) : B = C := by
ext x ext x
apply Iff.intro apply Iff.intro
@ -492,11 +492,11 @@ theorem exercise_4_20 {A B C : Set α}
rw [← hu] at this rw [← hu] at this
exact Or.elim this (absurd · hA) (by simp) exact Or.elim this (absurd · hA) (by simp)
/-- ### Exercise 4.21 /-- ### Exercise 2.21
Show that `⋃ (A ∪ B) = (⋃ A) ∪ (⋃ B)`. Show that `⋃ (A ∪ B) = (⋃ A) ∪ (⋃ B)`.
-/ -/
theorem exercise_4_21 {A B : Set (Set α)} theorem exercise_2_21 {A B : Set (Set α)}
: ⋃₀ (A ∪ B) = (⋃₀ A) ∪ (⋃₀ B) := by : ⋃₀ (A ∪ B) = (⋃₀ A) ∪ (⋃₀ B) := by
ext x ext x
apply Iff.intro apply Iff.intro
@ -516,11 +516,11 @@ theorem exercise_4_21 {A B : Set (Set α)}
have ⟨t, ht⟩ : ∃ t, t ∈ B ∧ x ∈ t := hB have ⟨t, ht⟩ : ∃ t, t ∈ B ∧ x ∈ t := hB
exact ⟨t, ⟨Set.mem_union_right A ht.left, ht.right⟩⟩ exact ⟨t, ⟨Set.mem_union_right A ht.left, ht.right⟩⟩
/-- ### Exercise 4.22 /-- ### Exercise 2.22
Show that if `A` and `B` are nonempty sets, then `⋂ (A ∪ B) = ⋂ A ∩ ⋂ B`. Show that if `A` and `B` are nonempty sets, then `⋂ (A ∪ B) = ⋂ A ∩ ⋂ B`.
-/ -/
theorem exercise_4_22 {A B : Set (Set α)} theorem exercise_2_22 {A B : Set (Set α)}
: ⋂₀ (A ∪ B) = ⋂₀ A ∩ ⋂₀ B := by : ⋂₀ (A ∪ B) = ⋂₀ A ∩ ⋂₀ B := by
ext x ext x
apply Iff.intro apply Iff.intro
@ -545,11 +545,11 @@ theorem exercise_4_22 {A B : Set (Set α)}
· intro hB · intro hB
exact (this t).right hB exact (this t).right hB
/-- ### Exercise 4.24a /-- ### Exercise 2.24a
Show that is `𝓐` is nonempty, then `𝒫 (⋂ 𝓐) = ⋂ { 𝒫 X | X ∈ 𝓐 }`. Show that is `𝓐` is nonempty, then `𝒫 (⋂ 𝓐) = ⋂ { 𝒫 X | X ∈ 𝓐 }`.
-/ -/
theorem exercise_4_24a {𝓐 : Set (Set α)} theorem exercise_2_24a {𝓐 : Set (Set α)}
: 𝒫 (⋂₀ 𝓐) = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := by : 𝒫 (⋂₀ 𝓐) = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := by
calc 𝒫 (⋂₀ 𝓐) calc 𝒫 (⋂₀ 𝓐)
_ = { x | x ⊆ ⋂₀ 𝓐 } := rfl _ = { x | x ⊆ ⋂₀ 𝓐 } := rfl
@ -564,7 +564,7 @@ theorem exercise_4_24a {𝓐 : Set (Set α)}
_ = { x | ∀ t ∈ { 𝒫 X | X ∈ 𝓐 }, x ∈ t} := by simp _ = { x | ∀ t ∈ { 𝒫 X | X ∈ 𝓐 }, x ∈ t} := by simp
_ = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := rfl _ = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := rfl
/-- ### Exercise 4.24b /-- ### Exercise 2.24b
Show that Show that
``` ```
@ -572,12 +572,12 @@ Show that
``` ```
Under what conditions does equality hold? Under what conditions does equality hold?
-/ -/
theorem exercise_4_24b {𝓐 : Set (Set α)} theorem exercise_2_24b {𝓐 : Set (Set α)}
: (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐) : (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐)
∧ ((⋃₀ { 𝒫 X | X ∈ 𝓐 } = 𝒫 ⋃₀ 𝓐) ↔ (⋃₀ 𝓐 ∈ 𝓐)) := by ∧ ((⋃₀ { 𝒫 X | X ∈ 𝓐 } = 𝒫 ⋃₀ 𝓐) ↔ (⋃₀ 𝓐 ∈ 𝓐)) := by
have hS : (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐) := by have hS : (⋃₀ { 𝒫 X | X ∈ 𝓐 } ⊆ 𝒫 ⋃₀ 𝓐) := by
simp simp
exact exercise_3_3 exact exercise_2_3
refine ⟨hS, ?_⟩ refine ⟨hS, ?_⟩
apply Iff.intro apply Iff.intro
· intro rS · intro rS
@ -593,7 +593,7 @@ theorem exercise_4_24b {𝓐 : Set (Set α)}
have : ⋃₀ 𝓐 = x := by have : ⋃₀ 𝓐 = x := by
rw [← hx.right] at ht rw [← hx.right] at ht
have hl : ⋃₀ 𝓐 ⊆ x := ht have hl : ⋃₀ 𝓐 ⊆ x := ht
have hr : x ⊆ ⋃₀ 𝓐 := exercise_3_3 x hx.left have hr : x ⊆ ⋃₀ 𝓐 := exercise_2_3 x hx.left
exact Set.Subset.antisymm hl hr exact Set.Subset.antisymm hl hr
rw [← this] at hx rw [← this] at hx
exact hx.left exact hx.left
@ -606,12 +606,12 @@ theorem exercise_4_24b {𝓐 : Set (Set α)}
simp only [Set.mem_setOf_eq, exists_exists_and_eq_and, Set.mem_powerset_iff] simp only [Set.mem_setOf_eq, exists_exists_and_eq_and, Set.mem_powerset_iff]
exact ⟨⋃₀ 𝓐, ⟨hA, hx⟩⟩ exact ⟨⋃₀ 𝓐, ⟨hA, hx⟩⟩
/-- ### Exercise 4.25 /-- ### Exercise 2.25
Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under
what conditions does equality hold? what conditions does equality hold?
-/ -/
theorem exercise_4_25 {A : Set α} (𝓑 : Set (Set α)) theorem exercise_2_25 {A : Set α} (𝓑 : Set (Set α))
: (A ∪ (⋃₀ 𝓑) = ⋃₀ { A ∪ X | X ∈ 𝓑 }) ↔ (A = ∅ ∨ Set.Nonempty 𝓑) := by : (A ∪ (⋃₀ 𝓑) = ⋃₀ { A ∪ X | X ∈ 𝓑 }) ↔ (A = ∅ ∨ Set.Nonempty 𝓑) := by
apply Iff.intro apply Iff.intro
· intro h · intro h

62
Bookshelf/Enderton/Set/Chapter_3.lean
View File

@ -19,7 +19,7 @@ theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
exact Set.mem_mem_imp_pair_subset hxs hxys exact Set.mem_mem_imp_pair_subset hxs hxys
/-- ### Exercise 5.1 /-- ### Exercise 3.1
Suppose that we attempted to generalize the Kuratowski definitions of ordered Suppose that we attempted to generalize the Kuratowski definitions of ordered
pairs to ordered triples by defining pairs to ordered triples by defining
@ -31,7 +31,7 @@ Show that this definition is unsuccessful by giving examples of objects `u`,
`v`, `w`, `x`, `y`, `z` with `⟨x, y, z⟩* = ⟨u, v, w⟩*` but with either `y ≠ v` `v`, `w`, `x`, `y`, `z` with `⟨x, y, z⟩* = ⟨u, v, w⟩*` but with either `y ≠ v`
or `z ≠ w` (or both). or `z ≠ w` (or both).
-/ -/
theorem exercise_5_1 {x y z u v w : ℕ} theorem exercise_3_1 {x y z u v w : ℕ}
(hx : x = 1) (hy : y = 1) (hz : z = 2) (hx : x = 1) (hy : y = 1) (hz : z = 2)
(hu : u = 1) (hv : v = 2) (hw : w = 2) (hu : u = 1) (hv : v = 2) (hw : w = 2)
: ({{x}, {x, y}, {x, y, z}} : Set (Set ℕ)) = {{u}, {u, v}, {u, v, w}} : ({{x}, {x, y}, {x, y, z}} : Set (Set ℕ)) = {{u}, {u, v}, {u, v, w}}
@ -42,11 +42,11 @@ theorem exercise_5_1 {x y z u v w : ℕ}
· rw [hy, hv] · rw [hy, hv]
simp only simp only
/-- ### Exercise 5.2a /-- ### Exercise 3.2a
Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`. Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`.
-/ -/
theorem exercise_5_2a {A : Set α} {B C : Set β} theorem exercise_3_2a {A : Set α} {B C : Set β}
: Set.prod A (B ∪ C) = (Set.prod A B) ∪ (Set.prod A C) := by : Set.prod A (B ∪ C) = (Set.prod A B) ∪ (Set.prod A C) := by
calc Set.prod A (B ∪ C) calc Set.prod A (B ∪ C)
_ = { p | p.1 ∈ A ∧ p.2 ∈ B ∪ C } := rfl _ = { p | p.1 ∈ A ∧ p.2 ∈ B ∪ C } := rfl
@ -58,11 +58,11 @@ theorem exercise_5_2a {A : Set α} {B C : Set β}
_ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl
_ = (Set.prod A B) ∪ (Set.prod A C) := rfl _ = (Set.prod A B) ∪ (Set.prod A C) := rfl
/-- ### Exercise 5.2b /-- ### Exercise 3.2b
Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`. Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`.
-/ -/
theorem exercise_5_2b {A : Set α} {B C : Set β} theorem exercise_3_2b {A : Set α} {B C : Set β}
(h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A) (h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A)
: B = C := by : B = C := by
by_cases hB : Set.Nonempty B by_cases hB : Set.Nonempty B
@ -87,11 +87,11 @@ theorem exercise_5_2b {A : Set α} {B C : Set β}
have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC) have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC)
exact (h (a, c)).mpr ⟨ha, hc⟩ exact (h (a, c)).mpr ⟨ha, hc⟩
/-- ### Exercise 5.3 /-- ### Exercise 3.3
Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`. Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`.
-/ -/
theorem exercise_5_3 {A : Set (Set α)} {𝓑 : Set (Set β)} theorem exercise_3_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
: Set.prod A (⋃₀ 𝓑) = ⋃₀ {Set.prod A X | X ∈ 𝓑} := by : Set.prod A (⋃₀ 𝓑) = ⋃₀ {Set.prod A X | X ∈ 𝓑} := by
calc Set.prod A (⋃₀ 𝓑) calc Set.prod A (⋃₀ 𝓑)
_ = { p | p.1 ∈ A ∧ p.2 ∈ ⋃₀ 𝓑} := rfl _ = { p | p.1 ∈ A ∧ p.2 ∈ ⋃₀ 𝓑} := rfl
@ -115,7 +115,7 @@ theorem exercise_5_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
· intro ⟨b, h₁, h₂, h₃⟩ · intro ⟨b, h₁, h₂, h₃⟩
exact ⟨b, h₁, h₂, h₃⟩ exact ⟨b, h₁, h₂, h₃⟩
/-- ### Exercise 5.5a /-- ### Exercise 3.5a
Assume that `A` and `B` are given sets, and show that there exists a set `C` Assume that `A` and `B` are given sets, and show that there exists a set `C`
such that for any `y`, such that for any `y`,
@ -124,7 +124,7 @@ y ∈ C ↔ y = {x} × B for some x in A.
``` ```
In other words, show that `{{x} × B | x ∈ A}` is a set. In other words, show that `{{x} × B | x ∈ A}` is a set.
-/ -/
theorem exercise_5_5a {A : Set α} {B : Set β} theorem exercise_3_5a {A : Set α} {B : Set β}
: ∃ C : Set (Set (α × β)), : ∃ C : Set (Set (α × β)),
y ∈ C ↔ ∃ x ∈ A, y = Set.prod {x} B := by y ∈ C ↔ ∃ x ∈ A, y = Set.prod {x} B := by
let C := {y ∈ 𝒫 (Set.prod A B) | ∃ a ∈ A, ∀ x, (x ∈ y ↔ ∃ b ∈ B, x = (a, b))} let C := {y ∈ 𝒫 (Set.prod A B) | ∃ a ∈ A, ∀ x, (x ∈ y ↔ ∃ b ∈ B, x = (a, b))}
@ -183,11 +183,11 @@ theorem exercise_5_5a {A : Set α} {B : Set β}
rw [hab.right] rw [hab.right]
exact ⟨hab.left, hb⟩ exact ⟨hab.left, hb⟩
/-- ### Exercise 5.5b /-- ### Exercise 3.5b
With `A`, `B`, and `C` as above, show that `A × B = ∪ C`. With `A`, `B`, and `C` as above, show that `A × B = ∪ C`.
-/ -/
theorem exercise_5_5b {A : Set α} (B : Set β) theorem exercise_3_5b {A : Set α} (B : Set β)
: Set.prod A B = ⋃₀ {Set.prod ({x} : Set α) B | x ∈ A} := by : Set.prod A B = ⋃₀ {Set.prod ({x} : Set α) B | x ∈ A} := by
rw [Set.Subset.antisymm_iff] rw [Set.Subset.antisymm_iff]
apply And.intro apply And.intro
@ -222,17 +222,17 @@ If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`.
-/ -/
theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A) theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A)
: x ∈ ⋃₀ (⋃₀ A) ∧ y ∈ ⋃₀ (⋃₀ A) := by : x ∈ ⋃₀ (⋃₀ A) ∧ y ∈ ⋃₀ (⋃₀ A) := by
have hp := Chapter_2.exercise_3_3 (OrderedPair x y) h have hp := Chapter_2.exercise_2_3 (OrderedPair x y) h
unfold OrderedPair at hp unfold OrderedPair at hp
have hq : {x, y} ∈ ⋃₀ A := hp (by simp) have hq : {x, y} ∈ ⋃₀ A := hp (by simp)
have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_3_3 {x, y} hq have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_2_3 {x, y} hq
exact ⟨this (by simp), this (by simp)⟩ exact ⟨this (by simp), this (by simp)⟩
/-- ### Exercise 6.6 /-- ### Exercise 3.6
Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`. Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`.
-/ -/
theorem exercise_6_6 {A : Set.Relation α} theorem exercise_3_6 {A : Set.Relation α}
: A ⊆ Set.prod (A.dom) (A.ran) := by : A ⊆ Set.prod (A.dom) (A.ran) := by
show ∀ t, t ∈ A → t ∈ Set.prod (Prod.fst '' A) (Prod.snd '' A) show ∀ t, t ∈ A → t ∈ Set.prod (Prod.fst '' A) (Prod.snd '' A)
intro (a, b) ht intro (a, b) ht
@ -246,11 +246,11 @@ theorem exercise_6_6 {A : Set.Relation α}
] ]
exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩ exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩
/-- ### Exercise 6.7 /-- ### Exercise 3.7
Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`. Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`.
-/ -/
theorem exercise_6_7 {R : Set.Relation α} theorem exercise_3_7 {R : Set.Relation α}
: R.fld = ⋃₀ ⋃₀ R.toOrderedPairs := by : R.fld = ⋃₀ ⋃₀ R.toOrderedPairs := by
let img := R.toOrderedPairs let img := R.toOrderedPairs
rw [Set.Subset.antisymm_iff] rw [Set.Subset.antisymm_iff]
@ -269,8 +269,8 @@ theorem exercise_6_7 {R : Set.Relation α}
simp only [Prod.exists, Set.mem_setOf_eq] simp only [Prod.exists, Set.mem_setOf_eq]
exact ⟨x, ⟨y, ⟨hp, rfl⟩⟩⟩ exact ⟨x, ⟨y, ⟨hp, rfl⟩⟩⟩
unfold OrderedPair at hm unfold OrderedPair at hm
have : {x} ∈ ⋃₀ img := Chapter_2.exercise_3_3 {{x}, {x, y}} hm (by simp) have : {x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{x}, {x, y}} hm (by simp)
exact (Chapter_2.exercise_3_3 {x} this) (show x ∈ {x} by rfl) exact (Chapter_2.exercise_2_3 {x} this) (show x ∈ {x} by rfl)
· intro hr · intro hr
unfold Set.Relation.ran Prod.snd at hr unfold Set.Relation.ran Prod.snd at hr
simp only [Set.mem_image, Prod.exists, exists_eq_right] at hr simp only [Set.mem_image, Prod.exists, exists_eq_right] at hr
@ -279,9 +279,9 @@ theorem exercise_6_7 {R : Set.Relation α}
simp only [Set.mem_image, Prod.exists] simp only [Set.mem_image, Prod.exists]
exact ⟨t, ⟨x, ⟨ht, rfl⟩⟩⟩ exact ⟨t, ⟨x, ⟨ht, rfl⟩⟩⟩
unfold OrderedPair at hm unfold OrderedPair at hm
have : {t, x} ∈ ⋃₀ img := Chapter_2.exercise_3_3 {{t}, {t, x}} hm have : {t, x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{t}, {t, x}} hm
(show {t, x} ∈ {{t}, {t, x}} by simp) (show {t, x} ∈ {{t}, {t, x}} by simp)
exact Chapter_2.exercise_3_3 {t, x} this (show x ∈ {t, x} by simp) exact Chapter_2.exercise_2_3 {t, x} this (show x ∈ {t, x} by simp)
· show ∀ t, t ∈ ⋃₀ ⋃₀ img → t ∈ Set.Relation.fld R · show ∀ t, t ∈ ⋃₀ ⋃₀ img → t ∈ Set.Relation.fld R
intro t ht intro t ht
@ -300,7 +300,7 @@ theorem exercise_6_7 {R : Set.Relation α}
-- `t = y` then `t ∈ ran R`. -- `t = y` then `t ∈ ran R`.
have hxy_mem : t = x ∨ t = y → t ∈ Set.Relation.fld R := by have hxy_mem : t = x ∨ t = y → t ∈ Set.Relation.fld R := by
intro ht intro ht
have hz : R ⊆ Set.prod (R.dom) (R.ran) := exercise_6_6 have hz : R ⊆ Set.prod (R.dom) (R.ran) := exercise_3_6
have : (x, y) ∈ Set.prod (R.dom) (R.ran) := hz p have : (x, y) ∈ Set.prod (R.dom) (R.ran) := hz p
unfold Set.prod at this unfold Set.prod at this
simp at this simp at this
@ -329,14 +329,14 @@ section
open Set.Relation open Set.Relation
/-- ### Exercise 6.8 (i) /-- ### Exercise 3.8 (i)
Show that for any set `𝓐`: Show that for any set `𝓐`:
``` ```
dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 } dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
``` ```
-/ -/
theorem exercise_6_8_i {A : Set (Set.Relation α)} theorem exercise_3_8_i {A : Set (Set.Relation α)}
: dom (⋃₀ A) = ⋃₀ { dom R | R ∈ A } := by : dom (⋃₀ A) = ⋃₀ { dom R | R ∈ A } := by
ext x ext x
unfold dom Prod.fst unfold dom Prod.fst
@ -355,14 +355,14 @@ theorem exercise_6_8_i {A : Set (Set.Relation α)}
· intro ⟨t, ht, y, hx⟩ · intro ⟨t, ht, y, hx⟩
exact ⟨y, t, ht, hx⟩ exact ⟨y, t, ht, hx⟩
/-- ### Exercise 6.8 (ii) /-- ### Exercise 3.8 (ii)
Show that for any set `𝓐`: Show that for any set `𝓐`:
``` ```
ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 } ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
``` ```
-/ -/
theorem exercise_6_8_ii {A : Set (Set.Relation α)} theorem exercise_3_8_ii {A : Set (Set.Relation α)}
: ran (⋃₀ A) = ⋃₀ { ran R | R ∈ A } := by : ran (⋃₀ A) = ⋃₀ { ran R | R ∈ A } := by
ext x ext x
unfold ran Prod.snd unfold ran Prod.snd
@ -380,7 +380,7 @@ theorem exercise_6_8_ii {A : Set (Set.Relation α)}
· intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩ · intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩ exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
/-- ### Exercise 6.9 (i) /-- ### Exercise 3.9 (i)
Discuss the result of replacing the union operation by the intersection Discuss the result of replacing the union operation by the intersection
operation in the preceding problem. operation in the preceding problem.
@ -388,7 +388,7 @@ operation in the preceding problem.
dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 } dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
``` ```
-/ -/
theorem exercise_6_9_i {A : Set (Set.Relation α)} theorem exercise_3_9_i {A : Set (Set.Relation α)}
: dom (⋂₀ A) ⊆ ⋂₀ { dom R | R ∈ A } := by : dom (⋂₀ A) ⊆ ⋂₀ { dom R | R ∈ A } := by
show ∀ x, x ∈ dom (⋂₀ A) → x ∈ ⋂₀ { dom R | R ∈ A } show ∀ x, x ∈ dom (⋂₀ A) → x ∈ ⋂₀ { dom R | R ∈ A }
unfold dom Prod.fst unfold dom Prod.fst
@ -406,7 +406,7 @@ theorem exercise_6_9_i {A : Set (Set.Relation α)}
intro _ y hy R hR intro _ y hy R hR
exact ⟨y, hy R hR⟩ exact ⟨y, hy R hR⟩
/-- ### Exercise 6.9 (ii) /-- ### Exercise 3.9 (ii)
Discuss the result of replacing the union operation by the intersection Discuss the result of replacing the union operation by the intersection
operation in the preceding problem. operation in the preceding problem.
@ -414,7 +414,7 @@ operation in the preceding problem.
ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 } ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
``` ```
-/ -/
theorem exercise_6_9_ii {A : Set (Set.Relation α)} theorem exercise_3_9_ii {A : Set (Set.Relation α)}
: ran (⋂₀ A) ⊆ ⋂₀ { ran R | R ∈ A } := by : ran (⋂₀ A) ⊆ ⋂₀ { ran R | R ∈ A } := by
show ∀ x, x ∈ ran (⋂₀ A) → x ∈ ⋂₀ { ran R | R ∈ A } show ∀ x, x ∈ ran (⋂₀ A) → x ∈ ⋂₀ { ran R | R ∈ A }
unfold ran Prod.snd unfold ran Prod.snd