@[reducible, inline]

abbrev Chapter5.BoundedAwayPos (a : ℕ → ℚ) : Prop

Definition 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.

Equations

• Chapter5.BoundedAwayPos a = ∃ c > 0, ∀ (n : ℕ), a n ≥ c

@[reducible, inline]

abbrev Chapter5.BoundedAwayNeg (a : ℕ → ℚ) : Prop

Definition 5.4.1 (sequences bounded away from zero with sign).

Equations

• Chapter5.BoundedAwayNeg a = ∃ c > 0, ∀ (n : ℕ), a n ≤ -c

theorem Chapter5.boundedAwayPos_def (a : ℕ → ℚ) : BoundedAwayPos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c

Definition 5.4.1 (sequences bounded away from zero with sign).

theorem Chapter5.boundedAwayNeg_def (a : ℕ → ℚ) : BoundedAwayNeg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c

Definition 5.4.1 (sequences bounded away from zero with sign).

theorem Chapter5.BoundedAwayZero.boundedAwayPos {a : ℕ → ℚ} (ha : BoundedAwayPos a) : BoundedAwayZero a

theorem Chapter5.BoundedAwayZero.boundedAwayNeg {a : ℕ → ℚ} (ha : BoundedAwayNeg a) : BoundedAwayZero a

theorem Chapter5.not_boundedAwayPos_boundedAwayNeg {a : ℕ → ℚ} : ¬(BoundedAwayPos a ∧ BoundedAwayNeg a)

@[reducible, inline]

abbrev Chapter5.Real.IsPos (x : Real) : Prop

Equations

• x.IsPos = ∃ (a : ℕ → ℚ), Chapter5.BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = Chapter5.LIM a

@[reducible, inline]

abbrev Chapter5.Real.IsNeg (x : Real) : Prop

Equations

• x.IsNeg = ∃ (a : ℕ → ℚ), Chapter5.BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = Chapter5.LIM a

theorem Chapter5.Real.isPos_def (x : Real) : x.IsPos ↔ ∃ (a : ℕ → ℚ), BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a

theorem Chapter5.Real.isNeg_def (x : Real) : x.IsNeg ↔ ∃ (a : ℕ → ℚ), BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a

theorem Chapter5.Real.trichotomous (x : Real) : x = 0 ∨ x.IsPos ∨ x.IsNeg

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

theorem Chapter5.Real.not_zero_pos (x : Real) : ¬(x = 0 ∧ x.IsPos)

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

theorem Chapter5.Real.nonzero_of_pos {x : Real} (hx : x.IsPos) : x ≠ 0

theorem Chapter5.Real.not_zero_neg (x : Real) : ¬(x = 0 ∧ x.IsNeg)

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

theorem Chapter5.Real.nonzero_of_neg {x : Real} (hx : x.IsNeg) : x ≠ 0

theorem Chapter5.Real.not_pos_neg (x : Real) : ¬(x.IsPos ∧ x.IsNeg)

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

@[simp]

theorem Chapter5.Real.neg_iff_pos_of_neg (x : Real) : x.IsNeg ↔ (-x).IsPos

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

