Skip to content

fix: disambiguate duplicate Verso labels across Chapter 3 #657

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 1 commit into
base: main
Choose a base branch
from
+30 −30
Open

fix: disambiguate duplicate Verso labels across Chapter 3 #657

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
34 changes: 17 additions & 17 deletions Analysis/Section_3_1.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,14 +253,14 @@ abbrev SetTheory.Set.empty : Set := ∅
abbrev SetTheory.Set.singleton_empty : Set := {(empty: Object)}
abbrev SetTheory.Set.pair_empty : Set := {(empty: Object), (singleton_empty: Object)}

/-- Exercise 3.1.2 -/
/-- Exercise 3.1.2 (empty set is not a singleton) -/
theorem SetTheory.Set.emptyset_neq_singleton : empty ≠ singleton_empty := by
sorry

/-- Exercise 3.1.2 -/
/-- Exercise 3.1.2 (empty set is not a pair) -/
theorem SetTheory.Set.emptyset_neq_pair : empty ≠ pair_empty := by sorry

/-- Exercise 3.1.2 -/
/-- Exercise 3.1.2 (singleton is not a pair) -/
theorem SetTheory.Set.singleton_empty_neq_pair : singleton_empty ≠ pair_empty := by
sorry

Expand All @@ -276,15 +276,15 @@ theorem SetTheory.Set.union_congr_left (A A' B:Set) (h: A = A') : A ∪ B = A'
-/
theorem SetTheory.Set.union_congr_right (A B B':Set) (h: B = B') : A ∪ B = A ∪ B' := by sorry

/-- Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3 -/
/-- Lemma 3.1.12 (Basic properties of unions, singletons) / Exercise 3.1.3 -/
theorem SetTheory.Set.singleton_union_singleton (a b:Object) :
({a}:Set) ∪ ({b}:Set) = {a,b} := by
sorry

/-- Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3 -/
/-- Lemma 3.1.12 (Basic properties of unions, commutativity) / Exercise 3.1.3 -/
theorem SetTheory.Set.union_comm (A B:Set) : A ∪ B = B ∪ A := by sorry

