theorem Chapter5.Real.upperBound_def (E : Set Real) (M : Real) : M ∈ upperBounds E ↔ ∀ x ∈ E, x ≤ M

Definition 5.5.1 (upper bounds). Here we use the upperBounds set defined in Mathlib.

theorem Chapter5.Real.lowerBound_def (E : Set Real) (M : Real) : M ∈ lowerBounds E ↔ ∀ x ∈ E, x ≥ M

theorem Chapter5.Real.Icc_def (x y : Real) : Set.Icc x y = {z : Real | x ≤ z ∧ z ≤ y}

API for Example 5.5.2

theorem Chapter5.Real.mem_Icc (x y z : Real) : z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y

API for Example 5.5.2

theorem Chapter5.Real.Ioi_def (x : Real) : Set.Ioi x = {z : Real | z > x}

API for Example 5.5.3

theorem Chapter5.Real.upperBound_upper {M M' : Real} (h : M ≤ M') {E : Set Real} (hb : M ∈ upperBounds E) : M' ∈ upperBounds E

theorem Chapter5.Real.isLUB_def (E : Set Real) (M : Real) : IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M

Definition 5.5.5 (least upper bound). Here we use the IsLUB predicate defined in Mathlib.

theorem Chapter5.Real.isGLB_def (E : Set Real) (M : Real) : IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M

theorem Chapter5.Real.LUB_unique {E : Set Real} {M M' : Real} (h1 : IsLUB E M) (h2 : IsLUB E M') : M = M'

Proposition 5.5.8 (Uniqueness of least upper bound)

theorem Chapter5.Real.bddAbove_def (E : Set Real) : BddAbove E ↔ ∃ (M : Real), M ∈ upperBounds E

Definition of "bounded above", using Mathlib notation

theorem Chapter5.Real.bddBelow_def (E : Set Real) : BddBelow E ↔ ∃ (M : Real), M ∈ lowerBounds E

theorem Chapter5.Real.upperBound_between {E : Set Real} {n : ℕ} {L K : ℤ} (hLK : L < K) (hK : ↑K * ↑(1 / (↑n + 1)) ∈ upperBounds E) (hL : ↑L * ↑(1 / (↑n + 1)) ∉ upperBounds E) : ∃ (m : ℤ), L < m ∧ m ≤ K ∧ ↑m * ↑(1 / (↑n + 1)) ∈ upperBounds E ∧ (↑m - 1) * ↑(1 / (↑n + 1)) ∉ upperBounds E

Exercise 5.5.2

