danabra.mov
My solutions to Tao's Analysis I, formalized in Lean
Section 3.2 solutions (#5)
+65
-11
+65
-11
analysis/Analysis/Section_3_2.lean
+65
-11
analysis/Analysis/Section_3_2.lean
···
60
60
-/
61
61
theorem SetTheory.Set.emptyset_exists (h: axiom_of_universal_specification):
62
62
∃ (X:Set), ∀ x, x ∉ X := by
63
-
sorry
63
+
let P : Object → Prop := fun _ ↦ False
64
+
obtain ⟨A, hA⟩ := h P
65
+
use A
66
+
intro x
67
+
rw [hA _]
68
+
unfold P
69
+
trivial
64
70
65
71
/--
66
72
Exercise 3.2.1. The spirit of the exercise is to establish these results without using either
···
68
74
-/
69
75
theorem SetTheory.Set.singleton_exists (h: axiom_of_universal_specification) (x:Object):
70
76
∃ (X:Set), ∀ y, y ∈ X ↔ y = x := by
71
-
sorry
77
+
let P : Object → Prop := fun y ↦ y = x
78
+
apply h
72
79
73
80
/--
74
81
Exercise 3.2.1. The spirit of the exercise is to establish these results without using either
···
76
83
-/
77
84
theorem SetTheory.Set.pair_exists (h: axiom_of_universal_specification) (x₁ x₂:Object):
78
85
∃ (X:Set), ∀ y, y ∈ X ↔ y = x₁ ∨ y = x₂ := by
79
-
sorry
86
+
let P : Object → Prop := fun y ↦ y = x₁ ∨ y = x₂
87
+
apply h
80
88
81
89
/--
82
90
Exercise 3.2.1. The spirit of the exercise is to establish these results without using either
···
84
92
-/
85
93
theorem SetTheory.Set.union_exists (h: axiom_of_universal_specification) (A B:Set):
86
94
∃ (Z:Set), ∀ z, z ∈ Z ↔ z ∈ A ∨ z ∈ B := by
87
-
sorry
95
+
let P : Object → Prop := fun z ↦ z ∈ A ∨ z ∈ B
96
+
apply h
88
97
89
98
/--
90
99
Exercise 3.2.1. The spirit of the exercise is to establish these results without using either
···
92
101
-/
93
102
theorem SetTheory.Set.specify_exists (h: axiom_of_universal_specification) (A:Set) (P: A → Prop):
94
103
∃ (Z:Set), ∀ z, z ∈ Z ↔ ∃ h : z ∈ A, P ⟨ z, h ⟩ := by
95
-
sorry
104
+
let P : Object → Prop := fun z ↦ ∃ h : z ∈ A, P ⟨ z, h ⟩
105
+
apply h
96
106
97
107
/--
98
108
Exercise 3.2.1. The spirit of the exercise is to establish these results without using either
···
101
111
theorem SetTheory.Set.replace_exists (h: axiom_of_universal_specification) (A:Set)
102
112
(P: A → Object → Prop) (hP: ∀ x y y', P x y ∧ P x y' → y = y') :
103
113
∃ (Z:Set), ∀ y, y ∈ Z ↔ ∃ a : A, P a y := by
104
-
sorry
114
+
let P : Object → Prop := fun y ↦ ∃ a : A, P a y
115
+
apply h
105
116
106
117
/-- Exercise 3.2.2 -/
107
-
theorem SetTheory.Set.not_mem_self (A:Set) : (A:Object) ∉ A := by sorry
118
+
theorem SetTheory.Set.not_mem_self (A:Set) : (A:Object) ∉ A := by
119
+
let B: Set := {(A: Object)}
120
+
have hB : B ≠ ∅ := by
121
+
unfold B
122
+
intro h
123
+
simp only [eq_empty_iff_forall_notMem, mem_singleton, forall_eq] at h
124
+
have ⟨x, hx⟩ := axiom_of_regularity hB
125
+
simp only [eq_empty_iff_forall_notMem, disjoint_iff] at hx
126
+
aesop
108
127
109
128
/-- Exercise 3.2.2 -/
110
-
theorem SetTheory.Set.not_mem_mem (A B:Set) : (A:Object) ∉ B ∨ (B:Object) ∉ A := by sorry
129
+
theorem SetTheory.Set.not_mem_mem (A B:Set) : (A:Object) ∉ B ∨ (B:Object) ∉ A := by
130
+
by_contra! h
131
+
obtain ⟨h1, h2⟩ := h
132
+
let C: Set := {(A: Object), (B: Object)}
133
+
have hC : C ≠ ∅ := by
134
+
unfold C
135
+
intro h
136
+
simp only [eq_empty_iff_forall_notMem, mem_pair, forall_eq] at h
137
+
specialize h A
138
+
simp only [true_or, not_true_eq_false] at h
139
+
have ⟨x, hx⟩ := axiom_of_regularity hC
140
+
simp only [eq_empty_iff_forall_notMem, disjoint_iff, mem_inter] at hx
141
+
have hxAB : x = (A: Object) ∨ x = (B: Object) := by aesop
142
+
rcases hxAB with hxA | hxB
143
+
· specialize hx A hxA B
144
+
aesop
145
+
specialize hx B hxB A
146
+
aesop
111
147
112
148
/-- Exercise 3.2.3 -/
113
149
theorem SetTheory.Set.univ_iff : axiom_of_universal_specification ↔
114
-
∃ (U:Set), ∀ x, x ∈ U := by sorry
150
+
∃ (U:Set), ∀ x, x ∈ U := by
151
+
constructor
152
+
· intro h
153
+
set P : Object → Prop := fun x ↦ True
154
+
obtain ⟨U, hU⟩ := h P
155
+
use U
156
+
intro x
157
+
rw [hU]
158
+
tauto
159
+
rintro ⟨U, hU⟩
160
+
unfold axiom_of_universal_specification
161
+
intro P
162
+
use specify U fun x ↦ P x
163
+
intro x
164
+
rw [specification_axiom'']
165
+
aesop
115
166
116
167
/-- Exercise 3.2.3 -/
117
-
theorem SetTheory.Set.no_univ : ¬ ∃ (U:Set), ∀ (x:Object), x ∈ U := by sorry
118
-
168
+
theorem SetTheory.Set.no_univ : ¬ ∃ (U:Set), ∀ (x:Object), x ∈ U := by
169
+
rintro ⟨U, hU⟩
170
+
have hU' := hU U
171
+
have := not_mem_self U
172
+
contradiction
119
173
120
174
end Chapter3