Analysis I, Section 6.2: The extended real number system

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:

open EReal

Definition 6.2.1

theorem EReal.def (x:EReal) : (∃ (y:Real), y = x) ∨ x = ⊤ ∨ x = ⊥ := x:EReal⊢ (∃ y, ↑y = x) ∨ x = ⊤ ∨ x = ⊥ ⊢ ∀ (x : EReal), (∃ y, ↑y = x) ∨ x = ⊤ ∨ x = ⊥ All goals completed! 🐙
theorem EReal.real_neq_infty (x:ℝ) : (x:EReal) ≠ ⊤ := coe_ne_top _theorem EReal.real_neq_neg_infty (x:ℝ) : (x:EReal) ≠ ⊥ := coe_ne_bot _theorem EReal.infty_neq_neg_infty : (⊤:EReal) ≠ (⊥:EReal) := add_top_iff_ne_bot.mp rflabbrev EReal.IsFinite (x:EReal) : Prop := ∃ (y:Real), y = xabbrev EReal.IsInfinite (x:EReal) : Prop := x = ⊤ ∨ x = ⊥theorem EReal.infinite_iff_not_finite (x:EReal): x.IsInfinite ↔ ¬ x.IsFinite := x:EReal⊢ x.IsInfinite ↔ ¬x.IsFinite y:ℝ⊢ (↑y).IsInfinite ↔ ¬(↑y).IsFinite⊢ ⊤.IsInfinite ↔ ¬⊤.IsFinite⊢ ⊥.IsInfinite ↔ ¬⊥.IsFinite y:ℝ⊢ (↑y).IsInfinite ↔ ¬(↑y).IsFinite⊢ ⊤.IsInfinite ↔ ¬⊤.IsFinite⊢ ⊥.IsInfinite ↔ ¬⊥.IsFinite All goals completed! 🐙

Definition 6.2.2 (Negation of extended reals)

theorem EReal.neg_of_real (x:Real) : -(x:EReal) = (-x:ℝ) := rfl
EReal.neg_top : -⊤ = ⊥
EReal.neg_bot : -⊥ = ⊤

Definition 6.2.3 (Ordering of extended reals)

