danabra.mov
My solutions to Tao's Analysis I, formalized in Lean
Section 3.4 solutions (#7)
* 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* More 3.4
* Golf
+233
-32
+233
-32
analysis/Analysis/Section_3_4.lean
+233
-32
analysis/Analysis/Section_3_4.lean
···
34
34
35
35
/-- Alternate definition of image using axiom of specification -/
36
36
theorem SetTheory.Set.image_eq_specify {X Y:Set} (f:X → Y) (S: Set) :
37
-
image f S = Y.specify (fun y ↦ ∃ x:X, x.val ∈ S ∧ f x = y) := by sorry
37
+
image f S = Y.specify (fun y ↦ ∃ x:X, x.val ∈ S ∧ f x = y) := by
38
+
ext y
39
+
constructor
40
+
· intro h
41
+
rw [mem_image] at h
42
+
obtain ⟨x, hx, hxy⟩ := h
43
+
rw [specification_axiom'', ←hxy]
44
+
use (f x).property, x
45
+
intro h
46
+
rw [mem_image]
47
+
rw [specification_axiom''] at h
48
+
obtain ⟨hy, ⟨x, hx, hxy⟩⟩ := h
49
+
use x, hx
50
+
rw [hxy]
38
51
39
52
/--
40
53
Connection with Mathlib's notion of image. Note the need to utilize the `Subtype.val` coercion
···
69
82
example : (fun n:ℤ ↦ n^2) '' {-1,0,1,2} = {0,1,4} := by aesop
70
83
71
84
theorem SetTheory.Set.mem_image_of_eval {X Y:Set} (f:X → Y) (S: Set) (x:X) :
72
-
x.val ∈ S → (f x).val ∈ image f S := by sorry
85
+
x.val ∈ S → (f x).val ∈ image f S := by
86
+
intro h
87
+
rw [mem_image]
88
+
use x
73
89
74
90
theorem SetTheory.Set.mem_image_of_eval_counter :
75
-
∃ (X Y:Set) (f:X → Y) (S: Set) (x:X), ¬((f x).val ∈ image f S → x.val ∈ S) := by sorry
91
+
∃ (X Y:Set) (f:X → Y) (S: Set) (x:X), ¬((f x).val ∈ image f S → x.val ∈ S) := by
92
+
use Nat, Nat, fun x ↦ 0, {((0:Nat):Object)}, 1
93
+
push_neg
94
+
simp only [mem_image, mem_singleton, and_true]
95
+
constructor
96
+
· use 0
97
+
simp [Subtype.coe_ne_coe]
76
98
77
99
/--
78
100
Definition 3.4.4 (inverse images).
···
119
141
all_goals simp
120
142
121
143
theorem SetTheory.Set.image_preimage_f_3_4_2 :
122
-
image f_3_4_2 (preimage f_3_4_2 {1,2,3}) ≠ {1,2,3} := by sorry
144
+
image f_3_4_2 (preimage f_3_4_2 {1,2,3}) ≠ {1,2,3} := by
145
+
intro h
146
+
have : 1 ∉ image f_3_4_2 (preimage f_3_4_2 {1, 2, 3}) := by simp
147
+
simp_all
123
148
124
149
/-- Example 3.4.7 (using the Mathlib notion of preimage) -/
125
150
example : (fun n:ℤ ↦ n^2) ⁻¹' {0,1,4} = {-2,-1,0,1,2} := by
···
129
154
on_goal 3 => have : 2 ^ 2 = (4:ℤ) := (by norm_num); rw [←h, sq_eq_sq_iff_eq_or_eq_neg] at this
130
155
all_goals aesop
131
156
132
-
example : (fun n:ℤ ↦ n^2) ⁻¹' ((fun n:ℤ ↦ n^2) '' {-1,0,1,2}) ≠ {-1,0,1,2} := by sorry
157
+
example : (fun n:ℤ ↦ n^2) ⁻¹' ((fun n:ℤ ↦ n^2) '' {-1,0,1,2}) ≠ {-1,0,1,2} := by
158
+
intro h
159
+
rw [Set.ext_iff] at h
160
+
specialize h (-2)
161
+
have : -2 ∉ ({-1, 0, 1, 2}: _root_.Set ℤ) := by simp
162
+
apply h.not.mpr this
163
+
simp
133
164
134
165
instance SetTheory.Set.inst_pow : Pow Set Set where
135
166
pow := SetTheory.pow
···
181
212
182
213
/-- Exercise 3.4.6 (i). One needs to provide a suitable definition of the power set here. -/
183
214
def SetTheory.Set.powerset (X:Set) : Set :=
184
-
(({0,1} ^ X): Set).replace (P := sorry) (by sorry)
215
+
(({0,1} ^ X): Set).replace (P := fun F Y ↦
216
+
∃ f : X → ({0,1}: Set), F = (f : Object) ∧ Y = (preimage f {1})
217
+
) (by aesop)
185
218
186
219
open Classical in
187
220
/-- Exercise 3.4.6 (i) -/
188
221
@[simp]
189
222
theorem SetTheory.Set.mem_powerset {X:Set} (x:Object) :
190
-
x ∈ powerset X ↔ ∃ Y:Set, x = Y ∧ Y ⊆ X := by sorry
223
+
x ∈ powerset X ↔ ∃ Y:Set, x = Y ∧ Y ⊆ X := by
224
+
rw [powerset, replacement_axiom]
225
+
constructor
226
+
· rintro ⟨_, ⟨f, _, hfx⟩⟩
227
+
use preimage f {1}, hfx
228
+
simp only [subset_def, mem_preimage']
229
+
rintro _ ⟨a, ⟨rfl, _⟩⟩
230
+
use a.property
231
+
intro h
232
+
obtain ⟨Y, rfl, _⟩ := h
233
+
let f : X → ({0,1}: Set) := fun x ↦
234
+
if x.val ∈ Y then ⟨1, by simp⟩
235
+
else ⟨0, by simp⟩
236
+
have hf := (powerset_axiom _).mpr (by use f)
237
+
use ⟨_, hf⟩, f
238
+
constructor
239
+
· rfl
240
+
congr
241
+
apply Set.ext
242
+
simp only [mem_preimage']
243
+
aesop
191
244
192
245
/-- Lemma 3.4.10 -/
193
246
theorem SetTheory.Set.exists_powerset (X:Set) :
···
227
280
/-- Example 3.4.12 -/
228
281
theorem SetTheory.Set.example_3_4_12 :
229
282
union { (({2,3}:Set):Object), (({3,4}:Set):Object), (({4,5}:Set):Object) } = {2,3,4,5} := by
230
-
sorry
283
+
apply Set.ext
284
+
simp only [union_axiom, Insert.insert]
285
+
aesop
231
286
232
287
/-- Connection with Mathlib union -/
233
288
theorem SetTheory.Set.union_eq (A: Set) :
···
265
320
(iUnion I A : _root_.Set Object) = ⋃ α, (A α: _root_.Set Object) := by
266
321
ext; simp only [mem_iUnion, _root_.Set.mem_setOf_eq, _root_.Set.mem_iUnion]
267
322
268
-
theorem SetTheory.Set.iUnion_of_empty (A: (∅:Set) → Set) : iUnion (∅:Set) A = ∅ := by sorry
323
+
theorem SetTheory.Set.iUnion_of_empty (A: (∅:Set) → Set) : iUnion (∅:Set) A = ∅ := by
324
+
ext
325
+
simp only [not_mem_empty, iff_false, mem_iUnion]
326
+
push_neg
327
+
intro α
328
+
have := α.property
329
+
aesop
269
330
270
331
/-- Indexed intersection -/
271
332
noncomputable abbrev SetTheory.Set.nonempty_choose {I:Set} (hI: I ≠ ∅) : I :=
···
279
340
280
341
theorem SetTheory.Set.mem_iInter {I:Set} (hI: I ≠ ∅) (A: I → Set) (x:Object) :
281
342
x ∈ iInter I hI A ↔ ∀ α:I, x ∈ A α := by
282
-
sorry
343
+
constructor
344
+
· intro h
345
+
rw [specification_axiom''] at h
346
+
exact h.2
347
+
intro h
348
+
rw [specification_axiom'']
349
+
use h (nonempty_choose hI)
283
350
284
351
/-- Exercise 3.4.1 -/
285
352
theorem SetTheory.Set.preimage_eq_image_of_inv {X Y V:Set} (f:X → Y) (f_inv: Y → X)
286
353
(hf: Function.LeftInverse f_inv f ∧ Function.RightInverse f_inv f) (hV: V ⊆ Y) :
287
-
image f_inv V = preimage f V := by sorry
354
+
image f_inv V = preimage f V := by
355
+
ext
356
+
simp only [mem_image, mem_preimage']
357
+
constructor
358
+
· rintro ⟨y, hy, rfl⟩
359
+
use (f_inv y), rfl
360
+
rwa [hf.2]
361
+
rintro ⟨x, rfl, hx⟩
362
+
use (f x), hx
363
+
rw [hf.1]
288
364
289
365
/- Exercise 3.4.2. State and prove an assertion connecting `preimage f (image f S)` and `S`. -/
290
-
-- theorem SetTheory.Set.preimage_of_image {X Y:Set} (f:X → Y) (S: Set) (hS: S ⊆ X) : sorry := by sorry
366
+
theorem SetTheory.Set.preimage_of_image {X Y:Set} (f:X → Y) (S: Set) (hS: S ⊆ X) :
367
+
S ⊆ preimage f (image f S) := by
368
+
simp only [subset_def, mem_preimage', mem_image] at *
369
+
intro x xs
370
+
let x': X := ⟨x, hS x xs⟩
371
+
use x', rfl, x'
291
372
292
373
/- Exercise 3.4.2. State and prove an assertion connecting `image f (preimage f U)` and `U`.
293
374
Interestingly, it is not needed for U to be a subset of Y. -/
294
-
-- theorem SetTheory.Set.image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry
375
+
theorem SetTheory.Set.image_of_preimage {X Y:Set} (f:X → Y) (U: Set) :
376
+
image f (preimage f U) ⊆ U := by
377
+
simp only [subset_def, mem_image]
378
+
rintro y ⟨x, hx, rfl⟩
379
+
rwa [mem_preimage] at hx
295
380
296
381
/- Exercise 3.4.2. State and prove an assertion connecting `preimage f (image f (preimage f U))` and `preimage f U`.
297
382
Interestingly, it is not needed for U to be a subset of Y.-/
298
-
-- theorem SetTheory.Set.preimage_of_image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry
383
+
theorem SetTheory.Set.preimage_of_image_of_preimage {X Y:Set} (f:X → Y) (U: Set) :
384
+
preimage f (image f (preimage f U)) = preimage f U := by
385
+
aesop
299
386
300
387
/--
301
388
Exercise 3.4.3.
302
389
-/
303
390
theorem SetTheory.Set.image_of_inter {X Y:Set} (f:X → Y) (A B: Set) :
304
-
image f (A ∩ B) ⊆ (image f A) ∩ (image f B) := by sorry
391
+
image f (A ∩ B) ⊆ (image f A) ∩ (image f B) := by
392
+
simp only [subset_def]
393
+
aesop
305
394
306
395
theorem SetTheory.Set.image_of_diff {X Y:Set} (f:X → Y) (A B: Set) :
307
-
(image f A) \ (image f B) ⊆ image f (A \ B) := by sorry
396
+
(image f A) \ (image f B) ⊆ image f (A \ B) := by
397
+
simp only [subset_def, mem_image, mem_inter, mem_sdiff]
398
+
rintro y ⟨⟨x, ⟨h1, h2⟩⟩, h'⟩
399
+
have : (x: Object) ∉ B := by contrapose! h'; use x
400
+
use x, ⟨h1, this⟩
308
401
309
402
theorem SetTheory.Set.image_of_union {X Y:Set} (f:X → Y) (A B: Set) :
310
-
image f (A ∪ B) = (image f A) ∪ (image f B) := by sorry
403
+
image f (A ∪ B) = (image f A) ∪ (image f B) := by
404
+
aesop
311
405
312
406
def SetTheory.Set.image_of_inter' : Decidable (∀ X Y:Set, ∀ f:X → Y, ∀ A B: Set, image f (A ∩ B) = (image f A) ∩ (image f B)) := by
313
407
-- The first line of this construction should be either `apply isTrue` or `apply isFalse`
314
-
sorry
408
+
apply isFalse
409
+
push_neg
410
+
let f : nat → nat := fun x ↦ 0
411
+
use nat, nat, f, {1}, {2}
412
+
intro h
413
+
rw [show ({1} ∩ {2}: Set) = ∅ by apply ext; simp] at h
414
+
rw [show (image f ∅) = ∅ by apply ext; simp [mem_image]] at h
415
+
symm at h
416
+
rw [eq_empty_iff_forall_notMem] at h
417
+
contrapose! h
418
+
simp only [mem_inter, mem_image, f]
419
+
use 0
420
+
constructor
421
+
· use 1
422
+
norm_num
423
+
use 2
424
+
norm_num
315
425
316
426
def SetTheory.Set.image_of_diff' : Decidable (∀ X Y:Set, ∀ f:X → Y, ∀ A B: Set, image f (A \ B) = (image f A) \ (image f B)) := by
317
427
-- The first line of this construction should be either `apply isTrue` or `apply isFalse`
318
-
sorry
428
+
apply isFalse
429
+
push_neg
430
+
let f : nat → nat := fun x ↦ 0
431
+
use nat, nat, f, {1, 2}, {2}
432
+
rw [show ({1, 2}: Set) \ {2} = {1} by apply ext; aesop]
433
+
intro h
434
+
rw [Set.ext_iff] at h
435
+
specialize h 0
436
+
have : 0 ∈ image f {1} := by rw [mem_image]; use 1; simp [f]
437
+
have : 0 ∈ image f {2} := by rw [mem_image]; use 2; simp [f]
438
+
simp_all [f]
319
439
320
440
/-- Exercise 3.4.4 -/
321
441
theorem SetTheory.Set.preimage_of_inter {X Y:Set} (f:X → Y) (A B: Set) :
322
-
preimage f (A ∩ B) = (preimage f A) ∩ (preimage f B) := by sorry
442
+
preimage f (A ∩ B) = (preimage f A) ∩ (preimage f B) := by
443
+
aesop
323
444
324
445
theorem SetTheory.Set.preimage_of_union {X Y:Set} (f:X → Y) (A B: Set) :
325
-
preimage f (A ∪ B) = (preimage f A) ∪ (preimage f B) := by sorry
446
+
preimage f (A ∪ B) = (preimage f A) ∪ (preimage f B) := by
447
+
aesop
326
448
327
449
theorem SetTheory.Set.preimage_of_diff {X Y:Set} (f:X → Y) (A B: Set) :
328
-
preimage f (A \ B) = (preimage f A) \ (preimage f B) := by sorry
450
+
preimage f (A \ B) = (preimage f A) \ (preimage f B) := by
451
+
aesop
329
452
330
453
/-- Exercise 3.4.5 -/
331
454
theorem SetTheory.Set.image_preimage_of_surj {X Y:Set} (f:X → Y) :
332
-
(∀ S, S ⊆ Y → image f (preimage f S) = S) ↔ Function.Surjective f := by sorry
455
+
(∀ S, S ⊆ Y → image f (preimage f S) = S) ↔ Function.Surjective f := by
456
+
constructor
457
+
· intro h y
458
+
simp only [subset_def, Set.ext_iff, mem_singleton, mem_image] at h
459
+
specialize h _ (by aesop) y
460
+
obtain ⟨x, ⟨_, hx⟩⟩ := h.mpr (by aesop)
461
+
use x, by rwa [coe_inj] at hx
462
+
intro h S hS
463
+
apply ext
464
+
intro y
465
+
simp only [mem_image, mem_preimage]
466
+
constructor
467
+
· rintro ⟨x, ⟨hx, rfl⟩⟩
468
+
exact hx
469
+
intro hy
470
+
obtain ⟨x, hx⟩ := h ⟨y, hS y hy⟩
471
+
use x, by rwa [hx], by rw [hx]
333
472
334
473
/-- Exercise 3.4.5 -/
335
474
theorem SetTheory.Set.preimage_image_of_inj {X Y:Set} (f:X → Y) :
336
-
(∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by sorry
475
+
(∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by
476
+
constructor
477
+
· intro h x1 x2 hf
478
+
simp only [subset_def] at h
479
+
have hx: ((f x2): Object) ∈ image f {(x2: Object)} := by rw [mem_image]; aesop
480
+
rwa [←hf, ←mem_preimage, h _ (by aesop), mem_singleton, coe_inj] at hx
481
+
intro h S hS
482
+
ext x
483
+
constructor
484
+
· simp only [mem_preimage', mem_image]
485
+
rintro ⟨x1, rfl, x2, hx2, heq⟩
486
+
rw [coe_inj] at heq
487
+
rwa [←h heq]
488
+
intro hx
489
+
simp only [mem_preimage', mem_image]
490
+
use ⟨x, hS x hx⟩, rfl, ⟨x, hS x hx⟩
337
491
338
492
/-- Helper lemma for Exercise 3.4.7. -/
339
493
@[simp]
···
349
503
/-- Exercise 3.4.7 -/
350
504
theorem SetTheory.Set.partial_functions {X Y:Set} :
351
505
∃ Z:Set, ∀ F:Object, F ∈ Z ↔ ∃ X' Y':Set, X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f: X' → Y', F = f := by
352
-
sorry
506
+
use union (Y.powerset.replace (P := fun oY' outer ↦
507
+
outer = union (X.powerset.replace (P := fun oX' inner ↦
508
+
∃ (X' Y' : Set),
509
+
oX'.val = X' ∧
510
+
oY'.val = Y' ∧
511
+
inner = (Y' ^ X': Set)
512
+
) (by simp_all))
513
+
) (by simp_all))
514
+
intro F
515
+
constructor
516
+
· intro hF
517
+
simp only [mem_union_powerset_replace_iff, EmbeddingLike.apply_eq_iff_eq] at hF
518
+
obtain ⟨⟨oY', hY'⟩, _, rfl, hF⟩ := hF
519
+
simp only [mem_union_powerset_replace_iff, EmbeddingLike.apply_eq_iff_eq] at hF
520
+
obtain ⟨⟨oX', hX'⟩, Y'X', hF, hF'⟩ := hF
521
+
simp only [EmbeddingLike.apply_eq_iff_eq] at hF
522
+
obtain ⟨X', Y', rfl, rfl, rfl⟩ := hF
523
+
simp_all only [mem_powerset', powerset_axiom]
524
+
obtain ⟨f, hF⟩ := hF'
525
+
use X', Y'
526
+
use hX', hY'
527
+
use f, hF.symm
528
+
rintro ⟨X', Y', hX', hY', f, rfl⟩
529
+
simp_all [mem_union_powerset_replace_iff, EmbeddingLike.apply_eq_iff_eq,
530
+
exists_eq_left, Subtype.exists]
531
+
use Y', by simp_all
532
+
use X', by simp_all
533
+
use Y' ^ X', by simp_all
534
+
rw [powerset_axiom]
535
+
use f
353
536
354
537
/--
355
538
Exercise 3.4.8. The point of this exercise is to prove it without using the
356
539
pairwise union operation `∪`.
357
540
-/
358
541
theorem SetTheory.Set.union_pair_exists (X Y:Set) : ∃ Z:Set, ∀ x, x ∈ Z ↔ (x ∈ X ∨ x ∈ Y) := by
359
-
sorry
542
+
use union {(X: Object), (Y: Object)}
543
+
simp [union_axiom]
544
+
aesop
360
545
361
546
/-- Exercise 3.4.9 -/
362
547
theorem SetTheory.Set.iInter'_insensitive {I:Set} (β β':I) (A: I → Set) :
363
-
iInter' I β A = iInter' I β' A := by sorry
548
+
iInter' I β A = iInter' I β' A := by
549
+
ext
550
+
simp_all
364
551
365
552
/-- Exercise 3.4.10 -/
366
553
theorem SetTheory.Set.union_iUnion {I J:Set} (A: (I ∪ J:Set) → Set) :
367
554
iUnion I (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
368
555
∪ iUnion J (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
369
-
= iUnion (I ∪ J) A := by sorry
556
+
= iUnion (I ∪ J) A := by
557
+
ext
558
+
simp only [mem_iUnion, mem_union]
559
+
aesop
370
560
371
561
/-- Exercise 3.4.10 -/
372
-
theorem SetTheory.Set.union_of_nonempty {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) : I ∪ J ≠ ∅ := by sorry
562
+
theorem SetTheory.Set.union_of_nonempty {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) : I ∪ J ≠ ∅ := by
563
+
intro h
564
+
simp_all [Set.ext_iff]
373
565
374
566
/-- Exercise 3.4.10 -/
375
567
theorem SetTheory.Set.inter_iInter {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) (A: (I ∪ J:Set) → Set) :
376
568
iInter I hI (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
377
569
∩ iInter J hJ (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
378
-
= iInter (I ∪ J) (union_of_nonempty hI hJ) A := by sorry
570
+
= iInter (I ∪ J) (union_of_nonempty hI hJ) A := by
571
+
ext x
572
+
simp only [mem_iInter, mem_inter]
573
+
aesop
379
574
380
575
/-- Exercise 3.4.11 -/
381
576
theorem SetTheory.Set.compl_iUnion {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
382
-
X \ iUnion I A = iInter I hI (fun α ↦ X \ A α) := by sorry
577
+
X \ iUnion I A = iInter I hI (fun α ↦ X \ A α) := by
578
+
apply ext; intro x
579
+
simp only [mem_sdiff, mem_iUnion]
580
+
aesop
383
581
384
582
/-- Exercise 3.4.11 -/
385
583
theorem SetTheory.Set.compl_iInter {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
386
-
X \ iInter I hI A = iUnion I (fun α ↦ X \ A α) := by sorry
584
+
X \ iInter I hI A = iUnion I (fun α ↦ X \ A α) := by
585
+
ext
586
+
simp only [mem_sdiff, mem_iInter, mem_iUnion]
587
+
aesop
387
588
388
589
end Chapter3