theorem Chapter5.Real.upperBound_discrete_unique {E : Set Real} {n : ℕ} {m m' : ℤ} (hm1 : ↑(↑m / (↑n + 1)) ∈ upperBounds E) (hm2 : ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E) (hm'1 : ↑(↑m' / (↑n + 1)) ∈ upperBounds E) (hm'2 : ↑(↑m' / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E) : m = m'

Exercise 5.5.3

theorem Chapter5.Sequence.IsCauchy.abs {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : (↑|a|).IsCauchy

Lemmas that can be helpful for proving 5.5.4

theorem Chapter5.Real.LIM.abs_eq {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) (h : LIM a = LIM b) : LIM |a| = LIM |b|

theorem Chapter5.Real.LIM.abs_eq_pos {a : ℕ → ℚ} (h : LIM a > 0) (ha : (↑a).IsCauchy) : LIM a = LIM |a|

theorem Chapter5.Real.LIM_abs {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : |LIM a| = LIM |a|

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

theorem Chapter5.Real.LIM_of_Cauchy {q : ℕ → ℚ} (hq : ∀ (M n : ℕ), n ≥ M → ∀ n' ≥ M, |q n - q n'| ≤ 1 / (↑M + 1)) : (↑q).IsCauchy ∧ ∀ (M : ℕ), |↑(q M) - LIM q| ≤ 1 / (↑M + 1)

Exercise 5.5.4

theorem Chapter5.Real.LUB_claim1 (n : ℕ) {E : Set Real} (hE : E.Nonempty) (hbound : BddAbove E) : ∃! m : ℤ, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E

The sequence m₁, m₂, … is well-defined. This proof uses a different indexing convention than the text

theorem Chapter5.Real.LUB_claim2 {E : Set Real} (N : ℕ) {a b : ℕ → ℚ} (hb : ∀ (n : ℕ), b n = 1 / (↑n + 1)) (hm1 : ∀ (n : ℕ), ↑(a n) ∈ upperBounds E) (hm2 : ∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E) (n : ℕ) : n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)

theorem Chapter5.Real.LUB_exist {E : Set Real} (hE : E.Nonempty) (hbound : BddAbove E) : ∃ (S : Real), IsLUB E S

Theorem 5.5.9 (Existence of least upper bound)

inductive Chapter5.ExtendedReal : Type

A bare-bones extended real class to define supremum.

• neg_infty : ExtendedReal
• real (x : Real) : ExtendedReal
• infty : ExtendedReal

@[implicit_reducible]

instance Chapter5.ExtendedReal.inst_Top : Top ExtendedReal

Mathlib prefers ⊤ to denote the +∞ element.

Equations

• Chapter5.ExtendedReal.inst_Top = { top := Chapter5.ExtendedReal.infty }

@[implicit_reducible]

instance Chapter5.ExtendedReal.inst_Bot : Bot ExtendedReal

Mathlib prefers ⊥ to denote the -∞ element.

Equations

• Chapter5.ExtendedReal.inst_Bot = { bot := Chapter5.ExtendedReal.neg_infty }

@[implicit_reducible]

instance Chapter5.ExtendedReal.coe_real : Coe Real ExtendedReal

Equations

• Chapter5.ExtendedReal.coe_real = { coe := fun (x : Chapter5.Real) => Chapter5.ExtendedReal.real x }

@[implicit_reducible]

instance Chapter5.ExtendedReal.real_coe : Coe ExtendedReal Real

Equations

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

@[reducible, inline]

abbrev Chapter5.ExtendedReal.IsFinite (X : ExtendedReal) : Prop

Equations

• Chapter5.ExtendedReal.neg_infty.IsFinite = False
• (Chapter5.ExtendedReal.real x).IsFinite = True
• Chapter5.ExtendedReal.infty.IsFinite = False

theorem Chapter5.ExtendedReal.finite_eq_coe {X : ExtendedReal} (hX : X.IsFinite) : X = real (match X with | neg_infty => 0 | real x => x | infty => 0)

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.sup (E : Set Real) : ExtendedReal

Definition 5.5.10 (Supremum)

Equations

• Chapter5.ExtendedReal.sup E = if h1 : E.Nonempty then if h2 : BddAbove E then Chapter5.ExtendedReal.real ⋯.choose else ⊤ else ⊥

theorem Chapter5.ExtendedReal.sup_of_empty : sup ∅ = ⊥

Definition 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_unbounded {E : Set Real} (hb : ¬BddAbove E) : sup E = ⊤

Definition 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) : IsLUB E (match sup E with | neg_infty => 0 | real x => x | infty => 0)

Definition 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_bounded_finite {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) : (sup E).IsFinite

theorem Chapter5.Real.exist_sqrt_two : ∃ (x : Real), x ^ 2 = 2

Proposition 5.5.12

theorem Chapter5.Real.exist_irrational : ∃ (x : Real), ¬∃ (q : ℚ), x = ↑q

Remark 5.5.13

theorem Chapter5.Real.mem_neg (E : Set Real) (x : Real) : x ∈ -E ↔ -x ∈ E

Helper lemma for Exercise 5.5.1.

theorem Chapter5.Real.inf_neg {E : Set Real} {M : Real} (h : IsLUB E M) : IsGLB (-E) (-M)

Exercise 5.5.1

theorem Chapter5.Real.GLB_exist {E : Set Real} (hE : E.Nonempty) (hbound : BddBelow E) : ∃ (S : Real), IsGLB E S

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.inf (E : Set Real) : ExtendedReal

Equations

• Chapter5.ExtendedReal.inf E = if h1 : E.Nonempty then if h2 : BddBelow E then Chapter5.ExtendedReal.real ⋯.choose else ⊥ else ⊤

theorem Chapter5.ExtendedReal.inf_of_empty : inf ∅ = ⊤

theorem Chapter5.ExtendedReal.inf_of_unbounded {E : Set Real} (hb : ¬BddBelow E) : inf E = ⊥

theorem Chapter5.ExtendedReal.inf_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddBelow E) : IsGLB E (match inf E with | neg_infty => 0 | real x => x | infty => 0)

theorem Chapter5.ExtendedReal.inf_of_bounded_finite {E : Set Real} (hnon : E.Nonempty) (hb : BddBelow E) : (inf E).IsFinite

theorem Chapter5.Real.irrat_between {x y : Real} (hxy : x < y) : ∃ (z : Real), x < z ∧ z < y ∧ ¬∃ (q : ℚ), z = ↑q

Exercise 5.5.5

@[implicit_reducible]

noncomputable instance Chapter5.Real.inst_SupSet : SupSet Real

Equations

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

@[implicit_reducible]

noncomputable instance Chapter5.Real.inst_conditionallyCompleteLattice : ConditionallyCompleteLattice Real

Use the sSup operation to build a conditionally complete lattice structure on Real.

Equations

• Chapter5.Real.inst_conditionallyCompleteLattice = conditionallyCompleteLatticeOfLatticeOfsSup Chapter5.Real ⋯

theorem Chapter5.ExtendedReal.sSup_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) : IsLUB E (sSup E)