Ordering the reals
Analysis I, Section 5.4: Ordering the reals
I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.
Main constructions and results of this section:
-
Ordering on the real line
Tips from past users
Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.
-
(Add tip here)
namespace Chapter5Definition 5.4.1 (sequences bounded away from zero with sign). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.
abbrev BoundedAwayPos (a:ℕ → ℚ) : Prop :=
∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ cDefinition 5.4.1 (sequences bounded away from zero with sign).
abbrev BoundedAwayNeg (a:ℕ → ℚ) : Prop :=
∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -cDefinition 5.4.1 (sequences bounded away from zero with sign).
theorem boundedAwayPos_def (a:ℕ → ℚ) : BoundedAwayPos a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c := a:ℕ → ℚ⊢ BoundedAwayPos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c
All goals completed! 🐙Definition 5.4.1 (sequences bounded away from zero with sign).
theorem boundedAwayNeg_def (a:ℕ → ℚ) : BoundedAwayNeg a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c := a:ℕ → ℚ⊢ BoundedAwayNeg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c
All goals completed! 🐙Examples 5.4.2
example : BoundedAwayPos (fun n ↦ 1 + 10^(-(n:ℤ)-1)) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), (fun n => 1 + 10 ^ (-↑n - 1)) n ≥ 1 n✝:ℕ⊢ (fun n => 1 + 10 ^ (-↑n - 1)) n✝ ≥ 1; n✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); All goals completed! 🐙 ⟩Examples 5.4.2
example : BoundedAwayNeg (fun n ↦ -1 - 10^(-(n:ℤ)-1)) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), (fun n => -1 - 10 ^ (-↑n - 1)) n ≤ -1 n✝:ℕ⊢ (fun n => -1 - 10 ^ (-↑n - 1)) n✝ ≤ -1; n✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); All goals completed! 🐙 ⟩Examples 5.4.2
example : ¬ BoundedAwayPos (fun n ↦ (-1)^n) := ⊢ ¬BoundedAwayPos fun n => (-1) ^ n
c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n => (-1) ^ n) n ≥ c⊢ False; c:ℚh1:c > 0h2:(fun n => (-1) ^ n) 1 ≥ c⊢ False; All goals completed! 🐙Examples 5.4.2
example : ¬ BoundedAwayNeg (fun n ↦ (-1)^n) := ⊢ ¬BoundedAwayNeg fun n => (-1) ^ n
c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n => (-1) ^ n) n ≤ -c⊢ False; c:ℚh1:c > 0h2:(fun n => (-1) ^ n) 0 ≤ -c⊢ False; All goals completed! 🐙Examples 5.4.2
example : BoundedAwayZero (fun n ↦ (-1)^n) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), |(fun n => (-1) ^ n) n| ≥ 1 n✝:ℕ⊢ |(fun n => (-1) ^ n) n✝| ≥ 1; All goals completed! 🐙 ⟩theorem BoundedAwayZero.boundedAwayPos {a:ℕ → ℚ} (ha: BoundedAwayPos a) : BoundedAwayZero a := a:ℕ → ℚha:BoundedAwayPos a⊢ BoundedAwayZero a
a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ |a n| ≥ c; rwa [abs_of_nonneg (a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ 0 ≤ a n All goals completed! 🐙)a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ a n ≥ ctheorem BoundedAwayZero.boundedAwayNeg {a:ℕ → ℚ} (ha: BoundedAwayNeg a) : BoundedAwayZero a := a:ℕ → ℚha:BoundedAwayNeg a⊢ BoundedAwayZero a
a:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ |a n| ≥ c; a:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ -a n ≥ c; All goals completed! 🐙theorem not_boundedAwayPos_boundedAwayNeg {a:ℕ → ℚ} : ¬ (BoundedAwayPos a ∧ BoundedAwayNeg a) := a:ℕ → ℚ⊢ ¬(BoundedAwayPos a ∧ BoundedAwayNeg a)
a:ℕ → ℚw✝¹:ℚleft✝¹:w✝¹ > 0h2:∀ (n : ℕ), a n ≥ w✝¹w✝:ℚleft✝:w✝ > 0h4:∀ (n : ℕ), a n ≤ -w✝⊢ False; All goals completed! 🐙abbrev Real.IsPos (x:Real) : Prop :=
∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM aabbrev Real.IsNeg (x:Real) : Prop :=
∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM atheorem Real.isPos_def (x:Real) :
IsPos x ↔ ∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := x:Real⊢ x.IsPos ↔ ∃ a, BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a All goals completed! 🐙theorem Real.isNeg_def (x:Real) :
IsNeg x ↔ ∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := x:Real⊢ x.IsNeg ↔ ∃ a, BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem Real.trichotomous (x:Real) : x = 0 ∨ x.IsPos ∨ x.IsNeg := x:Real⊢ x = 0 ∨ x.IsPos ∨ x.IsNeg All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem Real.not_zero_pos (x:Real) : ¬(x = 0 ∧ x.IsPos) := x:Real⊢ ¬(x = 0 ∧ x.IsPos) All goals completed! 🐙theorem Real.nonzero_of_pos {x:Real} (hx: x.IsPos) : x ≠ 0 := x:Realhx:x.IsPos⊢ x ≠ 0
x:Realhx:x.IsPosthis:?_mvar.15897 := Chapter5.Real.not_zero_pos _fvar.15893⊢ x ≠ 0
All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem Real.not_zero_neg (x:Real) : ¬(x = 0 ∧ x.IsNeg) := x:Real⊢ ¬(x = 0 ∧ x.IsNeg) All goals completed! 🐙theorem Real.nonzero_of_neg {x:Real} (hx: x.IsNeg) : x ≠ 0 := x:Realhx:x.IsNeg⊢ x ≠ 0
x:Realhx:x.IsNegthis:?_mvar.16366 := Chapter5.Real.not_zero_neg _fvar.16362⊢ x ≠ 0
All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem Real.not_pos_neg (x:Real) : ¬(x.IsPos ∧ x.IsNeg) := x:Real⊢ ¬(x.IsPos ∧ x.IsNeg) All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
@[simp]
theorem Real.neg_iff_pos_of_neg (x:Real) : x.IsNeg ↔ (-x).IsPos := x:Real⊢ x.IsNeg ↔ (-x).IsPos All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem Real.pos_add {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x+y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x + y).IsPos All goals completed! 🐙Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1
theorem Real.pos_mul {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x*y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x * y).IsPos All goals completed! 🐙theorem Real.pos_of_coe (q:ℚ) : (q:Real).IsPos ↔ q > 0 := q:ℚ⊢ (↑q).IsPos ↔ q > 0 All goals completed! 🐙theorem Real.neg_of_coe (q:ℚ) : (q:Real).IsNeg ↔ q < 0 := q:ℚ⊢ (↑q).IsNeg ↔ q < 0 All goals completed! 🐙open Classical in
/-- Need to use classical logic here because isPos and isNeg are not decidable -/
noncomputable abbrev Real.abs (x:Real) : Real := if x.IsPos then x else (if x.IsNeg then -x else 0)Definition 5.4.5 (absolute value)
@[simp]
theorem Real.abs_of_pos (x:Real) (hx: x.IsPos) : abs x = x := x:Realhx:x.IsPos⊢ x.abs = x
All goals completed! 🐙Definition 5.4.5 (absolute value)
@[simp]
theorem Real.abs_of_neg (x:Real) (hx: x.IsNeg) : abs x = -x := x:Realhx:x.IsNeg⊢ x.abs = -x
have : ¬x.IsPos := x:Realhx:x.IsNeg⊢ x.abs = -x x:Realhx:x.IsNegthis:?_mvar.22500 := Chapter5.Real.not_pos_neg _fvar.22489⊢ ¬x.IsPos; All goals completed! 🐙
All goals completed! 🐙Definition 5.4.5 (absolute value)
@[simp]
theorem Real.abs_of_zero : abs 0 = 0 := ⊢ abs 0 = 0
have hpos: ¬(0:Real).IsPos := ⊢ abs 0 = 0 this:?_mvar.259693 := Chapter5.Real.not_zero_pos 0⊢ ¬IsPos 0; All goals completed! 🐙
have hneg: ¬(0:Real).IsNeg := ⊢ abs 0 = 0 hpos:¬Chapter5.Real.IsPos 0 := ?_mvar.259687this:?_mvar.496262 := Chapter5.Real.not_zero_neg 0⊢ ¬IsNeg 0; All goals completed! 🐙
All goals completed! 🐙Definition 5.4.6 (Ordering of the reals)
instance Real.instLE : LE Real where
le x y := (x < y) ∨ (x = y)theorem Real.lt_iff (x y:Real) : x < y ↔ (x-y).IsNeg := x:Realy:Real⊢ x < y ↔ (x - y).IsNeg All goals completed! 🐙theorem Real.le_iff (x y:Real) : x ≤ y ↔ (x < y) ∨ (x = y) := x:Realy:Real⊢ x ≤ y ↔ x < y ∨ x = y All goals completed! 🐙theorem Real.gt_iff (x y:Real) : x > y ↔ (x-y).IsPos := x:Realy:Real⊢ x > y ↔ (x - y).IsPos All goals completed! 🐙theorem Real.ge_iff (x y:Real) : x ≥ y ↔ (x > y) ∨ (x = y) := x:Realy:Real⊢ x ≥ y ↔ x > y ∨ x = y All goals completed! 🐙theorem Real.lt_of_coe (q q':ℚ): q < q' ↔ (q:Real) < (q':Real) := q:ℚq':ℚ⊢ q < q' ↔ ↑q < ↑q' All goals completed! 🐙theorem Real.gt_of_coe (q q':ℚ): q > q' ↔ (q:Real) > (q':Real) := Real.lt_of_coe _ _theorem Real.isPos_iff (x:Real) : x.IsPos ↔ x > 0 := x:Real⊢ x.IsPos ↔ x > 0 All goals completed! 🐙theorem Real.isNeg_iff (x:Real) : x.IsNeg ↔ x < 0 := x:Real⊢ x.IsNeg ↔ x < 0 All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem Real.trichotomous' (x y:Real) : x > y ∨ x < y ∨ x = y := x:Realy:Real⊢ x > y ∨ x < y ∨ x = y All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem Real.not_gt_and_lt (x y:Real) : ¬ (x > y ∧ x < y):= x:Realy:Real⊢ ¬(x > y ∧ x < y) All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem Real.not_gt_and_eq (x y:Real) : ¬ (x > y ∧ x = y):= x:Realy:Real⊢ ¬(x > y ∧ x = y) All goals completed! 🐙Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2
theorem Real.not_lt_and_eq (x y:Real) : ¬ (x < y ∧ x = y):= x:Realy:Real⊢ ¬(x < y ∧ x = y) All goals completed! 🐙Proposition 5.4.7(b) (order is anti-symmetric) / Exercise 5.4.2
theorem Real.antisymm (x y:Real) : x < y ↔ (y - x).IsPos := x:Realy:Real⊢ x < y ↔ (y - x).IsPos All goals completed! 🐙Proposition 5.4.7(c) (order is transitive) / Exercise 5.4.2
theorem Real.lt_trans {x y z:Real} (hxy: x < y) (hyz: y < z) : x < z := x:Realy:Realz:Realhxy:x < yhyz:y < z⊢ x < z All goals completed! 🐙Proposition 5.4.7(d) (addition preserves order) / Exercise 5.4.2
theorem Real.add_lt_add_right {x y:Real} (z:Real) (hxy: x < y) : x + z < y + z := x:Realy:Realz:Realhxy:x < y⊢ x + z < y + z All goals completed! 🐙Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2
theorem Real.mul_lt_mul_right {x y z:Real} (hxy: x < y) (hz: z.IsPos) : x * z < y * z := x:Realy:Realz:Realhxy:x < yhz:z.IsPos⊢ x * z < y * z
x:Realy:Realz:Realhxy:(y - x).IsPoshz:z.IsPos⊢ (y * z - x * z).IsPos; x:Realy:Realz:Realhxy:(y - x).IsPoshz:z.IsPos⊢ y * z - x * z = (y - x) * z; All goals completed! 🐙Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2
theorem Real.mul_le_mul_left {x y z:Real} (hxy: x ≤ y) (hz: z.IsPos) : z * x ≤ z * y := x:Realy:Realz:Realhxy:x ≤ yhz:z.IsPos⊢ z * x ≤ z * y All goals completed! 🐙theorem Real.mul_pos_neg {x y:Real} (hx: x.IsPos) (hy: y.IsNeg) : (x * y).IsNeg := x:Realy:Realhx:x.IsPoshy:y.IsNeg⊢ (x * y).IsNeg
All goals completed! 🐙open Classical in
/--
(Not from textbook) Real has the structure of a linear ordering. The order is not computable,
and so classical logic is required to impose decidability.
-/
noncomputable instance Real.instLinearOrder : LinearOrder Real where
le_refl := sorry
le_trans := sorry
lt_iff_le_not_ge := sorry
le_antisymm := sorry
le_total := sorry
toDecidableLE := Classical.decRel _(Not from textbook) Linear Orders come with a definition of absolute value |.| Show that it agrees with our earlier definition.
theorem Real.abs_eq_abs (x:Real) : |x| = abs x := x:Real⊢ |x| = x.abs All goals completed! 🐙Proposition 5.4.8
theorem Real.inv_of_pos {x:Real} (hx: x.IsPos) : x⁻¹.IsPos := x:Realhx:x.IsPos⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1⊢ x⁻¹.IsPos
have hinv_non: x⁻¹ ≠ 0 := x:Realhx:x.IsPos⊢ x⁻¹.IsPos x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ = 0⊢ x⁻¹ * x ≠ 1; All goals completed! 🐙
have hnonneg : ¬x⁻¹.IsNeg := x:Realhx:x.IsPos⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.741017⁻¹ ≠ 0 := ?_mvar.793453h:x⁻¹.IsNeg⊢ False
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.741017⁻¹ ≠ 0 := ?_mvar.793453h:x⁻¹.IsNegthis:(x * x⁻¹).IsNeg⊢ False
have id : -(1:Real) = (-1:ℚ) := x:Realhx:x.IsPos⊢ x⁻¹.IsPos All goals completed! 🐙
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.741017⁻¹ ≠ 0 := ?_mvar.793453h:x⁻¹.IsNegid:-1 = ↑(-1) := ?_mvar.802738this:-1 > 0⊢ False
All goals completed! 🐙
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.741017⁻¹ ≠ 0 := ?_mvar.793453hnonneg:¬Chapter5.Real.IsNeg _fvar.741017⁻¹ := ?_mvar.794644trich:?_mvar.804208 := Chapter5.Real.trichotomous _fvar.741017⁻¹⊢ x⁻¹.IsPos
All goals completed! 🐙theorem Real.div_of_pos {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x/y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x / y).IsPos All goals completed! 🐙theorem Real.inv_of_gt {x y:Real} (hx: x.IsPos) (hy: y.IsPos) (hxy: x > y) : x⁻¹ < y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > y⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPos⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPosthis:y⁻¹ ≤ x⁻¹⊢ False
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPosthis✝:y⁻¹ ≤ x⁻¹this:1 > 1 := Trans.trans (Trans.trans (Trans.trans ⋯ ⋯) ⋯) ⋯⊢ False
All goals completed! 🐙(Not from textbook) Real has the structure of a strict ordered ring.
instance Real.instIsStrictOrderedRing : IsStrictOrderedRing Real where
add_le_add_left := ⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), c + a ≤ c + b All goals completed! 🐙
add_le_add_right := ⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), a + c ≤ b + c All goals completed! 🐙
mul_lt_mul_of_pos_left := ⊢ ∀ (a b c : Real), a < b → 0 < c → c * a < c * b All goals completed! 🐙
mul_lt_mul_of_pos_right := ⊢ ∀ (a b c : Real), a < b → 0 < c → a * c < b * c All goals completed! 🐙
le_of_add_le_add_left := ⊢ ∀ (a b c : Real), a + b ≤ a + c → b ≤ c All goals completed! 🐙
zero_le_one := ⊢ 0 ≤ 1 All goals completed! 🐙Proposition 5.4.9 (The non-negative reals are closed)
theorem Real.LIM_of_nonneg {a: ℕ → ℚ} (ha: ∀ n, a n ≥ 0) (hcauchy: (a:Sequence).IsCauchy) :
LIM a ≥ 0 := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
-- This proof is written to follow the structure of the original text.
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyhlim:LIM a < 0⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261hlim:x < 0⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261hlim:∃ a, BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a⊢ False; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb:BoundedAwayNeg bhb_cauchy:(↑b).IsCauchyhlim:x = LIM b⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb:∃ c > 0, ∀ (n : ℕ), b n ≤ -chb_cauchy:(↑b).IsCauchyhlim:x = LIM b⊢ False; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -c⊢ False
have claim1 : ∀ n, ¬ (c/2).Close (a n) (b n) := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cn:ℕ⊢ ¬(c / 2).Close (a n) (b n); a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cn:ℕha:a n ≥ 0⊢ ¬(c / 2).Close (a n) (b n); a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ ¬(c / 2).Close (a n) (b n)
a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c / 2 < |a n - b n|
calc
_ < c := a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c / 2 < c All goals completed! 🐙
_ ≤ a n - b n := a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c ≤ a n - b n All goals completed! 🐙
_ ≤ _ := le_abs_self _
have claim2 : ¬(c/2).EventuallyClose (a:Sequence) (b:Sequence) := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:(c / 2).EventuallyClose ↑a ↑b⊢ ∃ n, (c / 2).Close (a n) (b n); a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∃ N, ∀ n ≥ N, |a n - b n| ≤ c / 2⊢ ∃ n, (c / 2).Close (a n) (b n); a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1✝:∃ N, ∀ n ≥ N, |a n - b n| ≤ c / 2N:ℕclaim1:∀ n ≥ N, |a n - b n| ≤ c / 2⊢ (c / 2).Close (a N) (b N); All goals completed! 🐙
have claim3 : ¬Sequence.Equiv a b := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0 a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(_fvar.811942 / 2).Close (@_fvar.811261 n) (@_fvar.811886 n) := ?_mvar.812043claim2:Sequence.Equiv a b⊢ (c / 2).EventuallyClose ↑a ↑b; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(_fvar.811942 / 2).Close (@_fvar.811261 n) (@_fvar.811886 n) := ?_mvar.812043claim2:∀ ε > 0, ε.EventuallyClose ↑a ↑b⊢ (c / 2).EventuallyClose ↑a ↑b; All goals completed! 🐙
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811261b:ℕ → ℚhb_cauchy:(↑b).IsCauchyc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(_fvar.811942 / 2).Close (@_fvar.811261 n) (@_fvar.811886 n) := ?_mvar.812043claim2:¬Rat.EventuallyClose (_fvar.811942 / 2) ↑_fvar.811261 ↑_fvar.811886 := ?_mvar.815094claim3:¬Chapter5.Sequence.Equiv _fvar.811261 _fvar.811886 := ?_mvar.827492hlim:Sequence.Equiv a b⊢ False
All goals completed! 🐙Corollary 5.4.10
theorem Real.LIM_mono {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy)
(hmono: ∀ n, a n ≤ b n) :
LIM a ≤ LIM b := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b n⊢ LIM a ≤ LIM b
-- This proof is written to follow the structure of the original text.
have := LIM_of_nonneg (a := b - a) (a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b n⊢ ∀ (n : ℕ), (b - a) n ≥ 0 a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b nn:ℕ⊢ (b - a) n ≥ 0; All goals completed! 🐙) (Sequence.IsCauchy.sub hb ha)
a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b nthis:LIM b - LIM a ≥ 0⊢ LIM a ≤ LIM b; All goals completed! 🐙Remark 5.4.11 -
theorem Real.LIM_mono_fail :
∃ (a b:ℕ → ℚ), (a:Sequence).IsCauchy
∧ (b:Sequence).IsCauchy
∧ (∀ n, a n > b n)
∧ ¬LIM a > LIM b := ⊢ ∃ a b, (↑a).IsCauchy ∧ (↑b).IsCauchy ∧ (∀ (n : ℕ), a n > b n) ∧ ¬LIM a > LIM b
⊢ ∃ b,
(↑fun n => 1 + 1 / (↑n + 1)).IsCauchy ∧
(↑b).IsCauchy ∧ (∀ (n : ℕ), (fun n => 1 + 1 / (↑n + 1)) n > b n) ∧ ¬(LIM fun n => 1 + 1 / (↑n + 1)) > LIM b
⊢ (↑fun n => 1 + 1 / (↑n + 1)).IsCauchy ∧
(↑fun n => 1 - 1 / (↑n + 1)).IsCauchy ∧
(∀ (n : ℕ), 1 + 1 / (↑n + 1) > (fun n => 1 - 1 / (↑n + 1)) n) ∧
¬(LIM fun n => 1 + 1 / (↑n + 1)) > LIM fun n => 1 - 1 / (↑n + 1)
All goals completed! 🐙Proposition 5.4.12 (Bounding reals by rationals)
theorem Real.exists_rat_le_and_nat_ge {x:Real} (hx: x.IsPos) :
(∃ q:ℚ, q > 0 ∧ (q:Real) ≤ x) ∧ ∃ N:ℕ, x < (N:Real) := x:Realhx:x.IsPos⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
-- This proof is written to follow the structure of the original text.
x:Realhx:∃ a, BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhbound:BoundedAwayPos ahcauchy:(↑a).IsCauchyheq:x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhbound:∃ c > 0, ∀ (n : ℕ), a n ≥ chcauchy:(↑a).IsCauchyheq:x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ q⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qthis:?_mvar.836461 := Chapter5.Sequence.isBounded_of_isCauchy _fvar.836430⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qthis:∃ M ≥ 0, (↑a).BoundedBy M⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:(↑a).BoundedBy r⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q ≤ xx:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q ≤ x x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q = LIM fun x => q
All goals completed! 🐙
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x < ↑N
calc
x ≤ r := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x ≤ ↑r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x ≤ LIM fun x => r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ∀ (n : ℕ), a n ≤ r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑Nn:ℕ⊢ a n ≤ r; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0N:ℕhN:r < ↑Nn:ℕthis:|if 0 ≤ ↑n then a (↑n).toNat else 0| ≤ r⊢ a n ≤ r; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0N:ℕhN:r < ↑Nn:ℕthis:|a n| ≤ r⊢ a n ≤ r
All goals completed! 🐙
_ < ((N:ℚ):Real) := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ↑r < ↑↑N All goals completed! 🐙
_ = N := rflCorollary 5.4.13 (Archimedean property )
theorem Real.le_mul {ε:Real} (hε: ε.IsPos) (x:Real) : ∃ M:ℕ, M > 0 ∧ M * ε > x := ε:Realhε:ε.IsPosx:Real⊢ ∃ M > 0, ↑M * ε > x
-- This proof is written to follow the structure of the original text.
ε:Realhε:ε.IsPos⊢ ∃ M > 0, ↑M * ε > 0ε:Realhε:ε.IsPosx:Realhx:x.IsPos⊢ ∃ M > 0, ↑M * ε > xε:Realhε:ε.IsPosx:Realhx:x.IsNeg⊢ ∃ M > 0, ↑M * ε > x
ε:Realhε:ε.IsPos⊢ ∃ M > 0, ↑M * ε > 0 ε:Realhε:ε.IsPos⊢ 1 > 0 ∧ ↑1 * ε > 0; All goals completed! 🐙
ε:Realhε:ε.IsPosx:Realhx:x.IsPos⊢ ∃ M > 0, ↑M * ε > x ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑N⊢ ∃ M > 0, ↑M * ε > x
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := _fvar.851138 + 1⊢ ∃ M > 0, ↑M * ε > x; refine ⟨ M, ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := _fvar.851138 + 1⊢ M > 0 All goals completed! 🐙, ?_ ⟩
replace hN : x/ε < M := hN.trans (ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := _fvar.851138 + 1⊢ ↑N < ↑M All goals completed! 🐙)
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕM:ℕ := _fvar.851138 + 1hN:_fvar.847982 / _fvar.847980 < ↑_fvar.851227 := LT.lt.trans _fvar.851141 ?_mvar.853540⊢ x < ↑M * ε
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕM:ℕ := _fvar.851138 + 1hN:_fvar.847982 / _fvar.847980 < ↑_fvar.851227 := LT.lt.trans _fvar.851141 ?_mvar.853540⊢ x = x / ε * ε
ε:Realhε:ε > 0x:Realhx:x.IsPosN:ℕM:ℕ := _fvar.859059 + 1hN:x / ε < ↑M⊢ x = x / ε * ε; All goals completed! 🐙
ε:Realhε:ε.IsPosx:Realhx:x.IsNeg⊢ 1 > 0 ∧ ↑1 * ε > x; ε:Realx:Realhε:0 < εhx:x < 0⊢ x < ε; All goals completed! 🐙Proposition 5.4.14 / Exercise 5.4.5
theorem Real.rat_between {x y:Real} (hxy: x < y) : ∃ q:ℚ, x < (q:Real) ∧ (q:Real) < y := x:Realy:Realhxy:x < y⊢ ∃ q, x < ↑q ∧ ↑q < y All goals completed! 🐙Exercise 5.4.3
theorem Real.floor_exist (x:Real) : ∃! n:ℤ, (n:Real) ≤ x ∧ x < (n:Real)+1 := x:Real⊢ ∃! n, ↑n ≤ x ∧ x < ↑n + 1 All goals completed! 🐙Exercise 5.4.4
theorem Real.exist_inv_nat_le {x:Real} (hx: x.IsPos) : ∃ N:ℤ, N>0 ∧ (N:Real)⁻¹ < x := x:Realhx:x.IsPos⊢ ∃ N > 0, (↑N)⁻¹ < x All goals completed! 🐙Exercise 5.4.6
theorem Real.dist_lt_iff (ε x y:Real) : |x-y| < ε ↔ y-ε < x ∧ x < y+ε := ε:Realx:Realy:Real⊢ |x - y| < ε ↔ y - ε < x ∧ x < y + ε All goals completed! 🐙Exercise 5.4.6
theorem Real.dist_le_iff (ε x y:Real) : |x-y| ≤ ε ↔ y-ε ≤ x ∧ x ≤ y+ε := ε:Realx:Realy:Real⊢ |x - y| ≤ ε ↔ y - ε ≤ x ∧ x ≤ y + ε All goals completed! 🐙Exercise 5.4.7
theorem Real.le_add_eps_iff (x y:Real) : (∀ ε > 0, x ≤ y+ε) ↔ x ≤ y := x:Realy:Real⊢ (∀ ε > 0, x ≤ y + ε) ↔ x ≤ y All goals completed! 🐙Exercise 5.4.7
theorem Real.dist_le_eps_iff (x y:Real) : (∀ ε > 0, |x-y| ≤ ε) ↔ x = y := x:Realy:Real⊢ (∀ ε > 0, |x - y| ≤ ε) ↔ x = y All goals completed! 🐙Exercise 5.4.8
theorem Real.LIM_of_le {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∀ n, a n ≤ x) :
LIM a ≤ x := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∀ (n : ℕ), ↑(a n) ≤ x⊢ LIM a ≤ x All goals completed! 🐙Exercise 5.4.8
theorem Real.LIM_of_ge {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∀ n, a n ≥ x) :
LIM a ≥ x := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∀ (n : ℕ), ↑(a n) ≥ x⊢ LIM a ≥ x All goals completed! 🐙theorem Real.max_eq (x y:Real) : max x y = if x ≥ y then x else y := max_def' x ytheorem Real.min_eq (x y:Real) : min x y = if x ≤ y then x else y := rflExercise 5.4.9
theorem Real.neg_max (x y:Real) : max x y = - min (-x) (-y) := x:Realy:Real⊢ max x y = -min (-x) (-y) All goals completed! 🐙Exercise 5.4.9
theorem Real.neg_min (x y:Real) : min x y = - max (-x) (-y) := x:Realy:Real⊢ min x y = -max (-x) (-y) All goals completed! 🐙Exercise 5.4.9
theorem Real.max_comm (x y:Real) : max x y = max y x := x:Realy:Real⊢ max x y = max y x All goals completed! 🐙Exercise 5.4.9
theorem Real.max_self (x:Real) : max x x = x := x:Real⊢ max x x = x All goals completed! 🐙Exercise 5.4.9
theorem Real.max_add (x y z:Real) : max (x + z) (y + z) = max x y + z := x:Realy:Realz:Real⊢ max (x + z) (y + z) = max x y + z All goals completed! 🐙Exercise 5.4.9
theorem Real.max_mul (x y :Real) {z:Real} (hz: z.IsPos) : max (x * z) (y * z) = max x y * z := x:Realy:Realz:Realhz:z.IsPos⊢ max (x * z) (y * z) = max x y * z
All goals completed! 🐙/- Additional exercise: What happens if z is negative? -/Exercise 5.4.9
theorem Real.min_comm (x y:Real) : min x y = min y x := x:Realy:Real⊢ min x y = min y x All goals completed! 🐙Exercise 5.4.9
theorem Real.min_self (x:Real) : min x x = x := x:Real⊢ min x x = x All goals completed! 🐙Exercise 5.4.9
theorem Real.min_add (x y z:Real) : min (x + z) (y + z) = min x y + z := x:Realy:Realz:Real⊢ min (x + z) (y + z) = min x y + z All goals completed! 🐙Exercise 5.4.9
theorem Real.min_mul (x y :Real) {z:Real} (hz: z.IsPos) : min (x * z) (y * z) = min x y * z := x:Realy:Realz:Realhz:z.IsPos⊢ min (x * z) (y * z) = min x y * z
All goals completed! 🐙Exercise 5.4.9
theorem Real.inv_max {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (max x y)⁻¹ = min x⁻¹ y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (max x y)⁻¹ = min x⁻¹ y⁻¹ All goals completed! 🐙Exercise 5.4.9
theorem Real.inv_min {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (min x y)⁻¹ = max x⁻¹ y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (min x y)⁻¹ = max x⁻¹ y⁻¹ All goals completed! 🐙Not from textbook: the rationals map as an ordered ring homomorphism into the reals.
abbrev Real.ratCast_ordered_hom : ℚ →+*o Real where
toRingHom := ratCast_hom
monotone' := ⊢ Monotone (↑↑ratCast_hom).toFun All goals completed! 🐙end Chapter5