/-- Lemma 3.1.12 (Basic properties of unions) / Exercise 3.1.3 -/
/-- Lemma 3.1.12 (Basic properties of unions, associativity) / Exercise 3.1.3 -/
theorem SetTheory.Set.union_assoc (A B C:Set) : (A ∪ B) ∪ C = A ∪ (B ∪ C) := by
-- this proof is written to follow the structure of the original text.
ext x
Expand Down Expand Up @@ -347,15 +347,15 @@ theorem SetTheory.Set.ssubset_def (X Y:Set) : X ⊂ Y ↔ (X ⊆ Y ∧ X ≠ Y)
/-- Remark 3.1.15 -/
theorem SetTheory.Set.subset_congr_left {A A' B:Set} (hAA':A = A') (hAB: A ⊆ B) : A' ⊆ B := by sorry

/-- Examples 3.1.16 -/
/-- Examples 3.1.16 (reflexivity) -/
@[simp, refl]
theorem SetTheory.Set.subset_self (A:Set) : A ⊆ A := by sorry

/-- Examples 3.1.16 -/
/-- Examples 3.1.16 (the empty set is a subset) -/
@[simp]
theorem SetTheory.Set.empty_subset (A:Set) : ∅ ⊆ A := by sorry

/-- Proposition 3.1.17 (Partial ordering by set inclusion) -/
/-- Proposition 3.1.17 (Partial ordering by set inclusion, transitivity) -/
theorem SetTheory.Set.subset_trans {A B C:Set} (hAB:A ⊆ B) (hBC:B ⊆ C) : A ⊆ C := by
-- This proof is written to follow the structure of the original text.
rw [subset_def]
Expand All @@ -365,11 +365,11 @@ theorem SetTheory.Set.subset_trans {A B C:Set} (hAB:A ⊆ B) (hBC:B ⊆ C) : A
apply hBC x at hx
assumption

/-- Proposition 3.1.17 (Partial ordering by set inclusion) -/
/-- Proposition 3.1.17 (Partial ordering by set inclusion, antisymmetry) -/
theorem SetTheory.Set.subset_antisymm (A B:Set) (hAB:A ⊆ B) (hBA:B ⊆ A) : A = B := by
sorry

/-- Proposition 3.1.17 (Partial ordering by set inclusion) -/
/-- Proposition 3.1.17 (Partial ordering by set inclusion, strict transitivity) -/
theorem SetTheory.Set.ssubset_trans (A B C:Set) (hAB:A ⊂ B) (hBC:B ⊂ C) : A ⊂ C := by
sorry

Expand Down Expand Up @@ -425,17 +425,17 @@ lemma SetTheory.Set.subtype_mk_coe {A:Set} {x:Object} (hx:x ∈ A) : A.subtype_m

abbrev SetTheory.Set.specify (A:Set) (P: A → Prop) : Set := SetTheory.specify A P

/-- Axiom 3.6 (axiom of specification) -/
/-- Axiom 3.6 (axiom of specification, membership) -/
theorem SetTheory.Set.specification_axiom {A:Set} {P: A → Prop} {x:Object} (h: x ∈ A.specify P) :
x ∈ A :=
(SetTheory.specification_axiom A P).1 x h

/-- Axiom 3.6 (axiom of specification) -/
/-- Axiom 3.6 (axiom of specification, the property holds) -/
theorem SetTheory.Set.specification_axiom' {A:Set} (P: A → Prop) (x:A) :
x.val ∈ A.specify P ↔ P x :=
(SetTheory.specification_axiom A P).2 x

/-- Axiom 3.6 (axiom of specification) -/
/-- Axiom 3.6 (axiom of specification, the specified set is a subset) -/
@[simp]
theorem SetTheory.Set.specification_axiom'' {A:Set} (P: A → Prop) (x:Object) :
x ∈ A.specify P ↔ ∃ h:x ∈ A, P ⟨ x, h ⟩ := by
Expand Down Expand Up @@ -793,15 +793,15 @@ theorem SetTheory.Set.union_eq_partition (A B:Set) : A ∪ B = (A \ B) ∪ (A
theorem SetTheory.Set.specification_from_replacement {A:Set} {P: A → Prop} :
∃ B, B ⊆ A ∧ ∀ x, x.val ∈ B ↔ P x := by sorry

/-- Exercise 3.1.12. -/
/-- Exercise 3.1.12 (unions) -/
theorem SetTheory.Set.subset_union_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
A' ∪ B' ⊆ A ∪ B := by sorry

/-- Exercise 3.1.12. -/
/-- Exercise 3.1.12 (intersections) -/
theorem SetTheory.Set.subset_inter_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
A' ∩ B' ⊆ A ∩ B := by sorry

/-- Exercise 3.1.12. -/
/-- Exercise 3.1.12 (differences: a counterexample) -/
theorem SetTheory.Set.subset_diff_subset_counter :
∃ (A B A' B':Set), (A' ⊆ A) ∧ (B' ⊆ B) ∧ ¬ (A' \ B') ⊆ (A \ B) := by sorry

Expand Down
8 changes: 4 additions & 4 deletions Analysis/Section_3_2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,17 +110,17 @@ theorem SetTheory.Set.replace_exists (h: axiom_of_universal_specification) (A:Se
∃ (Z:Set), ∀ y, y ∈ Z ↔ ∃ a : A, P a y := by
sorry

/-- Exercise 3.2.2 -/
/-- Exercise 3.2.2 (no set contains itself) -/
theorem SetTheory.Set.not_mem_self (A:Set) : (A:Object) ∉ A := by sorry

/-- Exercise 3.2.2 -/
/-- Exercise 3.2.2 (no two sets contain each other) -/
theorem SetTheory.Set.not_mem_mem (A B:Set) : (A:Object) ∉ B ∨ (B:Object) ∉ A := by sorry

/-- Exercise 3.2.3 -/
/-- Exercise 3.2.3 (universal specification) -/
theorem SetTheory.Set.univ_iff : axiom_of_universal_specification ↔
∃ (U:Set), ∀ x, x ∈ U := by sorry

/-- Exercise 3.2.3 -/
/-- Exercise 3.2.3 (there is no universal set) -/
theorem SetTheory.Set.no_univ : ¬ ∃ (U:Set), ∀ (x:Object), x ∈ U := by sorry


Expand Down
14 changes: 7 additions & 7 deletions Analysis/Section_3_4.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -309,11 +309,11 @@ theorem SetTheory.Set.preimage_of_union {X Y:Set} (f:X → Y) (A B: Set) :
theorem SetTheory.Set.preimage_of_diff {X Y:Set} (f:X → Y) (A B: Set) :
preimage f (A \ B) = (preimage f A) \ (preimage f B) := by sorry

/-- Exercise 3.4.5 -/
/-- Exercise 3.4.5 (image of a preimage) -/
theorem SetTheory.Set.image_preimage_of_surj {X Y:Set} (f:X → Y) :
(∀ S, S ⊆ Y → image f (preimage f S) = S) ↔ Function.Surjective f := by sorry

/-- Exercise 3.4.5 -/
/-- Exercise 3.4.5 (preimage of an image) -/
theorem SetTheory.Set.preimage_image_of_inj {X Y:Set} (f:X → Y) :
(∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by sorry

Expand Down Expand Up @@ -344,26 +344,26 @@ theorem SetTheory.Set.union_pair_exists (X Y:Set) : ∃ Z:Set, ∀ x, x ∈ Z
theorem SetTheory.Set.iInter'_insensitive {I:Set} (β β':I) (A: I → Set) :
iInter' I β A = iInter' I β' A := by sorry

/-- Exercise 3.4.10 -/
/-- Exercise 3.4.10 (union over a union of index sets) -/
theorem SetTheory.Set.union_iUnion {I J:Set} (A: (I ∪ J:Set) → Set) :
iUnion I (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
∪ iUnion J (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
= iUnion (I ∪ J) A := by sorry

/-- Exercise 3.4.10 -/
/-- Exercise 3.4.10 (a union of nonempty index sets is nonempty) -/
theorem SetTheory.Set.union_of_nonempty {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) : I ∪ J ≠ ∅ := by sorry

/-- Exercise 3.4.10 -/
/-- Exercise 3.4.10 (intersection over a union of index sets) -/
theorem SetTheory.Set.inter_iInter {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) (A: (I ∪ J:Set) → Set) :
iInter I hI (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
∩ iInter J hJ (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
= iInter (I ∪ J) (union_of_nonempty hI hJ) A := by sorry

/-- Exercise 3.4.11 -/
/-- Exercise 3.4.11 (complement of a union) -/
theorem SetTheory.Set.compl_iUnion {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
X \ iUnion I A = iInter I hI (fun α ↦ X \ A α) := by sorry

/-- Exercise 3.4.11 -/
/-- Exercise 3.4.11 (complement of an intersection) -/
theorem SetTheory.Set.compl_iInter {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
X \ iInter I hI A = iUnion I (fun α ↦ X \ A α) := by sorry

Expand Down
4 changes: 2 additions & 2 deletions Analysis/Section_3_5.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,11 +171,11 @@ noncomputable abbrev SetTheory.Set.curry_equiv {X Y Z:Set} : (X → Y → Z) ≃
abbrev SetTheory.Set.tuple {I:Set} {X: I → Set} (x: ∀ i, X i) : Object :=
((fun i ↦ ⟨ x i, by rw [mem_iUnion]; use i; exact (x i).property ⟩):I → iUnion I X)

/-- Definition 3.5.6 -/
/-- Definition 3.5.6 (indexed product) -/
abbrev SetTheory.Set.iProd {I: Set} (X: I → Set) : Set :=
((iUnion I X)^I).specify (fun t ↦ ∃ x : ∀ i, X i, t = tuple x)

/-- Definition 3.5.6 -/
/-- Definition 3.5.6 (membership in an indexed product) -/
theorem SetTheory.Set.mem_iProd {I: Set} {X: I → Set} (t:Object) :
t ∈ iProd X ↔ ∃ x: ∀ i, X i, t = tuple x := by
simp only [iProd, specification_axiom'']; constructor
Expand Down
Loading