From f215a3180a9662036f1f638ef7b572c22f9d4d04 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 11 Nov 2023 15:15:03 -0700 Subject: [PATCH] Enderton (set). Chapter 6 formatting. More consistent header levels throughout. --- Bookshelf/Apostol/Chapter_1_11.lean | 18 +- Bookshelf/Apostol/Chapter_I_03.lean | 48 +-- Bookshelf/Avigad/Chapter_2.lean | 10 +- Bookshelf/Avigad/Chapter_3.lean | 8 +- Bookshelf/Avigad/Chapter_4.lean | 12 +- Bookshelf/Avigad/Chapter_5.lean | 18 +- Bookshelf/Avigad/Chapter_7.lean | 8 +- Bookshelf/Avigad/Chapter_8.lean | 16 +- Bookshelf/Enderton/Logic/Chapter_1.lean | 22 +- Bookshelf/Enderton/Set.tex | 2 +- Bookshelf/Enderton/Set/Chapter_1.lean | 10 +- Bookshelf/Enderton/Set/Chapter_2.lean | 68 +-- Bookshelf/Enderton/Set/Chapter_3.lean | 124 +++--- Bookshelf/Enderton/Set/Chapter_4.lean | 66 +-- Bookshelf/Enderton/Set/Chapter_6.lean | 541 +++++++++++++++--------- Bookshelf/Enderton/Set/OrderedPair.lean | 20 +- Bookshelf/Enderton/Set/Relation.lean | 8 +- Bookshelf/Smullyan/Aviary.lean | 76 ++-- Common/Set/Equinumerous.lean | 8 +- 19 files changed, 605 insertions(+), 478 deletions(-) diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean index b0dd582..c41d6eb 100644 --- a/Bookshelf/Apostol/Chapter_1_11.lean +++ b/Bookshelf/Apostol/Chapter_1_11.lean @@ -8,21 +8,21 @@ namespace Apostol.Chapter_1_11 open BigOperators -/-- #### Exercise 4a +/-- ### Exercise 4a `⌊x + n⌋ = ⌊x⌋ + n` for every integer `n`. -/ theorem exercise_4a (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n := Int.floor_add_int x n -/-- #### Exercise 4b.1 +/-- ### Exercise 4b.1 `⌊-x⌋ = -⌊x⌋` if `x` is an integer. -/ theorem exercise_4b_1 (x : ℤ) : ⌊-x⌋ = -⌊x⌋ := by simp only [Int.floor_int, id_eq] -/-- #### Exercise 4b.2 +/-- ### Exercise 4b.2 `⌊-x⌋ = -⌊x⌋ - 1` otherwise. -/ @@ -42,7 +42,7 @@ theorem exercise_4b_2 (x : ℝ) (h : ∃ n : ℤ, x ∈ Set.Ioo ↑n (↑n + (1 · exact (Set.mem_Ioo.mp hn).left · exact le_of_lt (Set.mem_Ico.mp hn').right -/-- #### Exercise 4c +/-- ### Exercise 4c `⌊x + y⌋ = ⌊x⌋ + ⌊y⌋` or `⌊x⌋ + ⌊y⌋ + 1`. -/ @@ -72,7 +72,7 @@ theorem exercise_4c (x y : ℝ) rw [← sub_lt_iff_lt_add', ← sub_sub, add_sub_cancel, add_sub_cancel] exact add_lt_add (Int.fract_lt_one x) (Int.fract_lt_one y) -/-- #### Exercise 5 +/-- ### Exercise 5 The formulas in Exercises 4(d) and 4(e) suggest a generalization for `⌊nx⌋`. State and prove such a generalization. @@ -81,7 +81,7 @@ theorem exercise_5 (n : ℕ) (x : ℝ) : ⌊n * x⌋ = Finset.sum (Finset.range n) (fun i => ⌊x + i/n⌋) := Real.Floor.floor_mul_eq_sum_range_floor_add_index_div n x -/-- #### Exercise 4d +/-- ### Exercise 4d `⌊2x⌋ = ⌊x⌋ + ⌊x + 1/2⌋` -/ @@ -94,7 +94,7 @@ theorem exercise_4d (x : ℝ) simp rw [add_comm] -/-- #### Exercise 4e +/-- ### Exercise 4e `⌊3x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋` -/ @@ -108,7 +108,7 @@ theorem exercise_4e (x : ℝ) conv => rhs; rw [← add_rotate']; arg 2; rw [add_comm] rw [← add_assoc] -/-- #### Exercise 7b +/-- ### Exercise 7b If `a` and `b` are positive integers with no common factor, we have the formula `∑_{n=1}^{b-1} ⌊na / b⌋ = ((a - 1)(b - 1)) / 2`. When `b = 1`, the sum on the @@ -125,7 +125,7 @@ theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.Coprime a b) section -/-- #### Exercise 8 +/-- ### Exercise 8 Let `S` be a set of points on the real line. The *characteristic function* of `S` is, by definition, the function `Χ` such that `Χₛ(x) = 1` for every `x` in diff --git a/Bookshelf/Apostol/Chapter_I_03.lean b/Bookshelf/Apostol/Chapter_I_03.lean index ff1ddce..2c8fc46 100644 --- a/Bookshelf/Apostol/Chapter_I_03.lean +++ b/Bookshelf/Apostol/Chapter_I_03.lean @@ -100,7 +100,7 @@ theorem is_lub_neg_set_iff_is_glb_set_neg (S : Set ℝ) _ = IsGreatest (lowerBounds S) (-x) := by rw [is_least_neg_set_eq_is_greatest_set_neq] _ = IsGLB S (-x) := rfl -/-- #### Theorem I.27 +/-- ### Theorem I.27 Every nonempty set `S` that is bounded below has a greatest lower bound; that is, there is a real number `L` such that `L = inf S`. @@ -143,11 +143,11 @@ lemma leq_nat_abs_ceil_self (x : ℝ) : x ≤ Int.natAbs ⌈x⌉ := by · have h' : ((Int.natAbs ⌈x⌉) : ℝ) ≥ 0 := by simp calc x _ ≤ 0 := le_of_lt (lt_of_not_le h) - _ ≤ ↑(Int.natAbs ⌈x⌉) := GE.ge.le h' + _ ≤ ↑(Int.natAbs ⌈x⌉) := GE.ge.le h' /-! ## The Archimedean property of the real-number system -/ -/-- #### Theorem I.29 +/-- ### Theorem I.29 For every real `x` there exists a positive integer `n` such that `n > x`. -/ @@ -159,7 +159,7 @@ theorem exists_pnat_geq_self (x : ℝ) : ∃ n : ℕ+, ↑n > x := by _ = n := rfl exact ⟨n, this⟩ -/-- #### Theorem I.30 +/-- ### Theorem I.30 If `x > 0` and if `y` is an arbitrary real number, there exists a positive integer `n` such that `nx > y`. @@ -174,7 +174,7 @@ theorem exists_pnat_mul_self_geq_of_pos {x y : ℝ} rw [div_mul, div_self (show x ≠ 0 from LT.lt.ne' hx), div_one] at p' exact ⟨n, p'⟩ -/-- #### Theorem I.31 +/-- ### Theorem I.31 If three real numbers `a`, `x`, and `y` satisfy the inequalities `a ≤ x ≤ a + y / n` for every integer `n ≥ 1`, then `x = a`. @@ -243,7 +243,7 @@ theorem forall_pnat_frac_leq_self_leq_imp_eq {x y a : ℝ} /-- Every member of a set `S` is less than or equal to some value `ub` if and only -if `ub` is an upper bound of `S`. +if `ub` is an upper bound of `S`. -/ lemma mem_upper_bounds_iff_forall_le {S : Set ℝ} : ub ∈ upperBounds S ↔ ∀ x ∈ S, x ≤ ub := by @@ -270,7 +270,7 @@ lemma mem_imp_ge_lub {x : ℝ} (h : IsLUB S s) : x ∈ upperBounds S → x ≥ s intro hx exact h.right hx -/-- #### Theorem I.32a +/-- ### Theorem I.32a Let `h` be a given positive number and let `S` be a set of real numbers. If `S` has a supremum, then for some `x` in `S` we have `x > sup S - h`. @@ -294,7 +294,7 @@ theorem sup_imp_exists_gt_sup_sub_delta {S : Set ℝ} {s h : ℝ} (hp : h > 0) /-- Every member of a set `S` is greater than or equal to some value `lb` if and -only if `lb` is a lower bound of `S`. +only if `lb` is a lower bound of `S`. -/ lemma mem_lower_bounds_iff_forall_ge {S : Set ℝ} : lb ∈ lowerBounds S ↔ ∀ x ∈ S, x ≥ lb := by @@ -321,7 +321,7 @@ lemma mem_imp_le_glb {x : ℝ} (h : IsGLB S s) : x ∈ lowerBounds S → x ≤ s intro hx exact h.right hx -/-- #### Theorem I.32b +/-- ### Theorem I.32b Let `h` be a given positive number and let `S` be a set of real numbers. If `S` has an infimum, then for some `x` in `S` we have `x < inf S + h`. @@ -343,7 +343,7 @@ theorem inf_imp_exists_lt_inf_add_delta {S : Set ℝ} {s h : ℝ} (hp : h > 0) exact le_of_not_gt (not_and.mp (nb x) hx) rwa [← mem_lower_bounds_iff_forall_ge] at nb' -/-- #### Theorem I.33a (Additive Property) +/-- ### Theorem I.33a (Additive Property) Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set `C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has a supremum, then `C` @@ -393,7 +393,7 @@ theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ) _ ≤ a' + b' + 1 / n := le_of_lt hab' _ ≤ c + 1 / n := add_le_add_right hc' (1 / n) -/-- #### Theorem I.33b (Additive Property) +/-- ### Theorem I.33b (Additive Property) Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set `C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has an infimum, then `C` @@ -443,7 +443,7 @@ theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ) _ ≤ a + b := le_of_lt hab' · exact hc.right hlb -/-- #### Theorem I.34 +/-- ### Theorem I.34 Given two nonempty subsets `S` and `T` of `ℝ` such that `s ≤ t` for every `s` in `S` and every `t` in `T`. Then `S` has a supremum, and `T` has an infimum, and @@ -489,7 +489,7 @@ theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ) _ < x := hx.right simp at this -/-- #### Exercise 1 +/-- ### Exercise 1 If `x` and `y` are arbitrary real numbers with `x < y`, prove that there is at least one real `z` satisfying `x < z < y`. @@ -506,7 +506,7 @@ theorem exercise_1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by _ < x + z := (add_lt_add_iff_left x).mpr hz' _ = y := hz.right -/-- #### Exercise 2 +/-- ### Exercise 2 If `x` is an arbitrary real number, prove that there are integers `m` and `n` such that `m < x < n`. @@ -514,7 +514,7 @@ such that `m < x < n`. theorem exercise_2 (x : ℝ) : ∃ m n : ℝ, m < x ∧ x < n := by refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num -/-- #### Exercise 3 +/-- ### Exercise 3 If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`. -/ @@ -525,7 +525,7 @@ theorem exercise_3 (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by conv at hr => arg 2; rw [mul_comm, ← mul_assoc]; simp rwa [one_mul] at hr -/-- #### Exercise 4 +/-- ### Exercise 4 If `x` is an arbitrary real number, prove that there is exactly one integer `n` which satisfies the inequalities `n ≤ x < n + 1`. This `n` is called the @@ -540,7 +540,7 @@ theorem exercise_4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by rw [← Int.floor_eq_iff] at hy exact Eq.symm hy -/-- #### Exercise 5 +/-- ### Exercise 5 If `x` is an arbitrary real number, prove that there is exactly one integer `n` which satisfies `x ≤ n < x + 1`. @@ -559,7 +559,7 @@ theorem exercise_5 (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by rwa [add_sub_cancel] at this · exact hy.left -/-! #### Exercise 6 +/-! ### Exercise 6 If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists at least one rational number `r` satisfying `x < r < y`, and hence infinitely many. @@ -569,7 +569,7 @@ in the real-number system. ###### TODO -/ -/-! #### Exercise 7 +/-! ### Exercise 7 If `x` is rational, `x ≠ 0`, and `y` irrational, prove that `x + y`, `x - y`, `xy`, `x / y`, and `y / x` are all irrational. @@ -577,14 +577,14 @@ If `x` is rational, `x ≠ 0`, and `y` irrational, prove that `x + y`, `x - y`, ###### TODO -/ -/-! #### Exercise 8 +/-! ### Exercise 8 Is the sum or product of two irrational numbers always irrational? ###### TODO -/ -/-! #### Exercise 9 +/-! ### Exercise 9 If `x` and `y` are arbitrary real numbers, `x < y`, prove that there exists at least one irrational number `z` satisfying `x < z < y`, and hence infinitely @@ -593,7 +593,7 @@ many. ###### TODO -/ -/-! #### Exercise 10 +/-! ### Exercise 10 An integer `n` is called *even* if `n = 2m` for some integer `m`, and *odd* if `n + 1` is even. Prove the following statements: @@ -618,7 +618,7 @@ def isEven (n : ℤ) := ∃ m : ℤ, n = 2 * m def isOdd (n : ℤ) := isEven (n + 1) -/-! #### Exercise 11 +/-! ### Exercise 11 Prove that there is no rational number whose square is `2`. @@ -629,7 +629,7 @@ contradiction.] ###### TODO -/ -/-! #### Exercise 12 +/-! ### Exercise 12 The Archimedean property of the real-number system was deduced as a consequence of the least-upper-bound axiom. Prove that the set of rational numbers satisfies diff --git a/Bookshelf/Avigad/Chapter_2.lean b/Bookshelf/Avigad/Chapter_2.lean index d96a4d4..88694c3 100644 --- a/Bookshelf/Avigad/Chapter_2.lean +++ b/Bookshelf/Avigad/Chapter_2.lean @@ -3,7 +3,7 @@ Dependent Type Theory -/ -/-! #### Exercise 1 +/-! ### Exercise 1 Define the function `Do_Twice`, as described in Section 2.4. -/ @@ -20,7 +20,7 @@ def doTwiceTwice (f : (Nat → Nat) → (Nat → Nat)) (x : Nat → Nat) := f (f end ex1 -/-! #### Exercise 2 +/-! ### Exercise 2 Define the functions `curry` and `uncurry`, as described in Section 2.4. -/ @@ -35,7 +35,7 @@ def uncurry (f : α → β → γ) : (α × β → γ) := end ex2 -/-! #### Exercise 3 +/-! ### Exercise 3 Above, we used the example `vec α n` for vectors of elements of type `α` of length `n`. Declare a constant `vec_add` that could represent a function that @@ -70,7 +70,7 @@ variable (c d : vec Prop 2) end ex3 -/-! #### Exercise 4 +/-! ### Exercise 4 Similarly, declare a constant `matrix` so that `matrix α m n` could represent the type of `m` by `n` matrices. Declare some constants to represent functions @@ -106,4 +106,4 @@ variable (d : ex3.vec Prop 3) end ex4 -end Avigad.Chapter2 \ No newline at end of file +end Avigad.Chapter2 diff --git a/Bookshelf/Avigad/Chapter_3.lean b/Bookshelf/Avigad/Chapter_3.lean index b83855f..a9bdf9c 100644 --- a/Bookshelf/Avigad/Chapter_3.lean +++ b/Bookshelf/Avigad/Chapter_3.lean @@ -3,7 +3,7 @@ Propositions and Proofs -/ -/-! #### Exercise 1 +/-! ### Exercise 1 Prove the following identities. -/ @@ -104,7 +104,7 @@ theorem imp_imp_not_imp_not : (p → q) → (¬q → ¬p) := end ex1 -/-! #### Exercise 2 +/-! ### Exercise 2 Prove the following identities. These require classical reasoning. -/ @@ -150,7 +150,7 @@ theorem imp_imp_imp : (((p → q) → p) → p) := end ex2 -/-! #### Exercise 3 +/-! ### Exercise 3 Prove `¬(p ↔ ¬p)` without using classical logic. -/ @@ -164,4 +164,4 @@ theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) := end ex3 -end Avigad.Chapter3 \ No newline at end of file +end Avigad.Chapter3 diff --git a/Bookshelf/Avigad/Chapter_4.lean b/Bookshelf/Avigad/Chapter_4.lean index 793d823..4e8d2b4 100644 --- a/Bookshelf/Avigad/Chapter_4.lean +++ b/Bookshelf/Avigad/Chapter_4.lean @@ -40,7 +40,7 @@ theorem forall_or_distrib end ex1 -/-! #### Exercise 2 +/-! ### Exercise 2 It is often possible to bring a component of a formula outside a universal quantifier, when it does not depend on the quantified variable. Try proving @@ -78,7 +78,7 @@ theorem forall_swap : (∀ x, r → p x) ↔ (r → ∀ x, p x) := end ex2 -/-! #### Exercise 3 +/-! ### Exercise 3 Consider the "barber paradox," that is, the claim that in a certain town there is a (male) barber that shaves all and only the men who do not shave themselves. @@ -101,7 +101,7 @@ theorem barber_paradox (h : ∀ x : men, shaves barber x ↔ ¬shaves x x) : Fal end ex3 -/-! #### Exercise 4 +/-! ### Exercise 4 Remember that, without any parameters, an expression of type `Prop` is just an assertion. Fill in the definitions of `prime` and `Fermat_prime` below, and @@ -143,7 +143,7 @@ def Fermat'sLastTheorem : Prop := end ex4 -/-! #### Exercise 5 +/-! ### Exercise 5 Prove as many of the identities listed in Section 4.4 as you can. -/ @@ -228,7 +228,7 @@ theorem exists_self_iff_self_exists (a : α) : (∃ x, r → p x) ↔ (r → ∃ end ex5 -/-! #### Exercise 6 +/-! ### Exercise 6 Give a calculational proof of the theorem `log_mul` below. -/ @@ -258,4 +258,4 @@ theorem log_mul {x y : Float} (hx : x > 0) (hy : y > 0) : end ex6 -end Avigad.Chapter4 \ No newline at end of file +end Avigad.Chapter4 diff --git a/Bookshelf/Avigad/Chapter_5.lean b/Bookshelf/Avigad/Chapter_5.lean index 0829235..ea4f169 100644 --- a/Bookshelf/Avigad/Chapter_5.lean +++ b/Bookshelf/Avigad/Chapter_5.lean @@ -13,7 +13,7 @@ namespace Avigad.Chapter5 namespace ex1 -/-! ##### Exercises 3.1 -/ +/-! #### Exercises 3.1 -/ section ex3_1 @@ -154,7 +154,7 @@ theorem imp_imp_not_imp_not : (p → q) → (¬q → ¬p) := by end ex3_1 -/-! ##### Exercises 3.2 -/ +/-! #### Exercises 3.2 -/ section ex3_2 @@ -223,7 +223,7 @@ theorem imp_imp_imp : (((p → q) → p) → p) := by end ex3_2 -/-! ##### Exercises 3.3 -/ +/-! #### Exercises 3.3 -/ section ex3_3 @@ -235,7 +235,7 @@ theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) := by end ex3_3 -/-! ##### Exercises 4.1 -/ +/-! #### Exercises 4.1 -/ section ex4_1 @@ -264,7 +264,7 @@ theorem forall_or_distrib : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x end ex4_1 -/-! ##### Exercises 4.2 -/ +/-! #### Exercises 4.2 -/ section ex4_2 @@ -316,7 +316,7 @@ theorem forall_swap : (∀ x, r → p x) ↔ (r → ∀ x, p x) := by end ex4_2 -/-! ##### Exercises 4.3 -/ +/-! #### Exercises 4.3 -/ section ex4_3 @@ -336,7 +336,7 @@ theorem barber_paradox (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) end ex4_3 -/-! ##### Exercises 4.5 -/ +/-! #### Exercises 4.5 -/ section ex4_5 @@ -448,7 +448,7 @@ end ex4_5 end ex1 -/-! #### Exercise 2 +/-! ### Exercise 2 Use tactic combinators to obtain a one line proof of the following: -/ @@ -461,4 +461,4 @@ theorem or_and_or_and_or (p q r : Prop) (hp : p) end ex2 -end Avigad.Chapter5 \ No newline at end of file +end Avigad.Chapter5 diff --git a/Bookshelf/Avigad/Chapter_7.lean b/Bookshelf/Avigad/Chapter_7.lean index 404a135..354ad48 100644 --- a/Bookshelf/Avigad/Chapter_7.lean +++ b/Bookshelf/Avigad/Chapter_7.lean @@ -5,7 +5,7 @@ Inductive Types namespace Avigad.Chapter7 -/-! #### Exercise 1 +/-! ### Exercise 1 Try defining other operations on the natural numbers, such as multiplication, the predecessor function (with `pred 0 = 0`), truncated subtraction (with @@ -77,7 +77,7 @@ end Nat end ex1 -/-! #### Exercise 2 +/-! ### Exercise 2 Define some operations on lists, like a `length` function or the `reverse` function. Prove some properties, such as the following: @@ -178,7 +178,7 @@ theorem reverse_reverse (t : List α) end ex2 -/-! #### Exercise 3 +/-! ### Exercise 3 Define an inductive data type consisting of terms built up from the following constructors: @@ -217,4 +217,4 @@ def eval_foo : Foo → List Nat → Nat end ex3 -end Avigad.Chapter7 \ No newline at end of file +end Avigad.Chapter7 diff --git a/Bookshelf/Avigad/Chapter_8.lean b/Bookshelf/Avigad/Chapter_8.lean index 1673b4d..299ee98 100644 --- a/Bookshelf/Avigad/Chapter_8.lean +++ b/Bookshelf/Avigad/Chapter_8.lean @@ -5,7 +5,7 @@ Induction and Recursion namespace Avigad.Chapter8 -/-! #### Exercise 1 +/-! ### Exercise 1 Open a namespace `Hidden` to avoid naming conflicts, and use the equation compiler to define addition, multiplication, and exponentiation on the natural @@ -29,7 +29,7 @@ def exp : Nat → Nat → Nat end ex1 -/-! #### Exercise 2 +/-! ### Exercise 2 Similarly, use the equation compiler to define some basic operations on lists (like the reverse function) and prove theorems about lists by induction (such as @@ -48,7 +48,7 @@ def reverse : List α → List α end ex2 -/-! #### Exercise 3 +/-! ### Exercise 3 Define your own function to carry out course-of-value recursion on the natural numbers. Similarly, see if you can figure out how to define `WellFounded.fix` on @@ -86,7 +86,7 @@ noncomputable def brecOn {motive : Nat → Sort u} end ex3 -/-! #### Exercise 4 +/-! ### Exercise 4 Following the examples in Section Dependent Pattern Matching, define a function that will append two vectors. This is tricky; you will have to define an @@ -113,7 +113,7 @@ end Vector end ex4 -/-! #### Exercise 5 +/-! ### Exercise 5 Consider the following type of arithmetic expressions. -/ @@ -149,7 +149,7 @@ def sampleVal : Nat → Nat -- Try it out. You should get 47 here. #eval eval sampleVal sampleExpr -/-! ##### Constant Fusion +/-! ### Constant Fusion Implement "constant fusion," a procedure that simplifies subterms like `5 + 7 to `12`. Using the auxiliary function `simpConst`, define a function "fuse": to @@ -189,7 +189,7 @@ theorem simpConst_eq (v : Nat → Nat) | times _ (var _) | times _ (plus _ _) | times _ (times _ _) => simp only - + theorem fuse_eq (v : Nat → Nat) : ∀ e : Expr, eval v (fuse e) = eval v e := by @@ -206,4 +206,4 @@ theorem fuse_eq (v : Nat → Nat) end ex5 -end Avigad.Chapter8 \ No newline at end of file +end Avigad.Chapter8 diff --git a/Bookshelf/Enderton/Logic/Chapter_1.lean b/Bookshelf/Enderton/Logic/Chapter_1.lean index 561b3de..beb9e81 100644 --- a/Bookshelf/Enderton/Logic/Chapter_1.lean +++ b/Bookshelf/Enderton/Logic/Chapter_1.lean @@ -131,7 +131,7 @@ lemma no_neg_sentential_count_eq_binary_count {φ : Wff} (h : ¬φ.hasNotSymbol) unfold sententialSymbolCount binarySymbolCount rw [ih₁ h.left, ih₂ h.right] -/-- #### Parentheses Count +/-- ### Parentheses Count Let `φ` be a well-formed formula and `c` be the number of places at which a sentential connective symbol exists. Then there is `2c` parentheses in `φ`. @@ -180,7 +180,7 @@ theorem length_eq_sum_symbol_count (φ : Wff) end Wff -/-! #### Exercise 1.1.2 +/-! ### Exercise 1.1.2 Show that there are no wffs of length `2`, `3`, or `6`, but that any other positive length is possible. @@ -296,7 +296,7 @@ theorem exercise_1_1_2_ii (n : ℕ) (hn : n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 6) end Exercise_1_1_2 -/-- #### Exercise 1.1.3 +/-- ### Exercise 1.1.3 Let `α` be a wff; let `c` be the number of places at which binary connective symbols (`∧`, `∨`, `→`, `↔`) occur in `α`; let `s` be the number of places at @@ -320,7 +320,7 @@ theorem exercise_1_1_3 (φ : Wff) rw [ih₁, ih₂] ring -/-- #### Exercise 1.1.5 (a) +/-- ### Exercise 1.1.5 (a) Suppose that `α` is a wff not containing the negation symbol `¬`. Show that the length of `α` (i.e., the number of symbols in the string) is odd. @@ -355,7 +355,7 @@ theorem exercise_1_1_5a (α : Wff) (hα : ¬α.hasNotSymbol) rw [hk₁, hk₂] ring -/-- #### Exercise 1.1.5 (b) +/-- ### Exercise 1.1.5 (b) Suppose that `α` is a wff not containing the negation symbol `¬`. Show that more than a quarter of the symbols are sentence symbols. @@ -390,7 +390,7 @@ theorem exercise_1_1_5b (α : Wff) (hα : ¬α.hasNotSymbol) ] exact inv_lt_one (by norm_num) -/-! #### Exercise 1.2.1 +/-! ### Exercise 1.2.1 Show that neither of the following two formulas tautologically implies the other: @@ -430,7 +430,7 @@ theorem exercise_1_2_2a (P Q : Prop) : (((P → Q) → P) → P) := by tauto -/-! #### Exercise 1.2.2 (b) +/-! ### Exercise 1.2.2 (b) Define `σₖ` recursively as follows: `σ₀ = (P → Q)` and `σₖ₊₁ = (σₖ → P)`. For which values of `k` is `σₖ` a tautology? (Part (a) corresponds to `k = 2`.) @@ -486,7 +486,7 @@ theorem exercise_1_2_2b_iii {k : ℕ} (h : Odd k) end Exercise_1_2_2 -/-- #### Exercise 1.2.3 (a) +/-- ### Exercise 1.2.3 (a) Determine whether or not `((P → Q)) ∨ (Q → P)` is a tautology. -/ @@ -494,7 +494,7 @@ theorem exercise_1_2_3a (P Q : Prop) : ((P → Q) ∨ (Q → P)) := by tauto -/-- #### Exercise 1.2.3 (b) +/-- ### Exercise 1.2.3 (b) Determine whether or not `((P ∧ Q) → R))` tautologically implies `((P → R) ∨ (Q → R))`. @@ -503,7 +503,7 @@ theorem exercise_1_2_3b (P Q R : Prop) : ((P ∧ Q) → R) ↔ ((P → R) ∨ (Q → R)) := by tauto -/-! #### Exercise 1.2.5 +/-! ### Exercise 1.2.5 Prove or refute each of the following assertions: @@ -519,7 +519,7 @@ theorem exercise_1_2_6b : (False ∨ True) ∧ ¬ False := by simp -/-! #### Exercise 1.2.15 +/-! ### Exercise 1.2.15 Of the following three formulas, which tautologically implies which? (a) `(A ↔ B)` diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 84052fc..27fb874 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -8999,7 +8999,7 @@ \begin{proof} Let $S$ be a \nameref{ref:finite-set} and $S'$ be a - \nameref{ref:proper-subset} $S'$ of $S$. + \nameref{ref:proper-subset} of $S$. Then there exists some set $T$, disjoint from $S'$, such that $S' \cup T = S$. By definition of a \nameref{ref:finite-set}, $S$ is diff --git a/Bookshelf/Enderton/Set/Chapter_1.lean b/Bookshelf/Enderton/Set/Chapter_1.lean index f43f122..c6da2c7 100644 --- a/Bookshelf/Enderton/Set/Chapter_1.lean +++ b/Bookshelf/Enderton/Set/Chapter_1.lean @@ -19,7 +19,7 @@ The `∅` does not equal the singleton set containing `∅`. lemma empty_ne_singleton_empty (h : ∅ = ({∅} : Set (Set α))) : False := absurd h (Ne.symm $ Set.singleton_ne_empty (∅ : Set α)) -/-- #### Exercise 1.1a +/-- ### Exercise 1.1a `{∅} ___ {∅, {∅}}` -/ @@ -27,7 +27,7 @@ theorem exercise_1_1a : {∅} ∈ ({∅, {∅}} : Set (Set (Set α))) ∧ {∅} ⊆ ({∅, {∅}} : Set (Set (Set α))) := ⟨by simp, by simp⟩ -/-- #### Exercise 1.1b +/-- ### Exercise 1.1b `{∅} ___ {∅, {{∅}}}` -/ @@ -39,7 +39,7 @@ theorem exercise_1_1b simp at h exact empty_ne_singleton_empty h -/-- #### Exercise 1.1c +/-- ### Exercise 1.1c `{{∅}} ___ {∅, {∅}}` -/ @@ -47,7 +47,7 @@ theorem exercise_1_1c : {{∅}} ∉ ({∅, {∅}} : Set (Set (Set (Set α)))) ∧ {{∅}} ⊆ ({∅, {∅}} : Set (Set (Set (Set α)))) := ⟨by simp, by simp⟩ -/-- #### Exercise 1.1d +/-- ### Exercise 1.1d `{{∅}} ___ {∅, {{∅}}}` -/ @@ -59,7 +59,7 @@ theorem exercise_1_1d simp at h exact empty_ne_singleton_empty h -/-- #### Exercise 1.1e +/-- ### Exercise 1.1e `{{∅}} ___ {∅, {∅, {∅}}}` -/ diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index ffc34b5..848dbab 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -10,7 +10,7 @@ Axioms and Operations namespace Enderton.Set.Chapter_2 -/-! #### Commutative Laws +/-! ### Commutative Laws For any sets `A` and `B`, ``` @@ -40,7 +40,7 @@ theorem commutative_law_ii (A B : Set α) #check Set.inter_comm -/-! #### Associative Laws +/-! ### Associative Laws For any sets `A`, `B`, and `C`, ``` @@ -75,7 +75,7 @@ theorem associative_law_ii (A B C : Set α) #check Set.inter_assoc -/-! #### Distributive Laws +/-! ### Distributive Laws For any sets `A`, `B`, and `C`, ``` @@ -108,7 +108,7 @@ theorem distributive_law_ii (A B C : Set α) #check Set.union_distrib_left -/-! #### De Morgan's Laws +/-! ### De Morgan's Laws For any sets `A`, `B`, and `C`, ``` @@ -149,7 +149,7 @@ theorem de_morgans_law_ii (A B C : Set α) #check Set.diff_inter -/-! #### Identities Involving ∅ +/-! ### Identities Involving ∅ For any set `A`, ``` @@ -185,7 +185,7 @@ theorem emptyset_identity_iii (A C : Set α) #check Set.inter_diff_self -/-! #### Monotonicity +/-! ### Monotonicity For any sets `A`, `B`, and `C`, ``` @@ -229,7 +229,7 @@ theorem monotonicity_iii (A B : Set (Set α)) (h : A ⊆ B) #check Set.sUnion_mono -/-! #### Anti-monotonicity +/-! ### Anti-monotonicity For any sets `A`, `B`, and `C`, ``` @@ -261,7 +261,7 @@ theorem anti_monotonicity_ii (A B : Set (Set α)) (h : A ⊆ B) #check Set.sInter_subset_sInter -/-- #### Intersection/Difference Associativity +/-- ### Intersection/Difference Associativity Let `A`, `B`, and `C` be sets. Then `A ∩ (B - C) = (A ∩ B) - C`. -/ @@ -278,7 +278,7 @@ theorem inter_diff_assoc (A B C : Set α) #check Set.inter_diff_assoc -/-- #### Exercise 2.1 +/-- ### Exercise 2.1 Assume that `A` is the set of integers divisible by `4`. Similarly assume that `B` and `C` are the sets of integers divisible by `9` and `10`, respectively. @@ -300,7 +300,7 @@ theorem exercise_2_1 {A B C : Set ℤ} · rw [hC] at hc exact Set.mem_setOf.mp hc -/-- #### Exercise 2.2 +/-- ### Exercise 2.2 Give an example of sets `A` and `B` for which `⋃ A = ⋃ B` but `A ≠ B`. -/ @@ -339,7 +339,7 @@ theorem exercise_2_2 {A B : Set (Set ℕ)} have h₂ := h₁ 2 simp at h₂ -/-- #### Exercise 2.3 +/-- ### Exercise 2.3 Show that every member of a set `A` is a subset of `U A`. (This was stated as an example in this section.) @@ -352,7 +352,7 @@ theorem exercise_2_3 {A : Set (Set α)} rw [Set.mem_setOf_eq] exact ⟨x, ⟨hx, hy⟩⟩ -/-- #### Exercise 2.4 +/-- ### Exercise 2.4 Show that if `A ⊆ B`, then `⋃ A ⊆ ⋃ B`. -/ @@ -364,7 +364,7 @@ theorem exercise_2_4 {A B : Set (Set α)} (h : A ⊆ B) : ⋃₀ A ⊆ ⋃₀ B rw [Set.mem_setOf_eq] exact ⟨t, ⟨h ht, hxt⟩⟩ -/-- #### Exercise 2.5 +/-- ### Exercise 2.5 Assume that every member of `𝓐` is a subset of `B`. Show that `⋃ 𝓐 ⊆ B`. -/ @@ -376,7 +376,7 @@ theorem exercise_2_5 {𝓐 : Set (Set α)} (h : ∀ x ∈ 𝓐, x ⊆ B) have ⟨t, ⟨ht𝓐, hyt⟩⟩ := hy exact (h t ht𝓐) hyt -/-- #### Exercise 2.6a +/-- ### Exercise 2.6a Show that for any set `A`, `⋃ 𝓟 A = A`. -/ @@ -393,7 +393,7 @@ theorem exercise_2_6a : ⋃₀ (𝒫 A) = A := by rw [Set.mem_setOf_eq] exact ⟨A, ⟨by rw [Set.mem_setOf_eq], hx⟩⟩ -/-- #### Exercise 2.6b +/-- ### Exercise 2.6b Show that `A ⊆ 𝓟 ⋃ A`. Under what conditions does equality hold? -/ @@ -412,7 +412,7 @@ theorem exercise_2_6b conv => rhs; rw [hB, exercise_2_6a] exact hB -/-- #### Exercise 2.7a +/-- ### Exercise 2.7a Show that for any sets `A` and `B`, `𝓟 A ∩ 𝓟 B = 𝓟 (A ∩ B)`. -/ @@ -430,7 +430,7 @@ theorem exercise_2_7A intro x hA _ exact hA -/-- #### Exercise 2.7b (i) +/-- ### Exercise 2.7b (i) Show that `𝓟 A ∪ 𝓟 B ⊆ 𝓟 (A ∪ B)`. -/ @@ -447,7 +447,7 @@ theorem exercise_2_7b_i rw [Set.mem_setOf_eq] exact Set.subset_union_of_subset_right hB A -/-- #### Exercise 2.7b (ii) +/-- ### Exercise 2.7b (ii) Under what conditions does `𝓟 A ∪ 𝓟 B = 𝓟 (A ∪ B)`.? -/ @@ -499,7 +499,7 @@ theorem exercise_2_7b_ii refine Or.inl (Set.Subset.trans hx ?_) exact subset_of_eq (Set.right_subset_union_eq_self hB) -/-- #### Exercise 2.9 +/-- ### Exercise 2.9 Give an example of sets `a` and `B` for which `a ∈ B` but `𝓟 a ∉ 𝓟 B`. -/ @@ -527,7 +527,7 @@ theorem exercise_2_9 (ha : a = {1}) (hB : B = {{1}}) have := h 1 simp at this -/-- #### Exercise 2.10 +/-- ### Exercise 2.10 Show that if `a ∈ B`, then `𝓟 a ∈ 𝓟 𝓟 ⋃ B`. -/ @@ -540,7 +540,7 @@ theorem exercise_2_10 {B : Set (Set α)} (ha : a ∈ B) rw [← hb, Set.mem_setOf_eq] exact h₂ -/-- #### Exercise 2.11 (i) +/-- ### Exercise 2.11 (i) Show that for any sets `A` and `B`, `A = (A ∩ B) ∪ (A - B)`. -/ @@ -557,7 +557,7 @@ theorem exercise_2_11_i {A B : Set α} · intro hx exact ⟨hx, em (B x)⟩ -/-- #### Exercise 2.11 (ii) +/-- ### Exercise 2.11 (ii) Show that for any sets `A` and `B`, `A ∪ (B - A) = A ∪ B`. -/ @@ -651,7 +651,7 @@ lemma left_diff_eq_singleton_one : (A \ B) \ C = {1} := by | inl y => rw [hx] at y; simp at y | inr y => rw [hx] at y; simp at y -/-- #### Exercise 2.14 +/-- ### Exercise 2.14 Show by example that for some sets `A`, `B`, and `C`, the set `A - (B - C)` is different from `(A - B) - C`. @@ -668,7 +668,7 @@ theorem exercise_2_14 : A \ (B \ C) ≠ (A \ B) \ C := by end -/-- #### Exercise 2.15 (a) +/-- ### Exercise 2.15 (a) Show that `A ∩ (B + C) = (A ∩ B) + (A ∩ C)`. -/ @@ -696,7 +696,7 @@ theorem exercise_2_15a (A B C : Set α) #check Set.inter_symmDiff_distrib_left -/-- #### Exercise 2.15 (b) +/-- ### Exercise 2.15 (b) Show that `A + (B + C) = (A + B) + C`. -/ @@ -749,7 +749,7 @@ theorem exercise_2_15b (A B C : Set α) #check symmDiff_assoc -/-- #### Exercise 2.16 +/-- ### Exercise 2.16 Simplify: `[(A ∪ B ∪ C) ∩ (A ∪ B)] - [(A ∪ (B - C)) ∩ A]` @@ -761,7 +761,7 @@ theorem exercise_2_16 {A B C : Set α} _ = (A ∪ B) \ A := by rw [Set.union_inter_cancel_left] _ = B \ A := by rw [Set.union_diff_left] -/-! #### Exercise 2.17 +/-! ### Exercise 2.17 Show that the following four conditions are equivalent. @@ -797,7 +797,7 @@ theorem exercise_2_17_iii {A B : Set α} (h : A ∪ B = B) theorem exercise_2_17_iv {A B : Set α} (h : A ∩ B = A) : A ⊆ B := Set.inter_eq_left.mp h -/-- #### Exercise 2.19 +/-- ### Exercise 2.19 Is `𝒫 (A - B)` always equal to `𝒫 A - 𝒫 B`? Is it ever equal to `𝒫 A - 𝒫 B`? -/ @@ -810,7 +810,7 @@ theorem exercise_2_19 {A B : Set α} have := h ∅ exact absurd (this.mp he) ne -/-- #### Exercise 2.20 +/-- ### Exercise 2.20 Let `A`, `B`, and `C` be sets such that `A ∪ B = A ∪ C` and `A ∩ B = A ∩ C`. Show that `B = C`. @@ -836,7 +836,7 @@ theorem exercise_2_20 {A B C : Set α} rw [← hu] at this exact Or.elim this (absurd · hA) (by simp) -/-- #### Exercise 2.21 +/-- ### Exercise 2.21 Show that `⋃ (A ∪ B) = (⋃ A) ∪ (⋃ B)`. -/ @@ -860,7 +860,7 @@ theorem exercise_2_21 {A B : Set (Set α)} have ⟨t, ht⟩ : ∃ t, t ∈ B ∧ x ∈ t := hB exact ⟨t, ⟨Set.mem_union_right A ht.left, ht.right⟩⟩ -/-- #### Exercise 2.22 +/-- ### Exercise 2.22 Show that if `A` and `B` are nonempty sets, then `⋂ (A ∪ B) = ⋂ A ∩ ⋂ B`. -/ @@ -889,7 +889,7 @@ theorem exercise_2_22 {A B : Set (Set α)} · intro hB exact (this t).right hB -/-- #### Exercise 2.24a +/-- ### Exercise 2.24a Show that is `𝓐` is nonempty, then `𝒫 (⋂ 𝓐) = ⋂ { 𝒫 X | X ∈ 𝓐 }`. -/ @@ -908,7 +908,7 @@ theorem exercise_2_24a {𝓐 : Set (Set α)} _ = { x | ∀ t ∈ { 𝒫 X | X ∈ 𝓐 }, x ∈ t} := by simp _ = ⋂₀ { 𝒫 X | X ∈ 𝓐 } := rfl -/-- #### Exercise 2.24b +/-- ### Exercise 2.24b Show that ``` @@ -950,7 +950,7 @@ theorem exercise_2_24b {𝓐 : Set (Set α)} simp only [Set.mem_setOf_eq, exists_exists_and_eq_and, Set.mem_powerset_iff] exact ⟨⋃₀ 𝓐, ⟨hA, hx⟩⟩ -/-- #### Exercise 2.25 +/-- ### Exercise 2.25 Is `A ∪ (⋃ 𝓑)` always the same as `⋃ { A ∪ X | X ∈ 𝓑 }`? If not, then under what conditions does equality hold? diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index c9916c1..47605f5 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -17,7 +17,7 @@ namespace Enderton.Set.Chapter_3 open Set.Relation -/-- #### Lemma 3B +/-- ### Lemma 3B If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`. -/ @@ -35,7 +35,7 @@ lemma lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C) -/ exact Set.mem_mem_imp_pair_subset hxs hxys -/-- #### Theorem 3D +/-- ### Theorem 3D If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`. -/ @@ -61,7 +61,7 @@ theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A) exact ⟨this (by simp), this (by simp)⟩ -/-- #### Theorem 3G (i) +/-- ### Theorem 3G (i) Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`. -/ @@ -75,7 +75,7 @@ theorem theorem_3g_i {F : Set.HRelation α β} unfold isOneToOne at hF exact (single_valued_eq_unique hF.left hy hy₁).symm -/-- #### Theorem 3G (ii) +/-- ### Theorem 3G (ii) Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`. -/ @@ -89,7 +89,7 @@ theorem theorem_3g_ii {F : Set.HRelation α β} unfold isOneToOne at hF exact (single_rooted_eq_unique hF.right hx hx₁).symm -/-- #### Theorem 3H +/-- ### Theorem 3H Assume that `F` and `G` are functions. Then ``` @@ -128,7 +128,7 @@ theorem theorem_3h_dom {F : Set.HRelation β γ} {G : Set.HRelation α β} simp only [Set.mem_setOf_eq] exact ⟨a, ha.left.left, hb⟩ -/-- #### Theorem 3J (a) +/-- ### Theorem 3J (a) Assume that `F : A → B`, and that `A` is nonempty. There exists a function `G : B → A` (a "left inverse") such that `G ∘ F` is the identity function on `A` @@ -281,7 +281,7 @@ theorem theorem_3j_a {F : Set.HRelation α β} rw [← single_valued_eq_unique hF.is_func hx₂.right ht₂.left] at ht₂ exact single_valued_eq_unique hG₁.is_func ht₂.right ht₁.right -/-- #### Theorem 3J (b) +/-- ### Theorem 3J (b) Assume that `F : A → B`, and that `A` is nonempty. There exists a function `H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on @@ -300,7 +300,7 @@ theorem theorem_3j_b {F : Set.HRelation α β} (hF : mapsInto F A B) simp only [Set.mem_setOf_eq, Prod.exists, exists_eq_right, Set.setOf_mem_eq] exact hy -/-- #### Theorem 3K (a) +/-- ### Theorem 3K (a) The following hold for any sets. (`F` need not be a function.) The image of a union is the union of the images: @@ -335,7 +335,7 @@ theorem theorem_3k_a {F : Set.HRelation α β} {𝓐 : Set (Set α)} simp only [Set.mem_sUnion, Set.mem_setOf_eq] exact ⟨u, ⟨A, hA.left, hu.left⟩, hu.right⟩ -/-! #### Theorem 3K (b) +/-! ### Theorem 3K (b) The following hold for any sets. (`F` need not be a function.) The image of an intersection is included in the intersection of the images: @@ -395,7 +395,7 @@ theorem theorem_3k_b_ii {F : Set.HRelation α β} {𝓐 : Set (Set α)} simp only [Set.mem_sInter, Set.mem_setOf_eq] exact ⟨u, hu⟩ -/-! #### Theorem 3K (c) +/-! ### Theorem 3K (c) The following hold for any sets. (`F` need not be a function.) The image of a difference includes the difference of the images: @@ -449,7 +449,7 @@ theorem theorem_3k_c_ii {F : Set.HRelation α β} {A B : Set α} exact absurd hu₁.left hu.left.right exact ⟨hv₁, hv₂⟩ -/-! #### Corollary 3L +/-! ### Corollary 3L For any function `G` and sets `A`, `B`, and `𝓐`: @@ -477,7 +477,7 @@ theorem corollary_3l_iii {G : Set.HRelation β α} {A B : Set α} single_valued_self_iff_single_rooted_inv.mp hG exact (theorem_3k_c_ii hG').symm -/-- #### Theorem 3M +/-- ### Theorem 3M If `R` is a symmetric and transitive relation, then `R` is an equivalence relation on `fld R`. @@ -497,7 +497,7 @@ theorem theorem_3m {R : Set.Relation α} have := hS ht exact hT this ht -/-- #### Theorem 3R +/-- ### Theorem 3R Let `R` be a linear ordering on `A`. @@ -521,7 +521,7 @@ theorem theorem_3r {R : Rel α α} (hR : IsStrictTotalOrder α R) right exact h₂ -/-- #### Exercise 3.1 +/-- ### Exercise 3.1 Suppose that we attempted to generalize the Kuratowski definitions of ordered pairs to ordered triples by defining @@ -544,7 +544,7 @@ theorem exercise_3_1 {x y z u v w : ℕ} · rw [hy, hv] simp only -/-- #### Exercise 3.2a +/-- ### Exercise 3.2a Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`. -/ @@ -560,7 +560,7 @@ theorem exercise_3_2a {A : Set α} {B C : Set β} _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl _ = (Set.prod A B) ∪ (Set.prod A C) := rfl -/-- #### Exercise 3.2b +/-- ### Exercise 3.2b Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`. -/ @@ -589,7 +589,7 @@ theorem exercise_3_2b {A : Set α} {B C : Set β} have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC) exact (h (a, c)).mpr ⟨ha, hc⟩ -/-- #### Exercise 3.3 +/-- ### Exercise 3.3 Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`. -/ @@ -617,7 +617,7 @@ theorem exercise_3_3 {A : Set (Set α)} {𝓑 : Set (Set β)} · intro ⟨b, h₁, h₂, h₃⟩ exact ⟨b, h₁, h₂, h₃⟩ -/-- #### Exercise 3.5a +/-- ### Exercise 3.5a Assume that `A` and `B` are given sets, and show that there exists a set `C` such that for any `y`, @@ -685,7 +685,7 @@ theorem exercise_3_5a {A : Set α} {B : Set β} rw [hab.right] exact ⟨hab.left, hb⟩ -/-- #### Exercise 3.5b +/-- ### Exercise 3.5b With `A`, `B`, and `C` as above, show that `A × B = ∪ C`. -/ @@ -718,7 +718,7 @@ theorem exercise_3_5b {A : Set α} (B : Set β) exact ⟨h, hb⟩ -/-- #### Exercise 3.6 +/-- ### Exercise 3.6 Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`. -/ @@ -736,7 +736,7 @@ theorem exercise_3_6 {A : Set.HRelation α β} ] exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩ -/-- #### Exercise 3.7 +/-- ### Exercise 3.7 Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`. -/ @@ -815,7 +815,7 @@ theorem exercise_3_7 {R : Set.Relation α} simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this exact hxy_mem this -/-- #### Exercise 3.8 (i) +/-- ### Exercise 3.8 (i) Show that for any set `𝓐`: ``` @@ -841,7 +841,7 @@ theorem exercise_3_8_i {A : Set (Set.HRelation α β)} · intro ⟨t, ht, y, hx⟩ exact ⟨y, t, ht, hx⟩ -/-- #### Exercise 3.8 (ii) +/-- ### Exercise 3.8 (ii) Show that for any set `𝓐`: ``` @@ -866,7 +866,7 @@ theorem exercise_3_8_ii {A : Set (Set.HRelation α β)} · intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩ exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩ -/-- #### Exercise 3.9 (i) +/-- ### Exercise 3.9 (i) Discuss the result of replacing the union operation by the intersection operation in the preceding problem. @@ -892,7 +892,7 @@ theorem exercise_3_9_i {A : Set (Set.HRelation α β)} intro _ y hy R hR exact ⟨y, hy R hR⟩ -/-- #### Exercise 3.9 (ii) +/-- ### Exercise 3.9 (ii) Discuss the result of replacing the union operation by the intersection operation in the preceding problem. @@ -918,7 +918,7 @@ theorem exercise_3_9_ii {A : Set (Set.HRelation α β)} intro _ y hy R hR exact ⟨y, hy R hR⟩ -/-- #### Exercise 3.12 +/-- ### Exercise 3.12 Assume that `f` and `g` are functions and show that ``` @@ -948,7 +948,7 @@ theorem exercise_3_12 {f g : Set.HRelation α β} rw [single_valued_eq_unique hf hp hy₁.left.left] exact hy₁.left.right -/-- #### Exercise 3.13 +/-- ### Exercise 3.13 Assume that `f` and `g` are functions with `f ⊆ g` and `dom g ⊆ dom f`. Show that `f = g`. @@ -972,7 +972,7 @@ theorem exercise_3_13 {f g : Set.HRelation α β} rw [single_valued_eq_unique hg hp hx.left.right] exact hx.left.left -/-- #### Exercise 3.14 (a) +/-- ### Exercise 3.14 (a) Assume that `f` and `g` are functions. Show that `f ∩ g` is a function. -/ @@ -981,7 +981,7 @@ theorem exercise_3_14_a {f g : Set.HRelation α β} : isSingleValued (f ∩ g) := single_valued_subset hf (Set.inter_subset_left f g) -/-- #### Exercise 3.14 (b) +/-- ### Exercise 3.14 (b) Assume that `f` and `g` are functions. Show that `f ∪ g` is a function **iff** `f(x) = g(x)` for every `x` in `(dom f) ∩ (dom g)`. @@ -1061,7 +1061,7 @@ theorem exercise_3_14_b {f g : Set.HRelation α β} · intro hz exact absurd (mem_pair_imp_fst_mem_dom hz) hgx -/-- #### Exercise 3.15 +/-- ### Exercise 3.15 Let `𝓐` be a set of functions such that for any `f` and `g` in `𝓐`, either `f ⊆ g` or `g ⊆ f`. Show that `⋃ 𝓐` is a function. @@ -1084,7 +1084,7 @@ theorem exercise_3_15 {𝓐 : Set (Set.HRelation α β)} have := hg' hg.right exact single_valued_eq_unique (h𝓐 f hf.left) this hf.right -/-! #### Exercise 3.17 +/-! ### Exercise 3.17 Show that the composition of two single-rooted sets is again single-rooted. Conclude that the composition of two one-to-one functions is again one-to-one. @@ -1119,7 +1119,7 @@ theorem exercise_3_17_ii {F : Set.HRelation β γ} {G : Set.HRelation α β} (single_valued_comp_is_single_valued hF.left hG.left) (exercise_3_17_i hF.right hG.right) -/-! #### Exercise 3.18 +/-! ### Exercise 3.18 Let `R` be the set ``` @@ -1252,7 +1252,7 @@ theorem exercise_3_18_v end Exercise_3_18 -/-! #### Exercise 3.19 +/-! ### Exercise 3.19 Let ``` @@ -1502,7 +1502,7 @@ theorem exercise_3_19_x end Exercise_3_19 -/-- #### Exercise 3.20 +/-- ### Exercise 3.20 Show that `F ↾ A = F ∩ (A × ran F)`. -/ @@ -1522,7 +1522,7 @@ theorem exercise_3_20 {F : Set.HRelation α β} {A : Set α} _ = F ∩ {p | p.fst ∈ A ∧ p.snd ∈ ran F} := rfl _ = F ∩ (Set.prod A (ran F)) := rfl -/-- #### Exercise 3.22 (a) +/-- ### Exercise 3.22 (a) Show that the following is correct for any sets. ``` @@ -1537,7 +1537,7 @@ theorem exercise_3_22_a {A B : Set α} {F : Set.HRelation α β} (h : A ⊆ B) have := h hu.left exact ⟨u, this, hu.right⟩ -/-- #### Exercise 3.22 (b) +/-- ### Exercise 3.22 (b) Show that the following is correct for any sets. ``` @@ -1567,7 +1567,7 @@ theorem exercise_3_22_b {A B : Set α} {F : Set.HRelation α β} _ = { v | ∃ a ∈ image G A, (a, v) ∈ F } := rfl _ = image F (image G A) := rfl -/-- #### Exercise 3.22 (c) +/-- ### Exercise 3.22 (c) Show that the following is correct for any sets. ``` @@ -1585,7 +1585,7 @@ theorem exercise_3_22_c {A B : Set α} {Q : Set.Relation α} _ = { p | p ∈ Q ∧ p.1 ∈ A} ∪ { p | p ∈ Q ∧ p.1 ∈ B } := rfl _ = (restriction Q A) ∪ (restriction Q B) := rfl -/-- #### Exercise 3.23 (i) +/-- ### Exercise 3.23 (i) Let `I` be the identity function on the set `A`. Show that for any sets `B` and `C`, `B ∘ I = B ↾ A`. @@ -1609,7 +1609,7 @@ theorem exercise_3_23_i {A : Set α} {B : Set.HRelation α β} {I : Set.Relation intro (x, y) hp refine ⟨x, ⟨hp.right, rfl⟩, hp.left⟩ -/-- #### Exercise 3.23 (ii) +/-- ### Exercise 3.23 (ii) Let `I` be the identity function on the set `A`. Show that for any sets `B` and `C`, `I⟦C⟧ = A ∩ C`. @@ -1641,7 +1641,7 @@ theorem exercise_3_23_ii {A C : Set α} {I : Set.Relation α} _ = C ∩ A := rfl _ = A ∩ C := Set.inter_comm C A -/-- #### Exercise 3.24 +/-- ### Exercise 3.24 Show that for a function `F`, `F⁻¹⟦A⟧ = { x ∈ dom F | F(x) ∈ A }`. -/ @@ -1671,7 +1671,7 @@ theorem exercise_3_24 {F : Set.HRelation α β} {A : Set β} · intro ⟨y, hy⟩ exact ⟨y, hy.left⟩ -/-- #### Exercise 3.25 (b) +/-- ### Exercise 3.25 (b) Show that the result of part (a) holds for any function `G`, not necessarily one-to-one. @@ -1694,7 +1694,7 @@ theorem exercise_3_25_b {G : Set.HRelation α β} (hG : isSingleValued G) have ⟨t, ht⟩ := ran_exists h.left exact ⟨t, ⟨t, x, ht, rfl, rfl⟩, by rwa [← h.right]⟩ -/-- #### Exercise 3.25 (a) +/-- ### Exercise 3.25 (a) Assume that `G` is a one-to-one function. Show that `G ∘ G⁻¹` is the identity function on `ran G`. @@ -1703,7 +1703,7 @@ theorem exercise_3_25_a {G : Set.HRelation α β} (hG : isOneToOne G) : comp G (inv G) = { p | p.1 ∈ ran G ∧ p.1 = p.2 } := exercise_3_25_b hG.left -/-- #### Exercise 3.27 +/-- ### Exercise 3.27 Show that `dom (F ∘ G) = G⁻¹⟦dom F⟧` for any sets `F` and `G`. (`F` and `G` need not be functions.) @@ -1737,7 +1737,7 @@ theorem exercise_3_27 {F : Set.HRelation β γ} {G : Set.HRelation α β} ] exact ⟨t, u, hu.right, ht⟩ -/-- #### Exercise 3.28 +/-- ### Exercise 3.28 Assume that `f` is a one-to-one function from `A` into `B`, and that `G` is the function with `dom G = 𝒫 A` defined by the equation `G(X) = f⟦X⟧`. Show that `G` @@ -1832,7 +1832,7 @@ theorem exercise_3_28 {A : Set α} {B : Set β} have hz := mem_pair_imp_snd_mem_ran hb.right exact hf.right.ran_ss hz -/-- #### Exercise 3.29 +/-- ### Exercise 3.29 Assume that `f : A → B` and define a function `G : B → 𝒫 A` by ``` @@ -1875,7 +1875,7 @@ theorem exercise_3_29 {f : Set.HRelation α β} {G : Set.HRelation β (Set α)} rw [heq] at this exact single_valued_eq_unique hf.is_func this.right ht -/-! #### Exercise 3.30 +/-! ### Exercise 3.30 Assume that `F : 𝒫 A → 𝒫 A` and that `F` has the monotonicity property: ``` @@ -1892,7 +1892,7 @@ variable {F : Set α → Set α} {A B C : Set α} (hB : B = ⋂₀ { X | X ⊆ A ∧ F X ⊆ X }) (hC : C = ⋃₀ { X | X ⊆ A ∧ X ⊆ F X }) -/-- ##### Exercise 3.30 (a) +/-- #### Exercise 3.30 (a) Show that `F(B) = B` and `F(C) = C`. -/ @@ -1988,7 +1988,7 @@ theorem exercise_3_30_a : F B = B ∧ F C = C := by · rw [Set.Subset.antisymm_iff] exact ⟨hC_subset, hC_supset⟩ -/-- ##### Exercise 3.30 (b) +/-- #### Exercise 3.30 (b) Show that if `F(X) = X`, then `B ⊆ X ⊆ C`. -/ @@ -2010,7 +2010,7 @@ theorem exercise_3_30_b : ∀ X, X ⊆ A ∧ F X = X → B ⊆ X ∧ X ⊆ C := end Exercise_3_30 -/-- #### Exercise 3.32 (a) +/-- ### Exercise 3.32 (a) Show that `R` is symmetric **iff** `R⁻¹ ⊆ R`. -/ @@ -2028,7 +2028,7 @@ theorem exercise_3_32_a {R : Set.Relation α} rw [← mem_self_comm_mem_inv] at hp exact hR hp -/-- #### Exercise 3.32 (b) +/-- ### Exercise 3.32 (b) Show that `R` is transitive **iff** `R ∘ R ⊆ R`. -/ @@ -2045,7 +2045,7 @@ theorem exercise_3_32_b {R : Set.Relation α} have : (x, z) ∈ comp R R := ⟨y, hx, hz⟩ exact hR this -/-- #### Exercise 3.33 +/-- ### Exercise 3.33 Show that `R` is a symmetric and transitive relation **iff** `R = R⁻¹ ∘ R`. -/ @@ -2095,7 +2095,7 @@ theorem exercise_3_33 {R : Set.Relation α} rw [h, hR] exact ⟨y, hx, this⟩ -/-- #### Exercise 3.34 (a) +/-- ### Exercise 3.34 (a) Assume that `𝓐` is a nonempty set, every member of which is a transitive relation. Is the set `⋂ 𝓐` a transitive relation? @@ -2110,7 +2110,7 @@ theorem exercise_3_34_a {𝓐 : Set (Set.Relation α)} have hy' := hy A hA exact h𝓐 A hA hx' hy' -/-- #### Exercise 3.34 (b) +/-- ### Exercise 3.34 (b) Assume that `𝓐` is a nonempty set, every member of which is a transitive relation. Is `⋃ 𝓐` a transitive relation? @@ -2157,7 +2157,7 @@ theorem exercise_3_34_b {𝓐 : Set (Set.Relation ℕ)} simp at this exact absurd (h h₁ h₂) h₃ -/-- #### Exercise 3.35 +/-- ### Exercise 3.35 Show that for any `R` and `x`, we have `[x]_R = R⟦{x}⟧`. -/ @@ -2168,7 +2168,7 @@ theorem exercise_3_35 {R : Set.Relation α} {x : α} _ = { t | ∃ u ∈ ({x} : Set α), (u, t) ∈ R } := by simp _ = image R {x} := rfl -/-- #### Exercise 3.36 +/-- ### Exercise 3.36 Assume that `f : A → B` and that `R` is an equivalence relation on `B`. Define `Q` to be the set `{⟨x, y⟩ ∈ A × A | ⟨f(x), f(y)⟩ ∈ R}`. Show that `Q` is an @@ -2234,7 +2234,7 @@ theorem exercise_3_36 {f : Set.HRelation α β} simp only [exists_and_left, Set.mem_setOf_eq] exact ⟨fx, hfx, fz, hfz, hR.trans h₁ h₂⟩ -/-- #### Exercise 3.37 +/-- ### Exercise 3.37 Assume that `P` is a partition of a set `A`. Define the relation `Rₚ` as follows: @@ -2311,7 +2311,7 @@ theorem exercise_3_37 {P : Set (Set α)} {A : Set α} simp only [Set.mem_setOf_eq] exact ⟨B₁, hB₁.left, hB₁.right.left, by rw [hB]; exact hB₂.right.right⟩ -/-- #### Exercise 3.38 +/-- ### Exercise 3.38 Theorem 3P shows that `A / R` is a partition of `A` whenever `R` is an equivalence relation on `A`. Show that if we start with the equivalence relation @@ -2379,7 +2379,7 @@ theorem exercise_3_38 {P : Set (Set α)} {A : Set α} simp only [Set.mem_setOf_eq] _ = neighborhood Rₚ x := rfl -/-- #### Exercise 3.39 +/-- ### Exercise 3.39 Assume that we start with an equivalence relation `R` on `A` and define `P` to be the partition `A / R`. Show that `Rₚ`, as defined in Exercise 37, is just @@ -2417,7 +2417,7 @@ theorem exercise_3_39 {P : Set (Set α)} {R Rₚ : Set.Relation α} {A : Set α} rw [hP] exact ⟨x, hxA, rfl⟩ -/-- #### Exercise 3.41 (a) +/-- ### Exercise 3.41 (a) Let `ℝ` be the set of real numbers and define the realtion `Q` on `ℝ × ℝ` by `⟨u, v⟩ Q ⟨x, y⟩` **iff** `u + y = x + v`. Show that `Q` is an equivalence @@ -2470,7 +2470,7 @@ theorem exercise_3_41_a {Q : Set.Relation (ℝ × ℝ)} conv => right; rw [add_comm] exact this -/-- #### Exercise 3.43 +/-- ### Exercise 3.43 Assume that `R` is a linear ordering on a set `A`. Show that `R⁻¹` is also a linear ordering on `A`. @@ -2493,7 +2493,7 @@ theorem exercise_3_43 {R : Rel α α} (hR : IsStrictTotalOrder α R) unfold Rel.inv flip at * exact hR.trans c b a hac hab -/-! #### Exercise 3.44 +/-! ### Exercise 3.44 Assume that `<` is a linear ordering on a set `A`. Assume that `f : A → A` and that `f` has the property that whenever `x < y`, then `f(x) < f(y)`. Show that @@ -2537,7 +2537,7 @@ theorem exercise_3_44_ii {R : Rel α α} (hR : IsStrictTotalOrder α R) have := hR.trans (f x) (f y) (f x) h (hf y x h₂) exact absurd this (hR.irrefl (f x)) -/-- #### Exercise 3.45 +/-- ### Exercise 3.45 Assume that `<_A` and `<_B` are linear orderings on `A` and `B`, respectively. Define the binary relation `<_L` on the Cartesian product `A × B` by: diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean index 4ea7bfb..6728d6e 100644 --- a/Bookshelf/Enderton/Set/Chapter_4.lean +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -11,7 +11,7 @@ Natural Numbers namespace Enderton.Set.Chapter_4 -/-- #### Theorem 4C +/-- ### Theorem 4C Every natural number except `0` is the successor of some natural number. -/ @@ -23,7 +23,7 @@ theorem theorem_4c (n : ℕ) #check Nat.exists_eq_succ_of_ne_zero -/-- #### Theorem 4I +/-- ### Theorem 4I For natural numbers `m` and `n`, ``` @@ -34,7 +34,7 @@ m + n⁺ = (m + n)⁺ theorem theorem_4i (m n : ℕ) : m + 0 = m ∧ m + n.succ = (m + n).succ := ⟨rfl, rfl⟩ -/-- #### Theorem 4J +/-- ### Theorem 4J For natural numbers `m` and `n`, ``` @@ -45,7 +45,7 @@ m ⬝ n⁺ = m ⬝ n + m . theorem theorem_4j (m n : ℕ) : m * 0 = 0 ∧ m * n.succ = m * n + m := ⟨rfl, rfl⟩ -/-- #### Left Additive Identity +/-- ### Left Additive Identity For all `n ∈ ω`, `A₀(n) = n`. In other words, `0 + n = n`. -/ @@ -60,7 +60,7 @@ lemma left_additive_identity (n : ℕ) #check Nat.zero_add -/-- #### Lemma 2 +/-- ### Lemma 2 For all `m, n ∈ ω`, `Aₘ₊(n) = Aₘ(n⁺)`. In other words, `m⁺ + n = m + n⁺`. -/ @@ -76,7 +76,7 @@ lemma lemma_2 (m n : ℕ) #check Nat.succ_add_eq_succ_add -/-- #### Theorem 4K-1 +/-- ### Theorem 4K-1 Associatve law for addition. For `m, n, p ∈ ω`, ``` @@ -99,7 +99,7 @@ theorem theorem_4k_1 {m n p : ℕ} #check Nat.add_assoc -/-- #### Theorem 4K-2 +/-- ### Theorem 4K-2 Commutative law for addition. For `m, n ∈ ω`, ``` @@ -119,7 +119,7 @@ theorem theorem_4k_2 {m n : ℕ} #check Nat.add_comm -/-- #### Zero Multiplicand +/-- ### Zero Multiplicand For all `n ∈ ω`, `M₀(n) = 0`. In other words, `0 ⬝ n = 0`. -/ @@ -135,7 +135,7 @@ theorem zero_multiplicand (n : ℕ) #check Nat.zero_mul -/-- #### Successor Distribution +/-- ### Successor Distribution For all `m, n ∈ ω`, `Mₘ₊(n) = Mₘ(n) + n`. In other words, ``` @@ -159,7 +159,7 @@ theorem succ_distrib (m n : ℕ) #check Nat.succ_mul -/-- #### Theorem 4K-3 +/-- ### Theorem 4K-3 Distributive law. For `m, n, p ∈ ω`, ``` @@ -181,7 +181,7 @@ theorem theorem_4k_3 (m n p : ℕ) _ = (m * n + n) + (m * p + p) := by rw [theorem_4k_1, theorem_4k_1] _ = m.succ * n + m.succ * p := by rw [succ_distrib, succ_distrib] -/-- #### Successor Identity +/-- ### Successor Identity For all `m ∈ ω`, `Aₘ(1) = m⁺`. In other words, `m + 1 = m⁺`. -/ @@ -197,7 +197,7 @@ theorem succ_identity (m : ℕ) #check Nat.succ_eq_one_add -/-- #### Right Multiplicative Identity +/-- ### Right Multiplicative Identity For all `m ∈ ω`, `Mₘ(1) = m`. In other words, `m ⬝ 1 = m`. -/ @@ -213,9 +213,9 @@ theorem right_mul_id (m : ℕ) #check Nat.mul_one -/-- #### Theorem 4K-5 +/-- ### Theorem 4K-5 -Commutative law for multiplication. For `m, n ∈ ω`, `m ⬝ n = n ⬝ m`. +Commutative law for multiplication. For `m, n ∈ ω`, `m ⬝ n = n ⬝ m`. -/ theorem theorem_4k_5 (m n : ℕ) : m * n = n * m := by @@ -232,7 +232,7 @@ theorem theorem_4k_5 (m n : ℕ) #check Nat.mul_comm -/-- #### Theorem 4K-4 +/-- ### Theorem 4K-4 Associative law for multiplication. For `m, n, p ∈ ω`, ``` @@ -254,7 +254,7 @@ theorem theorem_4k_4 (m n p : ℕ) #check Nat.mul_assoc -/-- #### Lemma 4L(b) +/-- ### Lemma 4L(b) No natural number is a member of itself. -/ @@ -269,7 +269,7 @@ lemma lemma_4l_b (n : ℕ) #check Nat.lt_irrefl -/-- #### Lemma 10 +/-- ### Lemma 10 For every natural number `n ≠ 0`, `0 ∈ n`. -/ @@ -285,7 +285,7 @@ theorem zero_least_nat (n : ℕ) #check Nat.pos_of_ne_zero -/-! #### Theorem 4N +/-! ### Theorem 4N For any natural numbers `n`, `m`, and `p`, ``` @@ -361,7 +361,7 @@ theorem theorem_4n_ii (m n p : ℕ) #check Nat.mul_lt_mul_of_pos_right -/-! #### Corollary 4P +/-! ### Corollary 4P The following cancellation laws hold for `m`, `n`, and `p` in `ω`: ``` @@ -384,7 +384,7 @@ theorem corollary_4p_i (m n p : ℕ) (h : m + p = n + p) #check Nat.add_right_cancel -/-- #### Well Ordering of ω +/-- ### Well Ordering of ω Let `A` be a nonempty subset of `ω`. Then there is some `m ∈ A` such that `m ≤ n` for all `n ∈ A`. @@ -401,7 +401,7 @@ theorem well_ordering_nat {A : Set ℕ} (hA : Set.Nonempty A) rw [this] at h simp only [sdiff_self, Set.bot_eq_empty] at h exact absurd h.symm (Set.Nonempty.ne_empty hA) - + -- Use strong induction to prove every element of `ω` is in the complement. have : ∀ n : ℕ, (∀ m, m < n → m ∈ A.compl) := by intro n @@ -438,7 +438,7 @@ theorem well_ordering_nat {A : Set ℕ} (hA : Set.Nonempty A) #check WellOrder -/-- #### Strong Induction Principle for ω +/-- ### Strong Induction Principle for ω Let `A` be a subset of `ω`, and assume that for every `n ∈ ω`, if every number less than `n` is in `A`, then `n ∈ A`. Then `A = ω`. @@ -455,21 +455,21 @@ theorem strong_induction_principle_nat (A : Set ℕ) by_contra nh have ⟨m, hm⟩ := well_ordering_nat (Set.nmem_singleton_empty.mp nh) refine absurd (h m ?_) hm.left - + -- Show that every number less than `m` is in `A`. intro x hx by_contra nx have : x < x := Nat.lt_of_lt_of_le hx (hm.right x nx) simp at this -/-- #### Exercise 4.1 +/-- ### Exercise 4.1 Show that `1 ≠ 3` i.e., that `∅⁺ ≠ ∅⁺⁺⁺`. -/ theorem exercise_4_1 : 1 ≠ 3 := by simp -/-- #### Exercise 4.13 +/-- ### Exercise 4.13 Let `m` and `n` be natural numbers such that `m ⬝ n = 0`. Show that either `m = 0` or `n = 0`. @@ -498,7 +498,7 @@ Call a natural number *odd* if it has the form `(2 ⬝ p) + 1` for some `p`. -/ def odd (n : ℕ) : Prop := ∃ p, (2 * p) + 1 = n -/-- #### Exercise 4.14 +/-- ### Exercise 4.14 Show that each natural number is either even or odd, but never both. -/ @@ -549,7 +549,7 @@ theorem exercise_4_14 (n : ℕ) have : even n := ⟨q, hq'⟩ exact absurd this h -/-- #### Exercise 4.17 +/-- ### Exercise 4.17 Prove that `mⁿ⁺ᵖ = mⁿ ⬝ mᵖ.` -/ @@ -567,7 +567,7 @@ theorem exercise_4_17 (m n p : ℕ) _ = m ^ n * (m ^ p * m) := by rw [theorem_4k_4] _ = m ^ n * m ^ p.succ := rfl -/-- #### Exercise 4.19 +/-- ### Exercise 4.19 Prove that if `m` is a natural number and `d` is a nonzero number, then there exist numbers `q` and `r` such that `m = (d ⬝ q) + r` and `r` is less than `d`. @@ -600,7 +600,7 @@ theorem exercise_4_19 (m d : ℕ) (hd : d ≠ 0) _ < d := hr simp at this -/-- #### Exercise 4.22 +/-- ### Exercise 4.22 Show that for any natural numbers `m` and `p` we have `m ∈ m + p⁺`. -/ @@ -612,7 +612,7 @@ theorem exercise_4_22 (m p : ℕ) _ < m + p.succ := ih _ < m + p.succ.succ := Nat.lt.base (m + p.succ) -/-- #### Exercise 4.23 +/-- ### Exercise 4.23 Assume that `m` and `n` are natural numbers with `m` less than `n`. Show that there is some `p` in `ω` for which `m + p⁺ = n`. (It follows from this and the @@ -637,7 +637,7 @@ theorem exercise_4_23 {m n : ℕ} (hm : m < n) refine ⟨0, ?_⟩ rw [hm₁] -/-- #### Exercise 4.24 +/-- ### Exercise 4.24 Assume that `m + n = p + q`. Show that ``` @@ -660,7 +660,7 @@ theorem exercise_4_24 (m n p q : ℕ) (h : m + n = p + q) rw [← h] at hr exact (theorem_4n_i m p n).mpr hr -/-- #### Exercise 4.25 +/-- ### Exercise 4.25 Assume that `n ∈ m` and `q ∈ p`. Show that ``` @@ -685,4 +685,4 @@ theorem exercise_4_25 (m n p q : ℕ) (h₁ : n < m) (h₂ : q < p) conv at h₁ => right; rw [add_comm] exact h₁ -end Enderton.Set.Chapter_4 \ No newline at end of file +end Enderton.Set.Chapter_4 diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean index 0b3ed3b..fd16a5f 100644 --- a/Bookshelf/Enderton/Set/Chapter_6.lean +++ b/Bookshelf/Enderton/Set/Chapter_6.lean @@ -20,16 +20,29 @@ former provides noncomputable utilities around obtaining inverse functions namespace Enderton.Set.Chapter_6 -/-- #### Theorem 6B +/-- ### Theorem 6B No set is equinumerous to its powerset. -/ theorem theorem_6b (A : Set α) : A ≉ 𝒫 A := by +/- +> Let `A` be an arbitrary set and `f: A → 𝒫 A`. +-/ rw [Set.not_equinumerous_def] intro f hf unfold Set.BijOn at hf +/- +> Define `φ = {a ∈ A | a ∉ f(a)}`. +-/ let φ := { a ∈ A | a ∉ f a } +/- +> Clearly `φ ∈ 𝒫 A`. Furthermore, for all `a ∈ A`, `φ ≠ f(a)` since `a ∈ φ` if +> and only if `a ∉ f(a)`. Thus `f` cannot be onto `𝒫 A`. Since `f` was +> arbitrarily chosen, there exists no one-to-one correspondence between `A` and +> `𝒫 A`. Since `A` was arbitrarily chosen, there is no set equinumerous to its +> powerset. +-/ suffices ∀ a ∈ A, f a ≠ φ by have hφ := hf.right.right (show φ ∈ 𝒫 A by simp) have ⟨a, ha⟩ := hφ @@ -82,23 +95,18 @@ lemma pigeonhole_principle_aux (n : ℕ) -/ induction n with /- -## (i) -> By definition, `0 = ∅`. +> #### (i) +> By definition, `0 = ∅`. Then `0` has no proper subsets. Hence `0 ∈ S` +> vacuously. -/ | zero => intro _ hM unfold Set.Iio at hM simp only [Nat.zero_eq, not_lt_zero', Set.setOf_false] at hM -/- -> Then `0` has no proper subsets. --/ rw [Set.ssubset_empty_iff_false] at hM -/- -> Hence `0 ∈ S` vacuously. --/ exact False.elim hM /- -## (ii) +> #### (ii) > Suppose `n ∈ S` and `M ⊂ n⁺`. Furthermore, let `f: M → n⁺` be a one-to-one > function. -/ @@ -111,19 +119,19 @@ lemma pigeonhole_principle_aux (n : ℕ) · rw [hM', Set.SurjOn_emptyset_Iio_iff_eq_zero] at hf_surj simp at hf_surj /- -> Otherwise `M ≠ 0`. Because `M` is finite, the trichotomy law for `ω` implies +> Otherwise `M ≠ 0`. Because `M` is finite, the *Trichotomy Law for `ω`* implies > the existence of a largest member `p ∈ M`. There are two cases to consider: -/ by_cases h : ¬ ∃ t, t ∈ M ∧ f t = n /- -### Case 1 +> ##### Case 1 > `n ∉ ran f`. > Then `f` is not onto `n⁺`. -/ · have ⟨t, ht⟩ := hf_surj (show n ∈ _ by simp) exact absurd ⟨t, ht⟩ h /- -### Case 2 +> ##### Case 2 > `n ∈ ran f`. > Then there exists some `t ∈ M` such that `⟨t, n⟩ ∈ f`. -/ @@ -159,7 +167,7 @@ lemma pigeonhole_principle_aux (n : ℕ) have hg_maps := Set.Function.swap_MapsTo_self hp₁ ht₁ hf_maps have hg_inj := Set.Function.swap_InjOn_self hp₁ ht₁ hf_inj /- -> Then (1) indicates `g` must not be onto `n`. +> Then *(1)* indicates `g` must not be onto `n`. -/ let M' := M \ {p} have hM' : M' ⊂ Set.Iio n := by @@ -240,9 +248,9 @@ lemma pigeonhole_principle_aux (n : ℕ) simp only [Set.mem_Iio, Set.mem_setOf_eq, not_exists, not_and] exact ng_surj /- -> By the trichotomy law for `ω`, `a ≠ n`. Therefore `a ∉ ran f'`. -> `ran f' = ran f` meaning `a ∉ ran f`. Because `a ∈ n ∈n⁺`, Theorem 4F implies -> `a ∈ n⁺`. Hence `f` is not onto `n⁺`. +> By the *Trichotomy Law for `ω`*, `a ≠ n`. Therefore `a ∉ ran f'`. +> `ran f' = ran f` meaning `a ∉ ran f`. Because `a ∈ n ∈ n⁺`, *Theorem 4F* +> implies `a ∈ n⁺`. Hence `f` is not onto `n⁺`. -/ refine absurd (hf_surj $ calc a _ < n := ha₁ @@ -294,14 +302,14 @@ lemma pigeonhole_principle_aux (n : ℕ) · refine ⟨y, hy₁, ?_⟩ rwa [if_neg hc₁, if_neg hc₂] /- -### Subconclusion +> ##### Subconclusion > The foregoing cases are exhaustive. Hence `n⁺ ∈ S`. - -## (iii) -> By (i) and (ii), `S` is an inductive set. By Theorem 4B, `S = ω`. Thus for all -> natural numbers `n`, there is no one-to-one correspondence between `n` and a -> proper subset of `n`. In other words, no natural number is equinumerous to a -> proper subset of itself. +> +> #### (iii) +> By *(i)* and *(ii)*, `S` is an inductive set. By *Theorem 4B*, `S = ω`. Thus +> for all natural numbers `n`, there is no one-to-one correspondence between `n` +> and a proper subset of `n`. In other words, no natural number is equinumerous +> to a proper subset of itself. -/ /-- @@ -314,34 +322,43 @@ theorem pigeonhole_principle {n : ℕ} have := pigeonhole_principle_aux n M hM f ⟨hf.left, hf.right.left⟩ exact absurd hf.right.right this -/-- #### Corollary 6C +/-- ### Corollary 6C No finite set is equinumerous to a proper subset of itself. -/ theorem corollary_6c [DecidableEq α] [Nonempty α] {S S' : Set α} (hS : Set.Finite S) (h : S' ⊂ S) : S ≉ S' := by +/- +> Let `S` be a finite set and `S'` be a proper subset of `S`. Then there exists +> some set `T`, disjoint from `S'`, such that `S' ∪ T = S`. By definition of a +> finite set, `S` is equinumerous to a natural number `n`. +-/ let T := S \ S' have hT : S = S' ∪ (S \ S') := by simp only [Set.union_diff_self] exact (Set.left_subset_union_eq_self (subset_of_ssubset h)).symm - - -- `hF : S' ∪ T ≈ S`. - -- `hG : S ≈ n`. - -- `hH : S' ∪ T ≈ n`. +/- +> By *Theorem 6A*, `S' ∪ T ≈ S` which, by the same theorem, implies +> `S' ∪ T ≈ n`. +-/ have hF := Set.equinumerous_refl S conv at hF => arg 1; rw [hT] have ⟨n, hG⟩ := Set.finite_iff_equinumerous_nat.mp hS - have ⟨H, hH⟩ := Set.equinumerous_trans hF hG - - -- Restrict `H` to `S'` to yield a bijection between `S'` and a proper subset - -- of `n`. - let R := (Set.Iio n) \ (H '' T) - have hR : Set.BijOn H S' R := by +/- +> Let `f` be a one-to-one correspondence between `S' ∪ T` and `n`. +-/ + have ⟨f, hf⟩ := Set.equinumerous_trans hF hG +/- +> Then `f ↾ S'` is a one-to-one correspondence between `S'` and a proper subset +> of `n`. +-/ + let R := (Set.Iio n) \ (f '' T) + have hR : Set.BijOn f S' R := by refine ⟨?_, ?_, ?_⟩ · -- `Set.MapsTo H S' R` intro x hx - refine ⟨hH.left $ Set.mem_union_left T hx, ?_⟩ + refine ⟨hf.left $ Set.mem_union_left T hx, ?_⟩ unfold Set.image by_contra nx simp only [Finset.mem_coe, Set.mem_setOf_eq] at nx @@ -349,7 +366,7 @@ theorem corollary_6c [DecidableEq α] [Nonempty α] have ⟨a, ha₁, ha₂⟩ := nx have hc₁ : a ∈ S' ∪ T := Set.mem_union_right S' ha₁ have hc₂ : x ∈ S' ∪ T := Set.mem_union_left T hx - rw [hH.right.left hc₁ hc₂ ha₂] at ha₁ + rw [hf.right.left hc₁ hc₂ ha₂] at ha₁ have hx₁ : {x} ⊆ S' := Set.singleton_subset_iff.mpr hx have hx₂ : {x} ⊆ T := Set.singleton_subset_iff.mpr ha₁ @@ -364,14 +381,14 @@ theorem corollary_6c [DecidableEq α] [Nonempty α] intro x₁ hx₁ x₂ hx₂ h have hc₁ : x₁ ∈ S' ∪ T := Set.mem_union_left T hx₁ have hc₂ : x₂ ∈ S' ∪ T := Set.mem_union_left T hx₂ - exact hH.right.left hc₁ hc₂ h + exact hf.right.left hc₁ hc₂ h · -- `Set.SurjOn H S' R` - show ∀ r, r ∈ R → r ∈ H '' S' + show ∀ r, r ∈ R → r ∈ f '' S' intro r hr unfold Set.image simp only [Set.mem_setOf_eq] dsimp only at hr - have := hH.right.right hr.left + have := hf.right.right hr.left simp only [Set.mem_image, Set.mem_union] at this have ⟨x, hx⟩ := this apply Or.elim hx.left @@ -382,9 +399,14 @@ theorem corollary_6c [DecidableEq α] [Nonempty α] rw [← hx.right] simp only [Set.mem_image, Finset.mem_coe] exact ⟨x, hx', rfl⟩ - - intro hf - have hf₁ : S ≈ R := Set.equinumerous_trans hf ⟨H, hR⟩ +/- +> By the *Pigeonhole Principle*, `n` is not equinumerous to any proper subset of +> `n`. Therefore *Theorem 6A* implies `S'` cannot be equinumerous to `n`, which, +> by the same theorem, implies `S'` cannot be equinumerous to `S`. Hence no +> finite set is equinumerous to a proper subset of itself. +-/ + intro hf' + have hf₁ : S ≈ R := Set.equinumerous_trans hf' ⟨f, hR⟩ have hf₂ : R ≈ Set.Iio n := by have ⟨k, hk⟩ := Set.equinumerous_symm hf₁ exact Set.equinumerous_trans ⟨k, hk⟩ hG @@ -398,106 +420,185 @@ theorem corollary_6c [DecidableEq α] [Nonempty α] · show ¬ ∀ r, r ∈ Set.Iio n → r ∈ R intro nr have ⟨t, ht₁⟩ : Set.Nonempty T := Set.diff_ssubset_nonempty h - have ht₂ : H t ∈ Set.Iio n := hH.left (Set.mem_union_right S' ht₁) - have ht₃ : H t ∈ R := nr (H t) ht₂ + have ht₂ : f t ∈ Set.Iio n := hf.left (Set.mem_union_right S' ht₁) + have ht₃ : f t ∈ R := nr (f t) ht₂ exact absurd ⟨t, ht₁, rfl⟩ ht₃.right -/-- #### Corollary 6D (a) +/-- ### Corollary 6D (a) Any set equinumerous to a proper subset of itself is infinite. -/ theorem corollary_6d_a [DecidableEq α] [Nonempty α] {S S' : Set α} (hS : S' ⊂ S) (hf : S ≈ S') : Set.Infinite S := by +/- +> Let `S` be a set equinumerous to proper subset `S'` of itself. Then `S` cannot +> be a finite set by *Corollary 6C*. By definition, `S` is an infinite set. +-/ by_contra nS simp only [Set.not_infinite] at nS exact absurd hf (corollary_6c nS hS) -/-- #### Corollary 6D (b) +/-- ### Corollary 6D (b) The set `ω` is infinite. -/ theorem corollary_6d_b : Set.Infinite (@Set.univ ℕ) := by +/- +> Consider set `S = {n ∈ ω | n is even}`. We prove that (i) `S` is equinumerous +> to `ω` and (ii) that `ω` is infinite. +-/ let S : Set ℕ := { 2 * n | n ∈ @Set.univ ℕ } let f x := 2 * x - suffices Set.BijOn f (@Set.univ ℕ) S by - refine corollary_6d_a ?_ ⟨f, this⟩ - rw [Set.ssubset_def] - apply And.intro - · simp - · show ¬ ∀ x, x ∈ Set.univ → x ∈ S - simp only [ - Set.mem_univ, - true_and, - Set.mem_setOf_eq, - forall_true_left, - not_forall, - not_exists - ] - refine ⟨1, ?_⟩ - intro x nx - simp only [mul_eq_one, false_and] at nx +/- +> #### (i) +> Define `f : ω → S` given by `f(n) = 2 ⬝ n`. Notice `f` is well-defined by the +> definition of an even natural number, introduced in *Exercise 4.14*. We first +> show `f` is one-to-one and then that `f` is onto. +-/ + have : Set.BijOn f (@Set.univ ℕ) S := by + refine ⟨by simp, ?_, ?_⟩ +/- +> Suppose `f(n₁) = f(n₁) = 2 ⬝ n₁`. We must prove that `n₁ = n₂`. +-/ + · -- `Set.InjOn f Set.univ` + intro n₁ _ n₂ _ hf +/- +> By the *Trichotomy Law for `ω`*, exactly one of the following may occur: +> `n₁ = n₂`, `n₁ < n₂`, or `n₂ < n₁`. If `n₁ < n₂`, then *Theorem 4N* implies +> `n₁ ⬝ 2 < n₂ ⬝ 2`. *Theorem 4K-5* then indicates `2 ⬝ n₁ < 2 ⬝ n₂`, a +> contradiction to `2 ⬝ n₁ = 2 ⬝ n₂`. A parallel argument holds for when +> `n₂ < n₁`. Thus `n₁ = n₂`. +-/ + match @trichotomous ℕ LT.lt _ n₁ n₂ with + | Or.inr (Or.inl r) => exact r + | Or.inl r => + have := (Chapter_4.theorem_4n_ii n₁ n₂ 1).mp r + conv at this => left; rw [mul_comm] + conv at this => right; rw [mul_comm] + exact absurd hf (Nat.ne_of_lt this) + | Or.inr (Or.inr r) => + have := (Chapter_4.theorem_4n_ii n₂ n₁ 1).mp r + conv at this => left; rw [mul_comm] + conv at this => right; rw [mul_comm] + exact absurd hf.symm (Nat.ne_of_lt this) +/- +> Next, let `m ∈ S`. That is, `m` is an even number. By definition, there exists +> some `n ∈ ω` such that `m = 2 ⬝ n`. Thus `f(n) = m`. +-/ + · -- `Set.SurjOn f Set.univ S` + show ∀ x, x ∈ S → x ∈ f '' Set.univ + intro x hx + unfold Set.image + simp only [Set.mem_univ, true_and, Set.mem_setOf_eq] at hx ⊢ + exact hx +/- +> By *(i)*, `ω` is equinumerous to a subset of itself. By *Corollary 6D (a)*, +> `ω` is infinite. +-/ + refine corollary_6d_a ?_ ⟨f, this⟩ + rw [Set.ssubset_def] + apply And.intro + · simp + · show ¬ ∀ x, x ∈ Set.univ → x ∈ S + simp only [ + Set.mem_univ, + true_and, + Set.mem_setOf_eq, + forall_true_left, + not_forall, + not_exists + ] + refine ⟨1, ?_⟩ + intro x nx + simp only [mul_eq_one, false_and] at nx - refine ⟨by simp, ?_, ?_⟩ - · -- `Set.InjOn f Set.univ` - intro n₁ _ n₂ _ hf - match @trichotomous ℕ LT.lt _ n₁ n₂ with - | Or.inr (Or.inl r) => exact r - | Or.inl r => - have := (Chapter_4.theorem_4n_ii n₁ n₂ 1).mp r - conv at this => left; rw [mul_comm] - conv at this => right; rw [mul_comm] - exact absurd hf (Nat.ne_of_lt this) - | Or.inr (Or.inr r) => - have := (Chapter_4.theorem_4n_ii n₂ n₁ 1).mp r - conv at this => left; rw [mul_comm] - conv at this => right; rw [mul_comm] - exact absurd hf.symm (Nat.ne_of_lt this) - · -- `Set.SurjOn f Set.univ S` - show ∀ x, x ∈ S → x ∈ f '' Set.univ - intro x hx - unfold Set.image - simp only [Set.mem_univ, true_and, Set.mem_setOf_eq] at hx ⊢ - exact hx - -/-- #### Corollary 6E +/-- ### Corollary 6E Any finite set is equinumerous to a unique natural number. -/ theorem corollary_6e [Nonempty α] (S : Set α) (hS : Set.Finite S) : ∃! n : ℕ, S ≈ Set.Iio n := by +/- +> Let `S` be a finite set. By definition `S` is equinumerous to a natural number +> `n`. +-/ have ⟨n, hf⟩ := Set.finite_iff_equinumerous_nat.mp hS refine ⟨n, hf, ?_⟩ +/- +> Suppose `S` is equinumerous to another natural number `m`. +-/ intro m hg +/- +> By the *Trichotomy Law for `ω`*, exactly one of three situations is possible: +> `n = m`, `n < m`, or `m < n`. +-/ match @trichotomous ℕ LT.lt _ m n with - | Or.inr (Or.inl r) => exact r - | Or.inl r => - have hh := Set.equinumerous_symm hg - have hk := Set.equinumerous_trans hh hf - have hmn : Set.Iio m ⊂ Set.Iio n := Set.Iio_nat_lt_ssubset r - exact absurd hk (pigeonhole_principle hmn) +/- +> If `n < m`, then `m ≈ S` and `S ≈ n`. By *Theorem 6A*, it follows `m ≈ n`. But +> the *Pigeonhole Principle* indicates no natural number is equinumerous to a +> proper subset of itself, a contradiction. +-/ | Or.inr (Or.inr r) => have hh := Set.equinumerous_symm hf have hk := Set.equinumerous_trans hh hg have hnm : Set.Iio n ⊂ Set.Iio m := Set.Iio_nat_lt_ssubset r exact absurd hk (pigeonhole_principle hnm) +/- +> If `m < n`, a parallel argument applies. +-/ + | Or.inl r => + have hh := Set.equinumerous_symm hg + have hk := Set.equinumerous_trans hh hf + have hmn : Set.Iio m ⊂ Set.Iio n := Set.Iio_nat_lt_ssubset r + exact absurd hk (pigeonhole_principle hmn) +/- +> Hence `n = m`, proving every finite set is equinumerous to a unique natural +> number. +-/ + | Or.inr (Or.inl r) => exact r -/-- #### Lemma 6F + +/-- ### Lemma 6F If `C` is a proper subset of a natural number `n`, then `C ≈ m` for some `m` less than `n`. -/ lemma lemma_6f {n : ℕ} : ∀ {C}, C ⊂ Set.Iio n → ∃ m, m < n ∧ C ≈ Set.Iio m := by +/- +> Let +> +> `S = {n ∈ ω | ∀C ⊂ n, ∃m < n such that C ≈ m}`. (2) +> +> We prove that (i) `0 ∈ S` and (ii) if `n ∈ S` then `n⁺ ∈ S`. Afterward we +> prove (iii) the lemma statement. +-/ induction n with +/- +> #### (i) +> By definition, `0 = ∅`. Thus `0` has no proper subsets. Hence `0 ∈ S` +> vacuously. +-/ | zero => intro C hC unfold Set.Iio at hC simp only [Nat.zero_eq, not_lt_zero', Set.setOf_false] at hC rw [Set.ssubset_empty_iff_false] at hC exact False.elim hC +/- +> #### (ii) +> Suppose `n ∈ S` and consider `n⁺`. By definition of the successor, +> `n⁺ = n ∪ {n}`. There are two cases to consider: +-/ | succ n ih => +/- +> Let `C` be an arbitrary, proper subset of `n⁺`. +-/ + intro C hC + + -- A useful theorem we use in a couple of places. have h_subset_equinumerous : ∀ S, S ⊆ Set.Iio n → ∃ m, m < n + 1 ∧ S ≈ Set.Iio m := by @@ -513,120 +614,150 @@ lemma lemma_6f {n : ℕ} · -- `S = Set.Iio n` intro h exact ⟨n, by simp, Set.eq_imp_equinumerous h⟩ - - intro C hC - by_cases hn : n ∈ C - · -- Since `C` is a proper subset of `n⁺`, the set `n⁺ - C` is nonempty. - have hC₁ : Set.Nonempty (Set.Iio (n + 1) \ C) := by - rw [Set.ssubset_def] at hC - have : ¬ ∀ x, x ∈ Set.Iio (n + 1) → x ∈ C := hC.right - simp only [Set.mem_Iio, not_forall, exists_prop] at this - exact this - -- `p` is the least element of `n⁺ - C`. - have ⟨p, hp⟩ := Chapter_4.well_ordering_nat hC₁ - - let C' := (C \ {n}) ∪ {p} - have hC'₁ : C' ⊆ Set.Iio n := by - show ∀ x, x ∈ C' → x ∈ Set.Iio n - intro x hx - match @trichotomous ℕ LT.lt _ x n with - | Or.inl r => exact r - | Or.inr (Or.inl r) => - rw [r] at hx - apply Or.elim hx - · intro nx - simp at nx - · intro nx - simp only [Set.mem_singleton_iff] at nx - rw [nx] at hn - exact absurd hn hp.left.right - | Or.inr (Or.inr r) => - apply Or.elim hx - · intro ⟨h₁, h₂⟩ - have h₃ := subset_of_ssubset hC h₁ - simp only [Set.mem_singleton_iff, Set.mem_Iio] at h₂ h₃ - exact Or.elim (Nat.lt_or_eq_of_lt h₃) id (absurd · h₂) - · intro h - simp only [Set.mem_singleton_iff] at h - have := hp.left.left - rw [← h] at this - exact Or.elim (Nat.lt_or_eq_of_lt this) - id (absurd · (Nat.ne_of_lt r).symm) - have ⟨m, hm₁, hm₂⟩ := h_subset_equinumerous C' hC'₁ - - suffices C' ≈ C from - ⟨m, hm₁, Set.equinumerous_trans (Set.equinumerous_symm this) hm₂⟩ - - -- Proves `f` is a one-to-one correspondence between `C'` and `C`. - let f x := if x = p then n else x - refine ⟨f, ?_, ?_, ?_⟩ - · -- `Set.MapsTo f C' C` - intro x hx - dsimp only - by_cases hxp : x = p - · rw [if_pos hxp] - exact hn - · rw [if_neg hxp] - apply Or.elim hx - · exact fun x => x.left - · intro hx₁ - simp only [Set.mem_singleton_iff] at hx₁ - exact absurd hx₁ hxp - · -- `Set.InjOn f C'` - intro x₁ hx₁ x₂ hx₂ hf - dsimp only at hf - by_cases hx₁p : x₁ = p - · by_cases hx₂p : x₂ = p - · rw [hx₁p, hx₂p] - · rw [if_pos hx₁p, if_neg hx₂p] at hf - apply Or.elim hx₂ - · intro nx - exact absurd hf.symm nx.right - · intro nx - simp only [Set.mem_singleton_iff] at nx - exact absurd nx hx₂p - · by_cases hx₂p : x₂ = p - · rw [if_neg hx₁p, if_pos hx₂p] at hf - apply Or.elim hx₁ - · intro nx - exact absurd hf nx.right - · intro nx - simp only [Set.mem_singleton_iff] at nx - exact absurd nx hx₁p - · rwa [if_neg hx₁p, if_neg hx₂p] at hf - · -- `Set.SurjOn f C' C` - show ∀ x, x ∈ C → x ∈ f '' C' - intro x hx - simp only [ - Set.union_singleton, - Set.mem_diff, - Set.mem_singleton_iff, - Set.mem_image, - Set.mem_insert_iff, - exists_eq_or_imp, - ite_true - ] - by_cases nx₁ : x = n - · left - exact nx₁.symm - · right - by_cases nx₂ : x = p - · have := hp.left.right - rw [← nx₂] at this - exact absurd hx this - · exact ⟨x, ⟨hx, nx₁⟩, by rwa [if_neg]⟩ - +/- +> There are two cases to consider: +-/ + by_cases hn : n ∉ C +/- +> ##### Case 1 +> Suppose `n ∉ C`. Then `C ⊆ n`. If `C` is a proper subset of `n`, *(2)* implies +> `C` is equinumerous to some `m < n < n⁺`. If `C = n`, then *Theorem 6A* +> implies `C` is equinumerous to `n < n⁺`. +-/ · refine h_subset_equinumerous C ?_ show ∀ x, x ∈ C → x ∈ Set.Iio n intro x hx - unfold Set.Iio apply Or.elim (Nat.lt_or_eq_of_lt (subset_of_ssubset hC hx)) · exact id · intro hx₁ rw [hx₁] at hx exact absurd hx hn +/- +> ##### Case 2 +> Suppose `n ∈ C`. Since `C` is a proper subset of `n⁺`, the set `n⁺ - C` is +> nonempty. By the *Well Ordering of `ω`*, `n⁺ - C` has a least element, say +> `p` (which does not equal `n`). +-/ + simp only [not_not] at hn + have hC₁ : Set.Nonempty (Set.Iio (n + 1) \ C) := by + rw [Set.ssubset_def] at hC + have : ¬ ∀ x, x ∈ Set.Iio (n + 1) → x ∈ C := hC.right + simp only [Set.mem_Iio, not_forall, exists_prop] at this + exact this + -- `p` is the least element of `n⁺ - C`. + have ⟨p, hp⟩ := Chapter_4.well_ordering_nat hC₁ +/- +> Consider now set `C' = (C - {n}) ∪ {p}`. By construction, `C' ⊆ n`. +-/ + let C' := (C \ {n}) ∪ {p} + have hC'₁ : C' ⊆ Set.Iio n := by + show ∀ x, x ∈ C' → x ∈ Set.Iio n + intro x hx + match @trichotomous ℕ LT.lt _ x n with + | Or.inl r => exact r + | Or.inr (Or.inl r) => + rw [r] at hx + apply Or.elim hx + · intro nx + simp at nx + · intro nx + simp only [Set.mem_singleton_iff] at nx + rw [nx] at hn + exact absurd hn hp.left.right + | Or.inr (Or.inr r) => + apply Or.elim hx + · intro ⟨h₁, h₂⟩ + have h₃ := subset_of_ssubset hC h₁ + simp only [Set.mem_singleton_iff, Set.mem_Iio] at h₂ h₃ + exact Or.elim (Nat.lt_or_eq_of_lt h₃) id (absurd · h₂) + · intro h + simp only [Set.mem_singleton_iff] at h + have := hp.left.left + rw [← h] at this + exact Or.elim (Nat.lt_or_eq_of_lt this) + id (absurd · (Nat.ne_of_lt r).symm) +/- +> As seen in *Case 1*, `C'` is equinumerous to some `m < n⁺`. +-/ + have ⟨m, hm₁, hm₂⟩ := h_subset_equinumerous C' hC'₁ +/- +> It suffices to show there exists a one-to-one correspondence between `C'` and +> `C`, since then *Theorem 6A* implies `C` is equinumerous to `m` as well. +-/ + suffices C' ≈ C from + ⟨m, hm₁, Set.equinumerous_trans (Set.equinumerous_symm this) hm₂⟩ +/- +> Function `f : C' → C` given by +> +> `f(x) = if x = p then n else x` +> +> is trivially one-to-one and onto as expected. +-/ + let f x := if x = p then n else x + refine ⟨f, ?_, ?_, ?_⟩ + · -- `Set.MapsTo f C' C` + intro x hx + dsimp only + by_cases hxp : x = p + · rw [if_pos hxp] + exact hn + · rw [if_neg hxp] + apply Or.elim hx + · exact fun x => x.left + · intro hx₁ + simp only [Set.mem_singleton_iff] at hx₁ + exact absurd hx₁ hxp + · -- `Set.InjOn f C'` + intro x₁ hx₁ x₂ hx₂ hf + dsimp only at hf + by_cases hx₁p : x₁ = p + · by_cases hx₂p : x₂ = p + · rw [hx₁p, hx₂p] + · rw [if_pos hx₁p, if_neg hx₂p] at hf + apply Or.elim hx₂ + · intro nx + exact absurd hf.symm nx.right + · intro nx + simp only [Set.mem_singleton_iff] at nx + exact absurd nx hx₂p + · by_cases hx₂p : x₂ = p + · rw [if_neg hx₁p, if_pos hx₂p] at hf + apply Or.elim hx₁ + · intro nx + exact absurd hf nx.right + · intro nx + simp only [Set.mem_singleton_iff] at nx + exact absurd nx hx₁p + · rwa [if_neg hx₁p, if_neg hx₂p] at hf + · -- `Set.SurjOn f C' C` + show ∀ x, x ∈ C → x ∈ f '' C' + intro x hx + simp only [ + Set.union_singleton, + Set.mem_diff, + Set.mem_singleton_iff, + Set.mem_image, + Set.mem_insert_iff, + exists_eq_or_imp, + ite_true + ] + by_cases nx₁ : x = n + · left + exact nx₁.symm + · right + by_cases nx₂ : x = p + · have := hp.left.right + rw [← nx₂] at this + exact absurd hx this + · exact ⟨x, ⟨hx, nx₁⟩, by rwa [if_neg]⟩ +/- +> #### (iii) +> By *(i)* and *(ii)*, `S` is an inductive set. By *Theorem 4B*, `S = ω`. +> Therefore, for every proper subset `C` of a natural number `n`, there exists +> some `m < n` such that `C ≈ n`. +-/ -/-- #### Corollary 6G +/-- ### Corollary 6G Any subset of a finite set is finite. -/ @@ -693,7 +824,7 @@ theorem corollary_6g {S S' : Set α} (hS : Set.Finite S) (hS' : S' ⊆ S) · intro h rwa [h] -/-- #### Subset Size +/-- ### Subset Size Let `A` be a finite set and `B ⊂ A`. Then there exist natural numbers `m, n ∈ ω` such that `B ≈ m`, `A ≈ n`, and `m ≤ n`. @@ -751,7 +882,7 @@ lemma subset_size [DecidableEq α] [Nonempty α] {A B : Set α} simp at h₁ exact absurd ⟨h, hh⟩ (corollary_6c hA this) -/-- #### Finite Domain and Range Size +/-- ### Finite Domain and Range Size Let `A` and `B` be finite sets and `f : A → B` be a function. Then there exist natural numbers `m, n ∈ ω` such that `dom f ≈ m`, `ran f ≈ n`, and `m ≥ n`. @@ -778,7 +909,7 @@ theorem finite_dom_ran_size [Nonempty α] {A B : Set α} sorry -/-- #### Set Difference Size +/-- ### Set Difference Size Let `A ≈ m` for some natural number `m` and `B ⊆ A`. Then there exists some `n ∈ ω` such that `B ≈ n` and `A - B ≈ m - n`. @@ -1036,7 +1167,7 @@ lemma sdiff_size [DecidableEq α] [Nonempty α] {A B : Set α} : ∃ n : ℕ, n ≤ m ∧ B ≈ Set.Iio n ∧ A \ B ≈ (Set.Iio m) \ (Set.Iio n) := sdiff_size_aux A hA B hB -/-- #### Exercise 6.7 +/-- ### Exercise 6.7 Assume that `A` is finite and `f : A → A`. Show that `f` is one-to-one **iff** `ran f = A`. @@ -1085,7 +1216,7 @@ theorem exercise_6_7 [DecidableEq α] [Nonempty α] {A : Set α} {f : α → α} have h₂ : A \ {y} ≈ Set.Iio (n₁ - 1) := sorry sorry -/-- #### Exercise 6.8 +/-- ### Exercise 6.8 Prove that the union of two finites sets is finite, without any use of arithmetic. @@ -1094,7 +1225,7 @@ theorem exercise_6_8 {A B : Set α} (hA : Set.Finite A) (hB : Set.Finite B) : Set.Finite (A ∪ B) := by sorry -/-- #### Exercise 6.9 +/-- ### Exercise 6.9 Prove that the Cartesian product of two finites sets is finite, without any use of arithmetic. diff --git a/Bookshelf/Enderton/Set/OrderedPair.lean b/Bookshelf/Enderton/Set/OrderedPair.lean index 35d094f..b3969a0 100644 --- a/Bookshelf/Enderton/Set/OrderedPair.lean +++ b/Bookshelf/Enderton/Set/OrderedPair.lean @@ -28,8 +28,7 @@ theorem ext_iff {x y u v : α} ] at hu huv apply Or.elim hu <;> apply Or.elim huv - · -- #### Case 1 - -- `{u} = {x}` and `{u, v} = {x}`. + · -- `{u} = {x}` and `{u, v} = {x}`. intro huv_x hu_x rw [Set.singleton_eq_singleton_iff] at hu_x rw [hu_x] at huv_x @@ -41,8 +40,7 @@ theorem ext_iff {x y u v : α} rw [← hx_v] at this exact ⟨hu_x.symm, this⟩ - · -- #### Case 2 - -- `{u} = {x}` and `{u, v} = {x, y}`. + · -- `{u} = {x}` and `{u, v} = {x, y}`. intro huv_xy hu_x rw [Set.singleton_eq_singleton_iff] at hu_x rw [hu_x] at huv_xy @@ -58,8 +56,7 @@ theorem ext_iff {x y u v : α} ] at this exact ⟨hu_x.symm, Or.elim this (absurd ·.symm hx_v) (·.symm)⟩ - · -- #### Case 3 - -- `{u} = {x, y}` and `{u, v} = {x}`. + · -- `{u} = {x, y}` and `{u, v} = {x}`. intro huv_x hu_xy rw [Set.ext_iff] at huv_x hu_xy have hu_x := huv_x u @@ -71,7 +68,7 @@ theorem ext_iff {x y u v : α} true_iff, or_true, iff_true - ] at hu_x hy_u + ] at hu_x hy_u apply Or.elim huv · intro huv_x rw [← hu_x, Set.ext_iff] at huv_x @@ -93,19 +90,18 @@ theorem ext_iff {x y u v : α} · intro hv_y exact ⟨hu_x.symm, hv_y.symm⟩ - · -- #### Case 4 - -- `{u} = {x, y}` and `{u, v} = {x, y}`. + · -- `{u} = {x, y}` and `{u, v} = {x, y}`. intro huv_xy hu_xy rw [Set.ext_iff] at huv_xy hu_xy have hx_u := hu_xy x have hy_u := hu_xy y simp only [ Set.mem_singleton_iff, Set.mem_insert_iff, true_or, iff_true, or_true - ] at hx_u hy_u + ] at hx_u hy_u have := huv_xy v simp only [ Set.mem_singleton_iff, Set.mem_insert_iff, or_true, true_iff - ] at this + ] at this apply Or.elim this · intro hv_x rw [hv_x, hx_u] @@ -116,4 +112,4 @@ theorem ext_iff {x y u v : α} · intro h rw [h.left, h.right] -end OrderedPair \ No newline at end of file +end OrderedPair diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean index 75df110..72a7a7a 100644 --- a/Bookshelf/Enderton/Set/Relation.lean +++ b/Bookshelf/Enderton/Set/Relation.lean @@ -168,7 +168,7 @@ theorem ran_inv_eq_dom_self {F : HRelation α β} The restriction of a `Relation` to a `Set`. -/ def restriction (R : HRelation α β) (A : Set α) : HRelation α β := - { p ∈ R | p.1 ∈ A } + { p ∈ R | p.1 ∈ A } /-! ## Image -/ @@ -580,7 +580,7 @@ theorem neighborhood_eq_iff_mem_relate {R : Set.Relation α} {A : Set α} /-- Assume that `R` is an equivalence relation on `A`. If two sets `x` and `y` -belong to the same neighborhood, then `xRy`. +belong to the same neighborhood, then `xRy`. -/ theorem neighborhood_mem_imp_relate {R : Set.Relation α} {A : Set α} (hR : isEquivalence R A) @@ -596,7 +596,7 @@ A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is disjoint and exhaustive. -/ structure Partition (P : Set (Set α)) (A : Set α) : Prop where - p_subset : ∀ p ∈ P, p ⊆ A + p_subset : ∀ p ∈ P, p ⊆ A nonempty : ∀ p ∈ P, Set.Nonempty p disjoint : ∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅ exhaustive : ∀ a ∈ A, ∃ p, p ∈ P ∧ a ∈ p @@ -666,4 +666,4 @@ theorem modEquiv_partition {A : Set α} {R : Relation α} (hR : isEquivalence R end Relation -end Set \ No newline at end of file +end Set diff --git a/Bookshelf/Smullyan/Aviary.lean b/Bookshelf/Smullyan/Aviary.lean index 457a202..a654d00 100644 --- a/Bookshelf/Smullyan/Aviary.lean +++ b/Bookshelf/Smullyan/Aviary.lean @@ -9,7 +9,7 @@ considering they still have the same limitation described above during actual use. Their inclusion here serves more as pseudo-documentation than anything. -/ -/-- #### Bald Eagle +/-- ### Bald Eagle `E'xy₁y₂y₃z₁z₂z₃ = x(y₁y₂y₃)(z₁z₂z₃)` -/ @@ -17,31 +17,31 @@ def E' (x : α → β → γ) (y₁ : δ → ε → α) (y₂ : δ) (y₃ : ε) (z₁ : ζ → η → β) (z₂ : ζ) (z₃ : η) := x (y₁ y₂ y₃) (z₁ z₂ z₃) -/-- #### Becard +/-- ### Becard `B₃xyzw = x(y(zw))` -/ def B₃ (x : α → ε) (y : β → α) (z : γ → β) (w : γ) := x (y (z w)) -/-- #### Blackbird +/-- ### Blackbird `B₁xyzw = x(yzw)` -/ def B₁ (x : α → ε) (y : β → γ → α) (z : β) (w : γ) := x (y z w) -/-- #### Bluebird +/-- ### Bluebird `Bxyz = x(yz)` -/ def B (x : α → γ) (y : β → α) (z : β) := x (y z) -/-- #### Bunting +/-- ### Bunting `B₂xyzwv = x(yzwv)` -/ def B₂ (x : α → ζ) (y : β → γ → ε → α) (z : β) (w : γ) (v : ε) := x (y z w v) -/-- #### Cardinal Once Removed +/-- ### Cardinal Once Removed `C*xyzw = xywz` -/ @@ -49,48 +49,48 @@ def C_star (x : α → β → γ → δ) (y : α) (z : γ) (w : β) := x y w z notation "C*" => C_star -/-- #### Cardinal +/-- ### Cardinal `Cxyz = xzy` -/ def C (x : α → β → δ) (y : β) (z : α) := x z y -/-- #### Converse Warbler +/-- ### Converse Warbler `W'xy = yxx` -/ def W' (x : α) (y : α → α → β) := y x x -/-- #### Dickcissel +/-- ### Dickcissel `D₁xyzwv = xyz(wv)` -/ def D₁ (x : α → β → δ → ε) (y : α) (z : β) (w : γ → δ) (v : γ) := x y z (w v) -/-! #### Double Mockingbird +/-! ### Double Mockingbird `M₂xy = xy(xy)` -/ -/-- #### Dove +/-- ### Dove `Dxyzw = xy(zw)` -/ def D (x : α → γ → δ) (y : α) (z : β → γ) (w : β) := x y (z w) -/-- #### Dovekie +/-- ### Dovekie `D₂xyzwv = x(yz)(wv)` -/ def D₂ (x : α → δ → ε) (y : β → α) (z : β) (w : γ → δ) (v : γ) := x (y z) (w v) -/-- #### Eagle +/-- ### Eagle `Exyzwv = xy(zwv)` -/ def E (x : α → δ → ε) (y : α) (z : β → γ → δ) (w : β) (v : γ) := x y (z w v) -/-- #### Finch Once Removed +/-- ### Finch Once Removed `F*xyzw = xwzy` -/ @@ -98,95 +98,95 @@ def F_star (x : α → β → γ → δ) (y : γ) (z : β) (w : α) := x w z y notation "F*" => F_star -/-- #### Finch +/-- ### Finch `Fxyz = zyx` -/ def F (x : α) (y : β) (z : β → α → γ) := z y x -/-- #### Goldfinch +/-- ### Goldfinch `Gxyzw = xw(yz)` -/ def G (x : α → γ → δ) (y : β → γ) (z : β) (w : α) := x w (y z) -/-- #### Hummingbird +/-- ### Hummingbird `Hxyz = xyzy` -/ def H (x : α → β → α → γ) (y : α) (z : β) := x y z y -/-- #### Identity Bird +/-- ### Identity Bird `Ix = x` -/ def I (x : α) : α := x -/-- #### Kestrel +/-- ### Kestrel `Kxy = x` -/ def K (x : α) (_ : β) := x -/-! #### Lark +/-! ### Lark `Lxy = x(yy)` -/ -/-! #### Mockingbird +/-! ### Mockingbird `Mx = xx` -/ -/-- #### Owl +/-- ### Owl `Oxy = y(xy)` -/ def O (x : (α → β) → α) (y : α → β) := y (x y) -/-- #### Phoenix +/-- ### Phoenix `Φxyzw = x(yw)(zw)` -/ def Φ (x : β → γ → δ) (y : α → β) (z : α → γ) (w : α) := x (y w) (z w) -/-- #### Psi Bird +/-- ### Psi Bird `Ψxyzw = x(yz)(yw)` -/ def Ψ (x : α → α → γ) (y : β → α) (z : β) (w : β) := x (y z) (y w) -/-- #### Quacky Bird +/-- ### Quacky Bird `Q₄xyz = z(yx)` -/ def Q₄ (x : α) (y : α → β) (z : β → γ) := z (y x) -/-- #### Queer Bird +/-- ### Queer Bird `Qxyz = y(xz)` -/ def Q (x : α → β) (y : β → γ) (z : α) := y (x z) -/-- #### Quirky Bird +/-- ### Quirky Bird `Q₃xyz = z(xy)` -/ def Q₃ (x : α → β) (y : α) (z : β → γ) := z (x y) -/-- #### Quixotic Bird +/-- ### Quixotic Bird `Q₁xyz = x(zy)` -/ def Q₁ (x : α → γ) (y : β) (z : β → α) := x (z y) -/-- #### Quizzical Bird +/-- ### Quizzical Bird `Q₂xyz = y(zx)` -/ def Q₂ (x : α) (y : β → γ) (z : α → β) := y (z x) -/-- #### Robin Once Removed +/-- ### Robin Once Removed `R*xyzw = xzwy` -/ @@ -194,36 +194,36 @@ def R_star (x : α → β → γ → δ) (y : γ) (z : α) (w : β) := x z w y notation "R*" => R_star -/-- #### Robin +/-- ### Robin `Rxyz = yzx` -/ def R (x : α) (y : β → α → γ) (z : β) := y z x -/-- #### Sage Bird +/-- ### Sage Bird `Θx = x(Θx)` -/ partial def Θ [Inhabited α] (x : α → α) := x (Θ x) -/-- #### Starling +/-- ### Starling `Sxyz = xz(yz)` -/ def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z) -/-- #### Thrush +/-- ### Thrush `Txy = yx` -/ def T (x : α) (y : α → β) := y x -/-! #### Turing Bird +/-! ### Turing Bird `Uxy = y(xxy)` -/ -/-- #### Vireo Once Removed +/-- ### Vireo Once Removed `V*xyzw = xwyz` -/ @@ -231,13 +231,13 @@ def V_star (x : α → β → γ → δ) (y : β) (z : γ) (w : α) := x w y z notation "V*" => V_star -/-- #### Vireo +/-- ### Vireo `Vxyz = zxy` -/ def V (x : α) (y : β) (z : α → β → γ) := z x y -/-- #### Warbler +/-- ### Warbler `Wxy = xyy` -/ diff --git a/Common/Set/Equinumerous.lean b/Common/Set/Equinumerous.lean index a271fa6..a59ca6e 100644 --- a/Common/Set/Equinumerous.lean +++ b/Common/Set/Equinumerous.lean @@ -8,7 +8,7 @@ Additional theorems around finite sets. namespace Set -/-! ### Definitions -/ +/-! ## Definitions -/ /-- A set `A` is equinumerous to a set `B` (written `A ≈ B`) if and only if there is @@ -79,7 +79,7 @@ theorem eq_imp_equinumerous {A B : Set α} (h : A = B) conv at this => right; rw [h] exact this -/-! ### Finite Sets -/ +/-! ## Finite Sets -/ /-- A set is finite if and only if it is equinumerous to a natural number. @@ -87,7 +87,7 @@ A set is finite if and only if it is equinumerous to a natural number. axiom finite_iff_equinumerous_nat {α : Type _} {S : Set α} : Set.Finite S ↔ ∃ n : ℕ, S ≈ Set.Iio n -/-! ### Emptyset -/ +/-! ## Emptyset -/ /-- Any set equinumerous to the emptyset is the emptyset. @@ -128,4 +128,4 @@ theorem equinumerous_emptyset_emptyset [Bot β] · unfold SurjOn simp -end Set \ No newline at end of file +end Set