theorem Chapter5.Real.pos_add {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (x + y).IsPos

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

theorem Chapter5.Real.pos_mul {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (x * y).IsPos

Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1

theorem Chapter5.Real.pos_of_coe (q : ℚ) : (↑q).IsPos ↔ q > 0

theorem Chapter5.Real.neg_of_coe (q : ℚ) : (↑q).IsNeg ↔ q < 0

@[reducible, inline]

noncomputable abbrev Chapter5.Real.abs (x : Real) : Real

Need to use classical logic here because IsPos and IsNeg are not decidable

Equations

• x.abs = if x.IsPos then x else if x.IsNeg then -x else 0

@[simp]

theorem Chapter5.Real.abs_of_pos (x : Real) (hx : x.IsPos) : x.abs = x

Definition 5.4.5 (absolute value)

@[simp]

theorem Chapter5.Real.abs_of_neg (x : Real) (hx : x.IsNeg) : x.abs = -x

Definition 5.4.5 (absolute value)

@[simp]

theorem Chapter5.Real.abs_of_zero : abs 0 = 0

Definition 5.4.5 (absolute value)

@[implicit_reducible]

instance Chapter5.Real.instLT : LT Real

Definition 5.4.6 (Ordering of the reals)

Equations

• Chapter5.Real.instLT = { lt := fun (x y : Chapter5.Real) => (x - y).IsNeg }

@[implicit_reducible]

instance Chapter5.Real.instLE : LE Real

Definition 5.4.6 (Ordering of the reals)

Equations

• Chapter5.Real.instLE = { le := fun (x y : Chapter5.Real) => x < y ∨ x = y }

theorem Chapter5.Real.lt_iff (x y : Real) : x < y ↔ (x - y).IsNeg

theorem Chapter5.Real.le_iff (x y : Real) : x ≤ y ↔ x < y ∨ x = y

theorem Chapter5.Real.gt_iff (x y : Real) : x > y ↔ (x - y).IsPos

theorem Chapter5.Real.ge_iff (x y : Real) : x ≥ y ↔ x > y ∨ x = y

theorem Chapter5.Real.lt_of_coe (q q' : ℚ) : q < q' ↔ ↑q < ↑q'

theorem Chapter5.Real.gt_of_coe (q q' : ℚ) : q > q' ↔ ↑q > ↑q'

theorem Chapter5.Real.isPos_iff (x : Real) : x.IsPos ↔ x > 0

theorem Chapter5.Real.isNeg_iff (x : Real) : x.IsNeg ↔ x < 0

theorem Chapter5.Real.trichotomous' (x y : Real) : x > y ∨ x < y ∨ x = y

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.not_gt_and_lt (x y : Real) : ¬(x > y ∧ x < y)

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.not_gt_and_eq (x y : Real) : ¬(x > y ∧ x = y)

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.not_lt_and_eq (x y : Real) : ¬(x < y ∧ x = y)

Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2

theorem Chapter5.Real.antisymm (x y : Real) : x < y ↔ y > x

Proposition 5.4.7(b) (order is anti-symmetric) / Exercise 5.4.2

theorem Chapter5.Real.lt_trans {x y z : Real} (hxy : x < y) (hyz : y < z) : x < z

Proposition 5.4.7(c) (order is transitive) / Exercise 5.4.2

theorem Chapter5.Real.add_lt_add_right {x y : Real} (z : Real) (hxy : x < y) : x + z < y + z

Proposition 5.4.7(d) (addition preserves order) / Exercise 5.4.2

theorem Chapter5.Real.mul_lt_mul_right {x y z : Real} (hxy : x < y) (hz : z.IsPos) : x * z < y * z

Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2

theorem Chapter5.Real.mul_le_mul_left {x y z : Real} (hxy : x ≤ y) (hz : z.IsPos) : z * x ≤ z * y

Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2

theorem Chapter5.Real.mul_pos_neg {x y : Real} (hx : x.IsPos) (hy : y.IsNeg) : (x * y).IsNeg

@[implicit_reducible]

noncomputable instance Chapter5.Real.instLinearOrder : LinearOrder Real

(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.

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter5.Real.abs_eq_abs (x : Real) : |x| = x.abs

(Not from textbook) LinearOrders come with a definition of absolute value (|·|). Show that it agrees with our earlier definition.

theorem Chapter5.Real.inv_of_pos {x : Real} (hx : x.IsPos) : x⁻¹.IsPos

Proposition 5.4.8

theorem Chapter5.Real.div_of_pos {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (x / y).IsPos

theorem Chapter5.Real.inv_of_gt {x y : Real} (hx : x.IsPos) (hy : y.IsPos) (hxy : x > y) : x⁻¹ < y⁻¹

instance Chapter5.Real.instIsStrictOrderedRing : IsStrictOrderedRing Real

(Not from textbook) Real has the structure of a strict ordered ring.

theorem Chapter5.Real.LIM_of_nonneg {a : ℕ → ℚ} (ha : ∀ (n : ℕ), a n ≥ 0) (hcauchy : (↑a).IsCauchy) : LIM a ≥ 0

Proposition 5.4.9 (The non-negative reals are closed)

theorem Chapter5.Real.LIM_mono {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) (hmono : ∀ (n : ℕ), a n ≤ b n) : LIM a ≤ LIM b

Corollary 5.4.10

theorem Chapter5.Real.LIM_mono_fail : ∃ (a : ℕ → ℚ) (b : ℕ → ℚ), (↑a).IsCauchy ∧ (↑b).IsCauchy ∧ (∀ (n : ℕ), a n > b n) ∧ ¬LIM a > LIM b

Remark 5.4.11 -

theorem Chapter5.Real.exists_rat_le_and_nat_gt {x : Real} (hx : x.IsPos) : (∃ q > 0, ↑q ≤ x) ∧ ∃ (N : ℕ), x < ↑N

Proposition 5.4.12 (Bounding reals by rationals)

theorem Chapter5.Real.le_mul {ε : Real} (hε : ε.IsPos) (x : Real) : ∃ M > 0, ↑M * ε > x

Corollary 5.4.13 (Archimedean property )

theorem Chapter5.Real.rat_between {x y : Real} (hxy : x < y) : ∃ (q : ℚ), x < ↑q ∧ ↑q < y

Proposition 5.4.14 / Exercise 5.4.5

theorem Chapter5.Real.floor_exist (x : Real) : ∃! n : ℤ, ↑n ≤ x ∧ x < ↑n + 1

Exercise 5.4.3

theorem Chapter5.Real.exist_inv_nat_le {x : Real} (hx : x.IsPos) : ∃ N > 0, (↑N)⁻¹ < x

Exercise 5.4.4

theorem Chapter5.Real.dist_lt_iff (ε x y : Real) : |x - y| < ε ↔ y - ε < x ∧ x < y + ε

Exercise 5.4.6

theorem Chapter5.Real.dist_le_iff (ε x y : Real) : |x - y| ≤ ε ↔ y - ε ≤ x ∧ x ≤ y + ε

Exercise 5.4.6

theorem Chapter5.Real.le_add_eps_iff (x y : Real) : (∀ ε > 0, x ≤ y + ε) ↔ x ≤ y

Exercise 5.4.7

theorem Chapter5.Real.dist_le_eps_iff (x y : Real) : (∀ ε > 0, |x - y| ≤ ε) ↔ x = y

Exercise 5.4.7

theorem Chapter5.Real.LIM_of_le {x : Real} {a : ℕ → ℚ} (hcauchy : (↑a).IsCauchy) (h : ∀ (n : ℕ), ↑(a n) ≤ x) : LIM a ≤ x

Exercise 5.4.8

theorem Chapter5.Real.LIM_of_ge {x : Real} {a : ℕ → ℚ} (hcauchy : (↑a).IsCauchy) (h : ∀ (n : ℕ), ↑(a n) ≥ x) : LIM a ≥ x

Exercise 5.4.8

theorem Chapter5.Real.max_eq (x y : Real) : max x y = if x ≥ y then x else y

theorem Chapter5.Real.min_eq (x y : Real) : min x y = if x ≤ y then x else y

theorem Chapter5.Real.neg_max (x y : Real) : max x y = -min (-x) (-y)

Exercise 5.4.9

theorem Chapter5.Real.neg_min (x y : Real) : min x y = -max (-x) (-y)

Exercise 5.4.9

theorem Chapter5.Real.max_comm (x y : Real) : max x y = max y x

Exercise 5.4.9

theorem Chapter5.Real.max_self (x : Real) : max x x = x

Exercise 5.4.9

theorem Chapter5.Real.max_add (x y z : Real) : max (x + z) (y + z) = max x y + z

Exercise 5.4.9

theorem Chapter5.Real.max_mul (x y : Real) {z : Real} (hz : z.IsPos) : max (x * z) (y * z) = max x y * z

Exercise 5.4.9

theorem Chapter5.Real.min_comm (x y : Real) : min x y = min y x

Exercise 5.4.9

theorem Chapter5.Real.min_self (x : Real) : min x x = x

Exercise 5.4.9

theorem Chapter5.Real.min_add (x y z : Real) : min (x + z) (y + z) = min x y + z

Exercise 5.4.9

theorem Chapter5.Real.min_mul (x y : Real) {z : Real} (hz : z.IsPos) : min (x * z) (y * z) = min x y * z

Exercise 5.4.9

theorem Chapter5.Real.inv_max {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (max x y)⁻¹ = min x⁻¹ y⁻¹

Exercise 5.4.9

theorem Chapter5.Real.inv_min {x y : Real} (hx : x.IsPos) (hy : y.IsPos) : (min x y)⁻¹ = max x⁻¹ y⁻¹

Exercise 5.4.9

@[reducible, inline]

abbrev Chapter5.Real.ratCast_ordered_hom : ℚ →+*o Real

Not from textbook: the rationals map as an ordered ring homomorphism into the reals.

Equations

• Chapter5.Real.ratCast_ordered_hom = { toRingHom := Chapter5.Real.ratCast_hom, monotone' := ⋯ }