theorem EReal.le_iff (x y:EReal) : x ≤ y ↔ (∃ (x' y':Real), x = x' ∧ y = y' ∧ x' ≤ y') ∨ y = ⊤ ∨ x = ⊥ := x:ERealy:EReal⊢ x ≤ y ↔ (∃ x' y', x = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ x = ⊥ y:ERealx':ℝ⊢ ↑x' ≤ y ↔ (∃ x'_1 y', ↑x' = ↑x'_1 ∧ y = ↑y' ∧ x'_1 ≤ y') ∨ y = ⊤ ∨ ↑x' = ⊥y:EReal⊢ ⊤ ≤ y ↔ (∃ x' y', ⊤ = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ ⊤ = ⊥y:EReal⊢ ⊥ ≤ y ↔ (∃ x' y', ⊥ = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ ⊥ = ⊥ y:ERealx':ℝ⊢ ↑x' ≤ y ↔ (∃ x'_1 y', ↑x' = ↑x'_1 ∧ y = ↑y' ∧ x'_1 ≤ y') ∨ y = ⊤ ∨ ↑x' = ⊥y:EReal⊢ ⊤ ≤ y ↔ (∃ x' y', ⊤ = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ ⊤ = ⊥y:EReal⊢ ⊥ ≤ y ↔ (∃ x' y', ⊥ = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ ⊥ = ⊥ y':ℝ⊢ ⊥ ≤ ↑y' ↔ (∃ x' y'_1, ⊥ = ↑x' ∧ ↑y' = ↑y'_1 ∧ x' ≤ y'_1) ∨ ↑y' = ⊤ ∨ ⊥ = ⊥⊢ ⊥ ≤ ⊤ ↔ (∃ x' y', ⊥ = ↑x' ∧ ⊤ = ↑y' ∧ x' ≤ y') ∨ ⊤ = ⊤ ∨ ⊥ = ⊥⊢ ⊥ ≤ ⊥ ↔ (∃ x' y', ⊥ = ↑x' ∧ ⊥ = ↑y' ∧ x' ≤ y') ∨ ⊥ = ⊤ ∨ ⊥ = ⊥ x':ℝy':ℝ⊢ ↑x' ≤ ↑y' ↔ (∃ x'_1 y'_1, ↑x' = ↑x'_1 ∧ ↑y' = ↑y'_1 ∧ x'_1 ≤ y'_1) ∨ ↑y' = ⊤ ∨ ↑x' = ⊥x':ℝ⊢ ↑x' ≤ ⊤ ↔ (∃ x'_1 y', ↑x' = ↑x'_1 ∧ ⊤ = ↑y' ∧ x'_1 ≤ y') ∨ ⊤ = ⊤ ∨ ↑x' = ⊥x':ℝ⊢ ↑x' ≤ ⊥ ↔ (∃ x'_1 y', ↑x' = ↑x'_1 ∧ ⊥ = ↑y' ∧ x'_1 ≤ y') ∨ ⊥ = ⊤ ∨ ↑x' = ⊥y':ℝ⊢ ⊤ ≤ ↑y' ↔ (∃ x' y'_1, ⊤ = ↑x' ∧ ↑y' = ↑y'_1 ∧ x' ≤ y'_1) ∨ ↑y' = ⊤ ∨ ⊤ = ⊥⊢ ⊤ ≤ ⊤ ↔ (∃ x' y', ⊤ = ↑x' ∧ ⊤ = ↑y' ∧ x' ≤ y') ∨ ⊤ = ⊤ ∨ ⊤ = ⊥⊢ ⊤ ≤ ⊥ ↔ (∃ x' y', ⊤ = ↑x' ∧ ⊥ = ↑y' ∧ x' ≤ y') ∨ ⊥ = ⊤ ∨ ⊤ = ⊥y':ℝ⊢ ⊥ ≤ ↑y' ↔ (∃ x' y'_1, ⊥ = ↑x' ∧ ↑y' = ↑y'_1 ∧ x' ≤ y'_1) ∨ ↑y' = ⊤ ∨ ⊥ = ⊥⊢ ⊥ ≤ ⊤ ↔ (∃ x' y', ⊥ = ↑x' ∧ ⊤ = ↑y' ∧ x' ≤ y') ∨ ⊤ = ⊤ ∨ ⊥ = ⊥⊢ ⊥ ≤ ⊥ ↔ (∃ x' y', ⊥ = ↑x' ∧ ⊥ = ↑y' ∧ x' ≤ y') ∨ ⊥ = ⊤ ∨ ⊥ = ⊥ All goals completed! 🐙

Definition 6.2.3 (Ordering of extended reals)

theorem EReal.lt_iff (x y:EReal) : x < y ↔ x ≤ y ∧ x ≠ y := lt_iff_le_and_ne
EReal.coe_lt_coe_iff {x y : ℝ} : ↑x < ↑y ↔ x < y

Examples 6.2.4

example : (3:EReal) ≤ (5:EReal) := ⊢ 3 ≤ 5 ⊢ (∃ x' y', 3 = ↑x' ∧ 5 = ↑y' ∧ x' ≤ y') ∨ 5 = ⊤ ∨ 3 = ⊥; ⊢ ∃ x' y', 3 = ↑x' ∧ 5 = ↑y' ∧ x' ≤ y'; ⊢ 3 = ↑3 ∧ 5 = ↑5 ∧ 3 ≤ 5; All goals completed! 🐙

Examples 6.2.4

example : (3:EReal) < ⊤ := ⊢ 3 < ⊤ ⊢ ¬3 = ⊤; All goals completed! 🐙

Examples 6.2.4

example : (⊥:EReal) < ⊤ := ⊢ ⊥ < ⊤ All goals completed! 🐙

Examples 6.2.4

example : ¬ (3:EReal) ≤ ⊥ := ⊢ ¬3 ≤ ⊥ h:3 ≤ ⊥⊢ False h:3 = ⊥⊢ False All goals completed! 🐙
instCompleteLinearOrderEReal : CompleteLinearOrder EReal

Proposition 6.2.5(a) / Exercise 6.2.1

theorem declaration uses 'sorry'EReal.refl (x:EReal) : x ≤ x := x:EReal⊢ x ≤ x All goals completed! 🐙

Proposition 6.2.5(b) / Exercise 6.2.1

theorem declaration uses 'sorry'EReal.trichotomy (x y:EReal) : x < y ∨ x = y ∨ x > y := x:ERealy:EReal⊢ x < y ∨ x = y ∨ x > y All goals completed! 🐙

Proposition 6.2.5(b) / Exercise 6.2.1

theorem declaration uses 'sorry'EReal.not_lt_and_eq (x y:EReal) : ¬ (x < y ∧ x = y) := x:ERealy:EReal⊢ ¬(x < y ∧ x = y) All goals completed! 🐙

Proposition 6.2.5(b) / Exercise 6.2.1

theorem declaration uses 'sorry'EReal.not_gt_and_eq (x y:EReal) : ¬ (x > y ∧ x = y) := x:ERealy:EReal⊢ ¬(x > y ∧ x = y) All goals completed! 🐙

Proposition 6.2.5(b) / Exercise 6.2.1

theorem declaration uses 'sorry'EReal.not_lt_and_gt (x y:EReal) : ¬ (x < y ∧ x > y) := x:ERealy:EReal⊢ ¬(x < y ∧ x > y) All goals completed! 🐙

Proposition 6.2.5(c) / Exercise 6.2.1

theorem declaration uses 'sorry'EReal.trans {x y z:EReal} (hxy : x ≤ y) (hyz: y ≤ z) : x ≤ z := x:ERealy:ERealz:ERealhxy:x ≤ yhyz:y ≤ z⊢ x ≤ z All goals completed! 🐙

Proposition 6.2.5(d) / Exercise 6.2.1

theorem declaration uses 'sorry'EReal.neg_of_lt {x y:EReal} (hxy : x ≤ y): -y ≤ -x := x:ERealy:ERealhxy:x ≤ y⊢ -y ≤ -x All goals completed! 🐙

Definition 6.2.6

theorem EReal.sup_of_bounded_nonempty {E: Set ℝ} (hbound: BddAbove E) (hnon: E.Nonempty) : sSup ((fun (x:ℝ) ↦ (x:EReal)) '' E) = sSup E := calc _ = sSup ((fun (x:WithTop ℝ) ↦ (x:WithBot (WithTop ℝ))) '' ((fun (x:ℝ) ↦ (x:WithTop ℝ)) '' E)) := E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = sSup ((fun x => ↑x) '' ((fun x => ↑x) '' E)) E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = sSup (((fun x => ↑x) ∘ fun x => ↑x) '' E); All goals completed! 🐙 _ = sSup ((fun (x:ℝ) ↦ (x:WithTop ℝ)) '' E) := E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' ((fun x => ↑x) '' E)) = ↑(sSup ((fun x => ↑x) '' E)) E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ↑(sSup ((fun x => ↑x) '' E)) = sSup ((fun x => ↑x) '' ((fun x => ↑x) '' E)); E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ((fun x => ↑x) '' E).NonemptyE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ BddAbove ((fun x => ↑x) '' E) E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ((fun x => ↑x) '' E).Nonempty All goals completed! 🐙 All goals completed! 🐙 _ = ((sSup E : ℝ) : WithTop ℝ) := E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ↑(sSup ((fun x => ↑x) '' E)) = ↑↑(sSup E) E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = ↑(sSup E); E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ↑(sSup E) = sSup ((fun x => ↑x) '' E); All goals completed! 🐙 _ = _ := rfl

Definition 6.2.6

theorem EReal.sup_of_unbounded_nonempty {E: Set ℝ} (hunbound: ¬ BddAbove E) (hnon: E.Nonempty) : sSup ((fun (x:ℝ) ↦ (x:EReal)) '' E) = ⊤ := E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = ⊤ E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonempty⊢ ∀ b < ⊤, ∃ a ∈ (fun x => ↑x) '' E, b < a E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyb:ERealhb:b < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, b < a E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyy:ℝhb:↑y < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ↑y < aE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyhb:⊤ < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ⊤ < aE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyhb:⊥ < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ⊥ < a E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyy:ℝhb:↑y < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ↑y < a E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyy:ℝhb:↑y < ⊤⊢ ∃ a ∈ E, y < a; E:Set ℝhnon:E.Nonemptyy:ℝhb:↑y < ⊤hunbound:∀ a ∈ E, a ≤ y⊢ BddAbove E; All goals completed! 🐙 E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyhb:⊤ < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ⊤ < a All goals completed! 🐙 All goals completed! 🐙

Definition 6.2.6

theorem EReal.sup_of_empty : sSup (∅:Set EReal) = ⊥ := sSup_empty

Definition 6.2.6

theorem EReal.sup_of_infty_mem {E: Set EReal} (hE: ⊤ ∈ E) : sSup E = ⊤ := csSup_eq_top_of_top_mem hE

Definition 6.2.6

theorem EReal.sup_of_neg_infty_mem {E: Set EReal} : sSup E = sSup (E \ {⊥}) := (sSup_diff_singleton_bot _).symm
theorem EReal.inf_eq_neg_sup (E: Set EReal) : sInf E = - sSup (-E) := E:Set EReal⊢ sInf E = -sSup (-E) E:Set EReal⊢ ∀ (b : EReal), sSup (-E) ≤ -b ↔ b ∈ lowerBounds E E:Set ERealb:EReal⊢ sSup (-E) ≤ -b ↔ b ∈ lowerBounds E E:Set ERealb:EReal⊢ (∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b) ↔ ∀ ⦃a : EReal⦄, a ∈ E → b ≤ a E:Set ERealb:EReal⊢ (∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b) → ∀ ⦃a : EReal⦄, a ∈ E → b ≤ aE:Set ERealb:EReal⊢ (∀ ⦃a : EReal⦄, a ∈ E → b ≤ a) → ∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b E:Set ERealb:EReal⊢ (∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b) → ∀ ⦃a : EReal⦄, a ∈ E → b ≤ a E:Set ERealb:ERealh:∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -ba:ERealha:a ∈ E⊢ b ≤ a; specialize h (-a) (E:Set ERealb:ERealh:∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -ba:ERealha:a ∈ E⊢ - -a ∈ E All goals completed! 🐙); All goals completed! 🐙 All goals completed! 🐙

Example 6.2.7

abbrev Example_6_2_7 : Set EReal := { x | ∃ n:ℕ, x = -((n+1):EReal)} ∪ {⊥}
declaration uses 'sorry'example : sSup Example_6_2_7 = -1 := ⊢ sSup Example_6_2_7 = -1 ⊢ sSup (Example_6_2_7 \ {⊥}) = -1 All goals completed! 🐙declaration uses 'sorry'example : sInf Example_6_2_7 = ⊥ := ⊢ sInf Example_6_2_7 = ⊥ ⊢ -sSup (-Example_6_2_7) = ⊥ All goals completed! 🐙

Example 6.2.8

abbrev Example_6_2_8 : Set EReal := { x | ∃ n:ℕ, x = (1 - (10:ℝ)^(-(n:ℤ)-1):Real)}
declaration uses 'sorry'example : sInf Example_6_2_8 = (0.9:ℝ) := ⊢ sInf Example_6_2_8 = ↑0.9 All goals completed! 🐙declaration uses 'sorry'example : sSup Example_6_2_8 = 1 := ⊢ sSup Example_6_2_8 = 1 All goals completed! 🐙

Example 6.2.9

abbrev Example_6_2_9 : Set EReal := { x | ∃ n:ℕ, x = n+1}
declaration uses 'sorry'example : sInf Example_6_2_9 = 1 := ⊢ sInf Example_6_2_9 = 1 All goals completed! 🐙declaration uses 'sorry'example : sSup Example_6_2_9 = ⊤ := ⊢ sSup Example_6_2_9 = ⊤ All goals completed! 🐙declaration uses 'sorry'example : sInf (∅ : Set EReal) = ⊤ := ⊢ sInf ∅ = ⊤ All goals completed! 🐙declaration uses 'sorry'example (E: Set EReal) : sSup E < sInf E ↔ E = ∅ := E:Set EReal⊢ sSup E < sInf E ↔ E = ∅ All goals completed! 🐙

Theorem 6.2.11 (a) / Exercise 6.2.2

theorem declaration uses 'sorry'EReal.mem_le_sup (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sSup E := E:Set ERealx:ERealhx:x ∈ E⊢ x ≤ sSup E All goals completed! 🐙

Theorem 6.2.11 (a) / Exercise 6.2.2

theorem declaration uses 'sorry'EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sInf E := E:Set ERealx:ERealhx:x ∈ E⊢ x ≤ sInf E All goals completed! 🐙

Theorem 6.2.11 (b) / Exercise 6.2.2

theorem declaration uses 'sorry'EReal.sup_le_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sSup E ≤ M := E:Set ERealM:ERealhM:M ∈ upperBounds E⊢ sSup E ≤ M All goals completed! 🐙

Theorem 6.2.11 (c) / Exercise 6.2.2

theorem declaration uses 'sorry'EReal.inf_ge_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sInf E ≥ M := E:Set ERealM:ERealhM:M ∈ upperBounds E⊢ sInf E ≥ M All goals completed! 🐙
isLUB_iff_sSup_eq.{u_1} {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a ↔ sSup s = a
isGLB_iff_sInf_eq.{u_1} {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : IsGLB s a ↔ sInf s = a

Not in textbook: identify the Chapter 5 extended reals with the Mathlib extended reals.

noncomputable abbrev Chapter5.ExtendedReal.toEReal (x:ExtendedReal) : EReal := match x with | real r => ((Real.equivR r):EReal) | infty => ⊤ | neg_infty => ⊥
theorem declaration uses 'sorry'Chapter5.ExtendedReal.coe_inj : Function.Injective toEReal := ⊢ Function.Injective toEReal All goals completed! 🐙theorem declaration uses 'sorry'Chapter5.ExtendedReal.coe_surj : Function.Surjective toEReal := ⊢ Function.Surjective toEReal All goals completed! 🐙noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Chapter5.ExtendedReal.equivEReal : Chapter5.ExtendedReal ≃ EReal where toFun := toEReal invFun := sorry left_inv x := x:ExtendedReal⊢ sorry x.toEReal = x All goals completed! 🐙 right_inv x := x:EReal⊢ (sorry x).toEReal = x All goals completed! 🐙