From f3b01eecabe2ad38dcc087ea544f6fb109498b6f Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:20 +0300 Subject: [PATCH 01/13] Disambiguate Proposition 3.6.14(b') for card_union_disjoint. Co-authored-by: Cursor --- Analysis/Section_3_6.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_3_6.lean b/Analysis/Section_3_6.lean index b5a171e18..551d31554 100644 --- a/Analysis/Section_3_6.lean +++ b/Analysis/Section_3_6.lean @@ -275,7 +275,7 @@ theorem SetTheory.Set.card_insert {X:Set} (hX: X.finite) {x:Object} (hx: x ∉ X theorem SetTheory.Set.card_union {X Y:Set} (hX: X.finite) (hY: Y.finite) : (X ∪ Y).finite ∧ (X ∪ Y).card ≤ X.card + Y.card := by sorry -/-- Proposition 3.6.14 (b) / Exercise 3.6.4 -/ +/-- Proposition 3.6.14 (b') / Exercise 3.6.4 -/ theorem SetTheory.Set.card_union_disjoint {X Y:Set} (hX: X.finite) (hY: Y.finite) (hdisj: Disjoint X Y) : (X ∪ Y).card = X.card + Y.card := by sorry From 3eeda8a99abee72ccbfa826d4497c8c418103a5a Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:20 +0300 Subject: [PATCH 02/13] Disambiguate Proposition 3.6.14(c') for card_ssubset. Co-authored-by: Cursor --- Analysis/Section_3_6.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_3_6.lean b/Analysis/Section_3_6.lean index 551d31554..c819d0b16 100644 --- a/Analysis/Section_3_6.lean +++ b/Analysis/Section_3_6.lean @@ -283,7 +283,7 @@ theorem SetTheory.Set.card_union_disjoint {X Y:Set} (hX: X.finite) (hY: Y.finite theorem SetTheory.Set.card_subset {X Y:Set} (hX: X.finite) (hY: Y ⊆ X) : Y.finite ∧ Y.card ≤ X.card := by sorry -/-- Proposition 3.6.14 (c) / Exercise 3.6.4 -/ +/-- Proposition 3.6.14 (c') / Exercise 3.6.4 -/ theorem SetTheory.Set.card_ssubset {X Y:Set} (hX: X.finite) (hY: Y ⊂ X) : Y.card < X.card := by sorry From 83e410aeb46f438c6e06204adb92dc8f7e382f8a Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:20 +0300 Subject: [PATCH 03/13] Disambiguate Proposition 3.6.14(d') for card_image_inj. Co-authored-by: Cursor --- Analysis/Section_3_6.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_3_6.lean b/Analysis/Section_3_6.lean index c819d0b16..b472310b7 100644 --- a/Analysis/Section_3_6.lean +++ b/Analysis/Section_3_6.lean @@ -291,7 +291,7 @@ theorem SetTheory.Set.card_ssubset {X Y:Set} (hX: X.finite) (hY: Y ⊂ X) : theorem SetTheory.Set.card_image {X Y:Set} (hX: X.finite) (f: X → Y) : (image f X).finite ∧ (image f X).card ≤ X.card := by sorry -/-- Proposition 3.6.14 (d) / Exercise 3.6.4 -/ +/-- Proposition 3.6.14 (d') / Exercise 3.6.4 -/ theorem SetTheory.Set.card_image_inj {X Y:Set} (hX: X.finite) {f: X → Y} (hf: Function.Injective f) : (image f X).card = X.card := by sorry From 2ff8237c5181b7ed184ba4cd0a0b373c5471f84e Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:51 +0300 Subject: [PATCH 04/13] Disambiguate Proposition 6.4.12(a') for lt_liminf_bounds. Co-authored-by: Cursor --- Analysis/Section_6_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean index f056b72da..206085f1a 100644 --- a/Analysis/Section_6_4.lean +++ b/Analysis/Section_6_4.lean @@ -154,7 +154,7 @@ theorem Sequence.gt_limsup_bounds {a:Sequence} {x:EReal} (h: x > a.limsup) : convert lt_of_le_of_lt ((a.from N).le_sup hn') ha using 1 grind -/-- Proposition 6.4.12(a) -/ +/-- Proposition 6.4.12(a') -/ theorem Sequence.lt_liminf_bounds {a:Sequence} {y:EReal} (h: y < a.liminf) : ∃ N ≥ a.m, ∀ n ≥ N, a n > y := by sorry From 38331c6271f5e4fbb1494a0bb2ced8d303bb3767 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:52 +0300 Subject: [PATCH 05/13] Disambiguate Proposition 6.4.12(b') for gt_liminf_bounds. Co-authored-by: Cursor --- Analysis/Section_6_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean index 206085f1a..0c0c0b40b 100644 --- a/Analysis/Section_6_4.lean +++ b/Analysis/Section_6_4.lean @@ -167,7 +167,7 @@ theorem Sequence.lt_limsup_bounds {a:Sequence} {x:EReal} (h: x < a.limsup) {N: choose n hn hxn _ using exists_between_lt_sup hx grind -/-- Proposition 6.4.12(b) -/ +/-- Proposition 6.4.12(b') -/ theorem Sequence.gt_liminf_bounds {a:Sequence} {x:EReal} (h: x > a.liminf) {N:ℤ} (hN: N ≥ a.m) : ∃ n ≥ N, a n < x := by sorry From 59e7a0cc780a2266c93d1fde9620dc91a11d1ea5 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:52 +0300 Subject: [PATCH 06/13] Disambiguate Proposition 6.4.12(c') for liminf_le_limsup. Co-authored-by: Cursor --- Analysis/Section_6_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean index 0c0c0b40b..bcadca6e2 100644 --- a/Analysis/Section_6_4.lean +++ b/Analysis/Section_6_4.lean @@ -175,7 +175,7 @@ theorem Sequence.gt_liminf_bounds {a:Sequence} {x:EReal} (h: x > a.liminf) {N: /-- Proposition 6.4.12(c) / Exercise 6.4.3 -/ theorem Sequence.inf_le_liminf (a:Sequence) : a.inf ≤ a.liminf := by sorry -/-- Proposition 6.4.12(c) / Exercise 6.4.3 -/ +/-- Proposition 6.4.12(c') / Exercise 6.4.3 -/ theorem Sequence.liminf_le_limsup (a:Sequence) : a.liminf ≤ a.limsup := by sorry /-- Proposition 6.4.12(c) / Exercise 6.4.3 -/ From 72f79136c3dea1f39fbfefaa17da543f61d09600 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:52 +0300 Subject: [PATCH 07/13] Disambiguate Proposition 6.4.12(c'') for limsup_le_sup. Co-authored-by: Cursor --- Analysis/Section_6_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean index bcadca6e2..e3fbeb581 100644 --- a/Analysis/Section_6_4.lean +++ b/Analysis/Section_6_4.lean @@ -178,7 +178,7 @@ theorem Sequence.inf_le_liminf (a:Sequence) : a.inf ≤ a.liminf := by sorry /-- Proposition 6.4.12(c') / Exercise 6.4.3 -/ theorem Sequence.liminf_le_limsup (a:Sequence) : a.liminf ≤ a.limsup := by sorry -/-- Proposition 6.4.12(c) / Exercise 6.4.3 -/ +/-- Proposition 6.4.12(c'') / Exercise 6.4.3 -/ theorem Sequence.limsup_le_sup (a:Sequence) : a.limsup ≤ a.sup := by sorry /-- Proposition 6.4.12(d) / Exercise 6.4.3 -/ From 2447307a5a5da878130c5f6b7fb3788436d4ae1e Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:33:52 +0300 Subject: [PATCH 08/13] Disambiguate Proposition 6.4.12(e') for limit_point_of_liminf. Co-authored-by: Cursor --- Analysis/Section_6_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_4.lean b/Analysis/Section_6_4.lean index e3fbeb581..0960398bd 100644 --- a/Analysis/Section_6_4.lean +++ b/Analysis/Section_6_4.lean @@ -191,7 +191,7 @@ theorem Sequence.limit_point_of_limsup {a:Sequence} {L_plus:ℝ} (h: a.limsup = a.LimitPoint L_plus := by sorry -/-- Proposition 6.4.12(e) / Exercise 6.4.3 -/ +/-- Proposition 6.4.12(e') / Exercise 6.4.3 -/ theorem Sequence.limit_point_of_liminf {a:Sequence} {L_minus:ℝ} (h: a.liminf = L_minus) : a.LimitPoint L_minus := by sorry From bc59ac48081c1df230281928f72a4edd29000a38 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:34:15 +0300 Subject: [PATCH 09/13] Disambiguate Theorem 6.2.11(a') for mem_ge_inf. Co-authored-by: Cursor --- Analysis/Section_6_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_2.lean b/Analysis/Section_6_2.lean index 1e4ea084e..e04c4ea80 100644 --- a/Analysis/Section_6_2.lean +++ b/Analysis/Section_6_2.lean @@ -164,7 +164,7 @@ example (E: Set EReal) : sSup E < sInf E ↔ E = ∅ := by sorry /-- Theorem 6.2.11 (a) / Exercise 6.2.2 -/ theorem EReal.mem_le_sup (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sSup E := by sorry -/-- Theorem 6.2.11 (a) / Exercise 6.2.2 -/ +/-- Theorem 6.2.11 (a') / Exercise 6.2.2 -/ theorem EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : sInf E ≤ x := by sorry /-- Theorem 6.2.11 (b) / Exercise 6.2.2 -/ From c4275603cae6c927ee5c42b96d0bd911cc97dec3 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:34:15 +0300 Subject: [PATCH 10/13] Disambiguate Exercise 4.4.2(b') for Rat.pos_infinite_descent. Co-authored-by: Cursor --- Analysis/Section_4_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_4_4.lean b/Analysis/Section_4_4.lean index 3a63507b1..64c42e552 100644 --- a/Analysis/Section_4_4.lean +++ b/Analysis/Section_4_4.lean @@ -53,7 +53,7 @@ def Int.infinite_descent : Decidable (∃ a:ℕ → ℤ, ∀ n, a (n+1) < a n) : -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorry -/-- Exercise 4.4.2 (b) -/ +/-- Exercise 4.4.2 (b') -/ def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n, a (n+1) < a n) := by -- the first line of this construction should be either `apply isTrue` or `apply isFalse`. sorry From aaf92977a3684d31c30a1ae42c56f2c587de6d47 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:35:27 +0300 Subject: [PATCH 11/13] Disambiguate Proposition 6.2.5(b') for not_lt_and_eq. Co-authored-by: Cursor --- Analysis/Section_6_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_2.lean b/Analysis/Section_6_2.lean index e04c4ea80..53a954080 100644 --- a/Analysis/Section_6_2.lean +++ b/Analysis/Section_6_2.lean @@ -80,7 +80,7 @@ theorem EReal.refl (x:EReal) : x ≤ x := by sorry /-- Proposition 6.2.5(b) / Exercise 6.2.1 -/ theorem EReal.trichotomy (x y:EReal) : x < y ∨ x = y ∨ x > y := by sorry -/-- Proposition 6.2.5(b) / Exercise 6.2.1 -/ +/-- Proposition 6.2.5(b') / Exercise 6.2.1 -/ theorem EReal.not_lt_and_eq (x y:EReal) : ¬ (x < y ∧ x = y) := by sorry /-- Proposition 6.2.5(b) / Exercise 6.2.1 -/ From 11edd6cf06b341329e0fdfc1e8cffcca89f78425 Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:35:27 +0300 Subject: [PATCH 12/13] Disambiguate Proposition 6.2.5(b'') for not_gt_and_eq. Co-authored-by: Cursor --- Analysis/Section_6_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_2.lean b/Analysis/Section_6_2.lean index 53a954080..2fdf407f6 100644 --- a/Analysis/Section_6_2.lean +++ b/Analysis/Section_6_2.lean @@ -83,7 +83,7 @@ theorem EReal.trichotomy (x y:EReal) : x < y ∨ x = y ∨ x > y := by sorry /-- Proposition 6.2.5(b') / Exercise 6.2.1 -/ theorem EReal.not_lt_and_eq (x y:EReal) : ¬ (x < y ∧ x = y) := by sorry -/-- Proposition 6.2.5(b) / Exercise 6.2.1 -/ +/-- Proposition 6.2.5(b'') / Exercise 6.2.1 -/ theorem EReal.not_gt_and_eq (x y:EReal) : ¬ (x > y ∧ x = y) := by sorry /-- Proposition 6.2.5(b) / Exercise 6.2.1 -/ From 8d1595d456db4ac4a05b35647a1171cab281fa4e Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 24 Jul 2026 09:36:08 +0300 Subject: [PATCH 13/13] Disambiguate Proposition 6.2.5(b''') for not_lt_and_gt. Co-authored-by: Cursor --- Analysis/Section_6_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_6_2.lean b/Analysis/Section_6_2.lean index 2fdf407f6..b55c98c5c 100644 --- a/Analysis/Section_6_2.lean +++ b/Analysis/Section_6_2.lean @@ -86,7 +86,7 @@ theorem EReal.not_lt_and_eq (x y:EReal) : ¬ (x < y ∧ x = y) := by sorry /-- Proposition 6.2.5(b'') / Exercise 6.2.1 -/ theorem EReal.not_gt_and_eq (x y:EReal) : ¬ (x > y ∧ x = y) := by sorry -/-- Proposition 6.2.5(b) / Exercise 6.2.1 -/ +/-- Proposition 6.2.5(b''') / Exercise 6.2.1 -/ theorem EReal.not_lt_and_gt (x y:EReal) : ¬ (x < y ∧ x > y) := by sorry /-- Proposition 6.2.5(c) / Exercise 6.2.1 -/