import Common.Real.Set /-! # Apostol.Chapter_I_3 A Set of Axioms for the Real-Number System -/ namespace Apostol.Chapter_I_3 #check Archimedean #check Real.exists_isLUB /-! ## The least-upper-bound axiom (completeness axiom) -/ /-- A property holds for the negation of elements in set `S` **iff** it also holds for the elements of the negation of `S`. -/ lemma set_neg_prop_iff_neg_set_prop (S : Set ℝ) (p : ℝ → Prop) : (∀ y, y ∈ S → p (-y)) ↔ (∀ y, y ∈ -S → p y) := by apply Iff.intro · intro h y hy rw [← neg_neg y, Set.neg_mem_neg] at hy have := h (-y) hy simp at this exact this · intro h y hy rw [← Set.neg_mem_neg] at hy exact h (-y) hy /-- The upper bounds of the negation of a set is the negation of the lower bounds of the set. -/ lemma upper_bounds_neg_eq_neg_lower_bounds (S : Set ℝ) : upperBounds (-S) = -lowerBounds S := by suffices (∀ x, x ∈ upperBounds (-S) ↔ x ∈ -(lowerBounds S)) from Set.ext this intro x apply Iff.intro · intro hx unfold lowerBounds show -x ∈ { x | ∀ ⦃a : ℝ⦄, a ∈ S → x ≤ a } show ∀ ⦃a : ℝ⦄, a ∈ S → (-x) ≤ a intro a ha; rw [neg_le]; revert ha a rw [set_neg_prop_iff_neg_set_prop S (fun a => a ≤ x)] exact hx · intro hx unfold upperBounds show ∀ ⦃a : ℝ⦄, a ∈ -S → a ≤ x rw [← set_neg_prop_iff_neg_set_prop S (fun a => a ≤ x)] intro y hy; rw [neg_le]; revert hy y exact hx /-- The negation of the upper bounds of a set is the lower bounds of the negation of the set. -/ lemma neg_upper_bounds_eq_lower_bounds_neg (S : Set ℝ) : -upperBounds S = lowerBounds (-S) := by suffices (∀ x, x ∈ -upperBounds S ↔ x ∈ lowerBounds (-S)) from Set.ext this intro x apply Iff.intro · intro hx unfold lowerBounds show ∀ ⦃a : ℝ⦄, a ∈ -S → x ≤ a rw [← set_neg_prop_iff_neg_set_prop S (fun a => x ≤ a)] intro y hy; rw [le_neg]; revert hy y exact hx · intro hx unfold upperBounds show -x ∈ { x | ∀ ⦃a : ℝ⦄, a ∈ S → a ≤ x } show ∀ ⦃a : ℝ⦄, a ∈ S → a ≤ (-x) intro a ha; rw [le_neg]; revert ha a rw [set_neg_prop_iff_neg_set_prop S (fun a => x ≤ a)] exact hx /-- An element `x` is the least element of the negation of a set **iff** `-x` is the greatest element of the set. -/ lemma is_least_neg_set_eq_is_greatest_set_neq (S : Set ℝ) : IsLeast (-S) x = IsGreatest S (-x) := by unfold IsLeast IsGreatest rw [← neg_upper_bounds_eq_lower_bounds_neg S] rfl /-- At least with respect to `ℝ`, `x` is the least upper bound of set `-S` **iff** `-x` is the greatest lower bound of `S`. -/ theorem is_lub_neg_set_iff_is_glb_set_neg (S : Set ℝ) : IsLUB (-S) x = IsGLB S (-x) := calc IsLUB (-S) x _ = IsLeast (upperBounds (-S)) x := rfl _ = IsLeast (-lowerBounds S) x := by rw [upper_bounds_neg_eq_neg_lower_bounds S] _ = IsGreatest (lowerBounds S) (-x) := by rw [is_least_neg_set_eq_is_greatest_set_neq] _ = IsGLB S (-x) := rfl /-- #### 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`. -/ theorem exists_isGLB (S : Set ℝ) (hne : S.Nonempty) (hbdd : BddBelow S) : ∃ x, IsGLB S x := by -- First we show the negation of a nonempty set bounded below is a nonempty -- set bounded above. In that case, we can then apply the completeness axiom -- to argue the existence of a supremum. have hne' : (-S).Nonempty := Set.nonempty_neg.mpr hne have hbdd' : ∃ x, ∀ (y : ℝ), y ∈ -S → y ≤ x := by rw [bddBelow_def] at hbdd let ⟨lb, lbp⟩ := hbdd refine ⟨-lb, ?_⟩ rw [← set_neg_prop_iff_neg_set_prop S (fun y => y ≤ -lb)] intro y hy exact neg_le_neg (lbp y hy) rw [←bddAbove_def] at hbdd' -- Once we have found a supremum for `-S`, we argue the negation of this value -- is the same as the infimum of `S`. let ⟨ub, ubp⟩ := Real.exists_isLUB (-S) hne' hbdd' exact ⟨-ub, (is_lub_neg_set_iff_is_glb_set_neg S).mp ubp⟩ /-- Every real should be less than or equal to the absolute value of its ceiling. -/ lemma leq_nat_abs_ceil_self (x : ℝ) : x ≤ Int.natAbs ⌈x⌉ := by by_cases h : x ≥ 0 · let k : ℤ := ⌈x⌉ unfold Int.natAbs have k' : k = ⌈x⌉ := rfl rw [←k'] have _ : k ≥ 0 := by -- Hint for match below rw [k', ge_iff_le] exact Int.ceil_nonneg (ge_iff_le.mp h) match k with | Int.ofNat m => calc x _ ≤ ⌈x⌉ := Int.le_ceil x _ = Int.ofNat m := by rw [←k'] · 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' /-! ## The Archimedean property of the real-number system -/ /-- #### Theorem I.29 For every real `x` there exists a positive integer `n` such that `n > x`. -/ theorem exists_pnat_geq_self (x : ℝ) : ∃ n : ℕ+, ↑n > x := by let x' : ℕ+ := ⟨Int.natAbs ⌈x⌉ + 1, by simp⟩ have h : x < x' := calc x _ ≤ Int.natAbs ⌈x⌉ := leq_nat_abs_ceil_self x _ < ↑↑(Int.natAbs ⌈x⌉ + 1) := by simp _ = x' := rfl exact ⟨x', h⟩ /-- #### Theorem I.30 If `x > 0` and if `y` is an arbitrary real number, there exists a positive integer `n` such that `nx > y`. This is known as the *Archimedean Property of the Reals*. -/ theorem exists_pnat_mul_self_geq_of_pos {x y : ℝ} : x > 0 → ∃ n : ℕ+, n * x > y := by intro hx let ⟨n, p⟩ := exists_pnat_geq_self (y / x) have p' := mul_lt_mul_of_pos_right p hx rw [div_mul, div_self (show x ≠ 0 from LT.lt.ne' hx), div_one] at p' exact ⟨n, p'⟩ /-- #### 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`. -/ theorem forall_pnat_leq_self_leq_frac_imp_eq {x y a : ℝ} : (∀ n : ℕ+, a ≤ x ∧ x ≤ a + (y / n)) → x = a := by intro h match @trichotomous ℝ LT.lt _ x a with | Or.inr (Or.inl r) => -- x = a exact r | Or.inl r => -- x < a have z : a < a := lt_of_le_of_lt (h 1).left r simp at z | Or.inr (Or.inr r) => -- x > a let ⟨c, hc⟩ := exists_pos_add_of_lt' r let ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos c y hc.left have hn := mul_lt_mul_of_pos_left hn $ have hp : 0 < (↑↑n : ℝ) := by simp show 0 < ((↑↑n)⁻¹ : ℝ) from inv_pos.mpr hp rw [ inv_mul_eq_div, ← mul_assoc, mul_comm (n⁻¹ : ℝ), ← one_div, mul_one_div ] at hn simp at hn have := calc a + y / ↑↑n _ < a + c := add_lt_add_left hn a _ = x := hc.right _ ≤ a + y / ↑↑n := (h n).right simp at this /-- If three real numbers `a`, `x`, and `y` satisfy the inequalities `a - y / n ≤ x ≤ a` for every integer `n ≥ 1`, then `x = a`. -/ theorem forall_pnat_frac_leq_self_leq_imp_eq {x y a : ℝ} : (∀ n : ℕ+, a - (y / n) ≤ x ∧ x ≤ a) → x = a := by intro h match @trichotomous ℝ LT.lt _ x a with | Or.inr (Or.inl r) => -- x = a exact r | Or.inl r => -- x < a let ⟨c, hc⟩ := exists_pos_add_of_lt' r let ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos c y hc.left have hn := mul_lt_mul_of_pos_left hn $ have hp : 0 < (↑↑n : ℝ) := by simp show 0 < ((↑↑n)⁻¹ : ℝ) from inv_pos.mpr hp rw [ inv_mul_eq_div, ← mul_assoc, mul_comm (n⁻¹ : ℝ), ← one_div, mul_one_div ] at hn simp at hn have := calc a - y / ↑↑n _ > a - c := sub_lt_sub_left hn a _ = x := sub_eq_of_eq_add (Eq.symm hc.right) _ ≥ a - y / ↑↑n := (h n).left simp at this | Or.inr (Or.inr r) => -- x > a have z : x < x := lt_of_le_of_lt (h 1).right r simp at z /-! ## Fundamental properties of the supremum and infimum -/ /-- 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`. -/ lemma mem_upper_bounds_iff_forall_le {S : Set ℝ} : ub ∈ upperBounds S ↔ ∀ x ∈ S, x ≤ ub := by apply Iff.intro · intro h _ hx exact (h hx) · exact id /-- If a set `S` has a least upper bound, it follows every member of `S` is less than or equal to that value. -/ lemma forall_lub_imp_forall_le {S : Set ℝ} : IsLUB S ub → ∀ x ∈ S, x ≤ ub := by intro h rw [← mem_upper_bounds_iff_forall_le] exact h.left /-- Any member of the upper bounds of a set must be greater than or equal to the least member of that set. -/ lemma mem_imp_ge_lub {x : ℝ} (h : IsLUB S s) : x ∈ upperBounds S → x ≥ s := by intro hx exact h.right hx /-- #### 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`. -/ theorem sup_imp_exists_gt_sup_sub_delta {S : Set ℝ} {s h : ℝ} (hp : h > 0) : IsLUB S s → ∃ x ∈ S, x > s - h := by intro hb -- Suppose all members of our set was less than `s - h`. Then `s` couldn't be -- the *least* upper bound. by_contra nb suffices s - h ∈ upperBounds S by have h' : h < h := calc h _ ≤ 0 := (le_sub_self_iff s).mp (hb.right this) _ < h := hp simp at h' rw [not_exists] at nb have nb' : ∀ x ∈ S, x ≤ s - h := by intro x hx exact le_of_not_gt (not_and.mp (nb x) hx) rwa [← mem_upper_bounds_iff_forall_le] at nb' /-- 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`. -/ lemma mem_lower_bounds_iff_forall_ge {S : Set ℝ} : lb ∈ lowerBounds S ↔ ∀ x ∈ S, x ≥ lb := by apply Iff.intro · intro h _ hx exact (h hx) · exact id /-- If a set `S` has a greatest lower bound, it follows every member of `S` is greater than or equal to that value. -/ lemma forall_glb_imp_forall_ge {S : Set ℝ} : IsGLB S lb → ∀ x ∈ S, x ≥ lb := by intro h rw [← mem_lower_bounds_iff_forall_ge] exact h.left /-- Any member of the lower bounds of a set must be less than or equal to the greatest member of that set. -/ lemma mem_imp_le_glb {x : ℝ} (h : IsGLB S s) : x ∈ lowerBounds S → x ≤ s := by intro hx exact h.right hx /-- #### 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`. -/ theorem inf_imp_exists_lt_inf_add_delta {S : Set ℝ} {s h : ℝ} (hp : h > 0) : IsGLB S s → ∃ x ∈ S, x < s + h := by intro hb -- Suppose all members of our set was greater than `s + h`. Then `s` couldn't -- be the *greatest* lower bound. by_contra nb suffices s + h ∈ lowerBounds S by have h' : h < h := calc h _ ≤ 0 := (add_le_iff_nonpos_right s).mp (hb.right this) _ < h := hp simp at h' rw [not_exists] at nb have nb' : ∀ x ∈ S, x ≥ s + h := by intro x hx 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) 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` has a supremum, and `sup C = sup A + sup B`. -/ theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ) (hA : A.Nonempty) (hB : B.Nonempty) (ha : IsLUB A a) (hb : IsLUB B b) : IsLUB (Real.minkowski_sum A B) (a + b) := by let C := Real.minkowski_sum A B -- First we show `a + b` is an upper bound of `C`. have hub : a + b ∈ upperBounds C := by rw [mem_upper_bounds_iff_forall_le] intro x hx have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx have hs₁ : a' ≤ a := (forall_lub_imp_forall_le ha) a' ha' have hs₂ : b' ≤ b := (forall_lub_imp_forall_le hb) b' hb' exact calc x _ = a' + b' := hxab _ ≤ a + b := add_le_add hs₁ hs₂ -- Now we show `a + b` is the *least* upper bound of `C`. We know a least -- upper bound `c` exists; show that `c = a + b`. have ⟨c, hc⟩ := Real.exists_isLUB C (Real.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩) ⟨a + b, hub⟩ suffices (∀ n : ℕ+, c ≤ a + b ∧ a + b ≤ c + (1 / n)) by rwa [← forall_pnat_leq_self_leq_frac_imp_eq this] at hc intro n apply And.intro · exact hc.right hub · have hd : 1 / (2 * n) > (0 : ℝ) := by norm_num have ⟨a', ha'⟩ := sup_imp_exists_gt_sup_sub_delta hd ha have ⟨b', hb'⟩ := sup_imp_exists_gt_sup_sub_delta hd hb have hab' : a + b < a' + b' + 1 / n := by have ha'' := add_lt_add_right ha'.right (1 / (2 * ↑↑n)) have hb'' := add_lt_add_right hb'.right (1 / (2 * ↑↑n)) rw [sub_add_cancel] at ha'' hb'' have hr := add_lt_add ha'' hb'' ring_nf at hr ring_nf rwa [add_assoc, add_comm b' (↑↑n)⁻¹, ← add_assoc] have hc' : a' + b' ≤ c := by refine forall_lub_imp_forall_le hc (a' + b') ?_ show ∃ a ∈ A, ∃ b ∈ B, a' + b' = a + b exact ⟨a', ⟨ha'.left, ⟨b', ⟨hb'.left, rfl⟩⟩⟩⟩ calc 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) 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` has an infimum, and `inf C = inf A + inf B`. -/ theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ) (hA : A.Nonempty) (hB : B.Nonempty) (ha : IsGLB A a) (hb : IsGLB B b) : IsGLB (Real.minkowski_sum A B) (a + b) := by let C := Real.minkowski_sum A B -- First we show `a + b` is a lower bound of `C`. have hlb : a + b ∈ lowerBounds C := by rw [mem_lower_bounds_iff_forall_ge] intro x hx have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx have hs₁ : a' ≥ a := (forall_glb_imp_forall_ge ha) a' ha' have hs₂ : b' ≥ b := (forall_glb_imp_forall_ge hb) b' hb' exact calc x _ = a' + b' := hxab _ ≥ a + b := add_le_add hs₁ hs₂ -- Now we show `a + b` is the *greatest* lower bound of `C`. We know a -- greatest lower bound `c` exists; show that `c = a + b`. have ⟨c, hc⟩ := exists_isGLB C (Real.nonempty_minkowski_sum_iff_nonempty_add_nonempty.mpr ⟨hA, hB⟩) ⟨a + b, hlb⟩ suffices (∀ n : ℕ+, c - (1 / n) ≤ a + b ∧ a + b ≤ c) by rwa [← forall_pnat_frac_leq_self_leq_imp_eq this] at hc intro n apply And.intro · have hd : 1 / (2 * n) > (0 : ℝ) := by norm_num have ⟨a', ha'⟩ := inf_imp_exists_lt_inf_add_delta hd ha have ⟨b', hb'⟩ := inf_imp_exists_lt_inf_add_delta hd hb have hab' : a' + b' - 1 / n < a + b := by have ha'' := sub_lt_sub_right ha'.right (1 / (2 * ↑↑n)) have hb'' := sub_lt_sub_right hb'.right (1 / (2 * ↑↑n)) rw [add_sub_cancel] at ha'' hb'' have hr := add_lt_add ha'' hb'' ring_nf at hr ring_nf rwa [← add_sub_assoc, add_sub_right_comm] have hc' : c ≤ a' + b' := by refine forall_glb_imp_forall_ge hc (a' + b') ?_ show ∃ a ∈ A, ∃ b ∈ B, a' + b' = a + b exact ⟨a', ⟨ha'.left, ⟨b', ⟨hb'.left, rfl⟩⟩⟩⟩ calc c - 1 / n _ ≤ a' + b' - 1 / n := sub_le_sub_right hc' (1 / n) _ ≤ a + b := le_of_lt hab' · exact hc.right hlb /-- #### 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 they satisfy the inequality `sup S ≤ inf T`. -/ theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ) (hS : S.Nonempty) (hT : T.Nonempty) (p : ∀ s ∈ S, ∀ t ∈ T, s ≤ t) : ∃ (s : ℝ), IsLUB S s ∧ ∃ (t : ℝ), IsGLB T t ∧ s ≤ t := by -- Sshow a supremum of `S` and an infimum of `T` exists (since each set bounds -- above and below the other, respectively). let ⟨s, hs⟩ := hS let ⟨t, ht⟩ := hT have ps : t ∈ upperBounds S := by intro x hx exact p x hx t ht have pt : s ∈ lowerBounds T := by intro x hx exact p s hs x hx have ⟨S_lub, hS_lub⟩ := Real.exists_isLUB S hS ⟨t, ps⟩ have ⟨T_glb, hT_glb⟩ := exists_isGLB T hT ⟨s, pt⟩ refine ⟨S_lub, ⟨hS_lub, ⟨T_glb, ⟨hT_glb, ?_⟩⟩⟩⟩ -- Assume `T_glb < S_lub`. Then `∃ c, T_glb + c < S_lub` which in turn implies -- existence of some `x ∈ S` such that `T_glb < S_lub - c / 2 < x < S_lub`. by_contra nr rw [not_le] at nr have ⟨c, hc⟩ := exists_pos_add_of_lt' nr have c_div_two_gt_zero : c / 2 > 0 := by have hr := div_lt_div_of_lt (show (0 : ℝ) < 2 by simp) hc.left rwa [zero_div] at hr have T_glb_lt_S_lub_sub_c_div_two : T_glb < S_lub - c / 2 := by have hr := congrFun (congrArg HSub.hSub hc.right) (c / 2) rw [add_sub_assoc, sub_half c] at hr calc T_glb _ < T_glb + c / 2 := (lt_add_iff_pos_right T_glb).mpr c_div_two_gt_zero _ = S_lub - c / 2 := hr -- Since `x ∈ S`, `p` implies `x ≤ t` for all `t ∈ T`. So `x ≤ T_glb`. But the -- above implies `T_glb < x`. have ⟨x, hx⟩ := sup_imp_exists_gt_sup_sub_delta c_div_two_gt_zero hS_lub have : x < x := calc x _ ≤ T_glb := mem_imp_le_glb hT_glb (p x hx.left) _ < S_lub - c / 2 := T_glb_lt_S_lub_sub_c_div_two _ < x := hx.right simp at this /-! ## Exercises -/ /-- #### 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`. -/ theorem exercise_1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by have ⟨z, hz⟩ := exists_pos_add_of_lt' h refine ⟨x + z / 2, ⟨?_, ?_⟩⟩ · have hz' : z / 2 > 0 := by have hr := div_lt_div_of_lt (show (0 : ℝ) < 2 by simp) hz.left rwa [zero_div] at hr exact (lt_add_iff_pos_right x).mpr hz' · have hz' : z / 2 < z := div_lt_self hz.left (show 1 < 2 by norm_num) calc x + z / 2 _ < x + z := (add_lt_add_iff_left x).mpr hz' _ = y := hz.right /-- #### Exercise 2 If `x` is an arbitrary real number, prove that there are integers `m` and `n` 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 If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`. -/ theorem exercise_3 (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by have ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos x 1 h refine ⟨n, ?_⟩ have hr := mul_lt_mul_of_pos_right hn (show 0 < 1 / ↑↑n by norm_num) conv at hr => arg 2; rw [mul_comm, ← mul_assoc]; simp rwa [one_mul] at hr /-- #### 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 greatest integer in `x` and is denoted by `⌊x⌋`. For example, `⌊5⌋ = 5`, `⌊5 / 2⌋ = 2`, `⌊-8/3⌋ = -3`. -/ theorem exercise_4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by let n := Int.floor x refine ⟨n, ⟨?_, ?_⟩⟩ · exact ⟨Int.floor_le x, Int.lt_floor_add_one x⟩ · intro y hy rw [← Int.floor_eq_iff] at hy exact Eq.symm hy /-- #### Exercise 5 If `x` is an arbitrary real number, prove that there is exactly one integer `n` which satisfies `x ≤ n < x + 1`. -/ theorem exercise_5 (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by let n := Int.ceil x refine ⟨n, ⟨?_, ?_⟩⟩ · exact ⟨Int.le_ceil x, Int.ceil_lt_add_one x⟩ · simp only intro y hy suffices y - 1 < x ∧ x ≤ y by rw [← Int.ceil_eq_iff] at this exact Eq.symm this apply And.intro · have := (sub_lt_sub_iff_right 1).mpr hy.right rwa [add_sub_cancel] at this · exact hy.left /-! #### 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. This property is often described by saying that the rational numbers are *dense* in the real-number system. ###### TODO -/ /-! #### 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. ###### TODO -/ /-! #### Exercise 8 Is the sum or product of two irrational numbers always irrational? ###### TODO -/ /-! #### 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 many. ###### TODO -/ /-! #### 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: (a) An integer cannot be both even and odd. (b) Every integer is either even or odd. (c) The sum or product of two even integers is even. What can you say about the sum or product of two odd integers? (d) If `n²` is even, so is `n`. If `a² = 2b²`, where `a` and `b` are integers, then both `a` and `b` are even. (e) Every rational number can be expressed in the form `a / b`, where `a` and `b` are integers, at least one of which is odd. ###### TODO -/ def is_even (n : ℤ) := ∃ m : ℤ, n = 2 * m def is_odd (n : ℤ) := is_even (n + 1) /-! #### Exercise 11 Prove that there is no rational number whose square is `2`. [Hint: Argue by contradiction. Assume `(a / b)² = 2`, where `a` and `b` are integers, at least one of which is odd. Use parts of Exercise 10 to deduce a contradiction.] ###### TODO -/ /-! #### 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 the Archimedean property but not the least-upper-bound property. This shows that the Archimedean property does not imply the least-upper-bound axiom. ###### TODO -/ end Apostol.Chapter_I_3