Skip to content

fix: disambiguate Verso labels for 3.6.14, 6.4.12, 6.2, and 4.4.2 #608

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Chessing234 wants to merge 18 commits into
base: main
Choose a base branch
from
Open

fix: disambiguate Verso labels for 3.6.14, 6.4.12, 6.2, and 4.4.2 #608

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
f3b01ee
Disambiguate Proposition 3.6.14(b') for card_union_disjoint.
Chessing234 Jul 24, 2026
3eeda8a
Disambiguate Proposition 3.6.14(c') for card_ssubset.
Chessing234 Jul 24, 2026
83e410a
Disambiguate Proposition 3.6.14(d') for card_image_inj.
Chessing234 Jul 24, 2026
2ff8237
Disambiguate Proposition 6.4.12(a') for lt_liminf_bounds.
Chessing234 Jul 24, 2026
38331c6
Disambiguate Proposition 6.4.12(b') for gt_liminf_bounds.
Chessing234 Jul 24, 2026
59e7a0c
Disambiguate Proposition 6.4.12(c') for liminf_le_limsup.
Chessing234 Jul 24, 2026
72f7913
Disambiguate Proposition 6.4.12(c'') for limsup_le_sup.
Chessing234 Jul 24, 2026
2447307
Disambiguate Proposition 6.4.12(e') for limit_point_of_liminf.
Chessing234 Jul 24, 2026
bc59ac4
Disambiguate Theorem 6.2.11(a') for mem_ge_inf.
Chessing234 Jul 24, 2026
c427560
Disambiguate Exercise 4.4.2(b') for Rat.pos_infinite_descent.
Chessing234 Jul 24, 2026
fc21800
Merge Proposition 3.6.14 Verso label fixes.
Chessing234 Jul 24, 2026
36260bf
Merge Proposition 6.4.12 Verso label fixes.
Chessing234 Jul 24, 2026
aaf9297
Disambiguate Proposition 6.2.5(b') for not_lt_and_eq.
Chessing234 Jul 24, 2026
68dfc0c
Merge Section 6.2 Verso label fixes.
Chessing234 Jul 24, 2026
11edd6c
Disambiguate Proposition 6.2.5(b'') for not_gt_and_eq.
Chessing234 Jul 24, 2026
c12e19e
Merge Exercise 4.4.2 Verso label fix.
Chessing234 Jul 24, 2026
8d1595d
Disambiguate Proposition 6.2.5(b''') for not_lt_and_gt.
Chessing234 Jul 24, 2026
16b11ea
Merge remaining Proposition 6.2.5(b''') label fix.
Chessing234 Jul 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Analysis/Section_3_6.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -275,23 +275,23 @@ 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

/-- Proposition 3.6.14 (c) / Exercise 3.6.4 -/
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

/-- Proposition 3.6.14 (d) / Exercise 3.6.4 -/
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

Expand Down
2 changes: 1 addition & 1 deletion Analysis/Section_4_4.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions Analysis/Section_6_2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,13 +80,13 @@ 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 -/
/-- 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 -/
Expand Down Expand Up @@ -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 -/
Expand Down
10 changes: 5 additions & 5 deletions Analysis/Section_6_4.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -167,18 +167,18 @@ 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

/-- 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 -/
/-- 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 -/
Expand All @@ -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
Expand Down
Loading