theorem EReal.def (x : EReal) : (∃ (y : ℝ), ↑y = x) ∨ x = ⊤ ∨ x = ⊥

Definition 6.2.1

theorem EReal.real_neq_infty (x : ℝ) : ↑x ≠ ⊤

theorem EReal.real_neq_neg_infty (x : ℝ) : ↑x ≠ ⊥

theorem EReal.infty_neq_neg_infty : ⊤ ≠ ⊥

@[reducible, inline]

abbrev EReal.IsFinite (x : EReal) : Prop

Equations

• x.IsFinite = ∃ (y : ℝ), ↑y = x

@[reducible, inline]

abbrev EReal.IsInfinite (x : EReal) : Prop

Equations

• x.IsInfinite = (x = ⊤ ∨ x = ⊥)

theorem EReal.infinite_iff_not_finite (x : EReal) : x.IsInfinite ↔ ¬x.IsFinite

theorem EReal.neg_of_real (x : ℝ) : -↑x = ↑(-x)

Definition 6.2.2 (Negation of extended reals)

theorem EReal.le_iff (x y : EReal) : x ≤ y ↔ (∃ (x' : ℝ) (y' : ℝ), x = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ x = ⊥

Definition 6.2.3 (Ordering of extended reals)

theorem EReal.lt_iff (x y : EReal) : x < y ↔ x ≤ y ∧ x ≠ y

Definition 6.2.3 (Ordering of extended reals)

theorem EReal.refl (x : EReal) : x ≤ x

Proposition 6.2.5(a) / Exercise 6.2.1

theorem EReal.trichotomy (x y : EReal) : x < y ∨ x = y ∨ x > y

Proposition 6.2.5(b) / Exercise 6.2.1

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

Proposition 6.2.5(b') / Exercise 6.2.1

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

Proposition 6.2.5(b'') / Exercise 6.2.1

theorem EReal.not_lt_and_gt (x y : EReal) : ¬(x < y ∧ x > y)

Proposition 6.2.5(b''') / Exercise 6.2.1

theorem EReal.trans {x y z : EReal} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z

Proposition 6.2.5(c) / Exercise 6.2.1

theorem EReal.neg_of_lt {x y : EReal} (hxy : x ≤ y) : -y ≤ -x

Proposition 6.2.5(d) / Exercise 6.2.1

theorem EReal.sup_of_bounded_nonempty {E : Set ℝ} (hbound : BddAbove E) (hnon : E.Nonempty) : sSup ((fun (x : ℝ) => ↑x) '' E) = ↑(sSup E)

Definition 6.2.6

theorem EReal.sup_of_unbounded_nonempty {E : Set ℝ} (hunbound : ¬BddAbove E) (hnon : E.Nonempty) : sSup ((fun (x : ℝ) => ↑x) '' E) = ⊤

Definition 6.2.6

theorem EReal.sup_of_empty : sSup ∅ = ⊥

Definition 6.2.6

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

Definition 6.2.6

theorem EReal.sup_of_neg_infty_mem {E : Set EReal} : sSup E = sSup (E \ {⊥})

Definition 6.2.6

theorem EReal.inf_eq_neg_sup (E : Set EReal) : sInf E = -sSup (-E)

@[reducible, inline]

abbrev Example_6_2_7 : Set EReal

Example 6.2.7

Equations

• Example_6_2_7 = {x : EReal | ∃ (n : ℕ), x = -(↑n + 1)} ∪ {⊥}

@[reducible, inline]

abbrev Example_6_2_8 : Set EReal

Example 6.2.8

Equations

• Example_6_2_8 = {x : EReal | ∃ (n : ℕ), x = ↑(1 - 10 ^ (-↑n - 1))}

@[reducible, inline]

abbrev Example_6_2_9 : Set EReal

Example 6.2.9

Equations

• Example_6_2_9 = {x : EReal | ∃ (n : ℕ), x = ↑n + 1}

theorem EReal.mem_le_sup (E : Set EReal) {x : EReal} (hx : x ∈ E) : x ≤ sSup E

Theorem 6.2.11 (a) / Exercise 6.2.2

theorem EReal.mem_ge_inf (E : Set EReal) {x : EReal} (hx : x ∈ E) : sInf E ≤ x

Theorem 6.2.11 (a') / Exercise 6.2.2

theorem EReal.sup_le_upper (E : Set EReal) {M : EReal} (hM : M ∈ upperBounds E) : sSup E ≤ M

Theorem 6.2.11 (b) / Exercise 6.2.2

theorem EReal.inf_ge_lower (E : Set EReal) {M : EReal} (hM : M ∈ lowerBounds E) : sInf E ≥ M

Theorem 6.2.11 (c) / Exercise 6.2.2

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.toEReal (x : ExtendedReal) : EReal

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

Equations

• (Chapter5.ExtendedReal.real r).toEReal = ↑(Chapter5.Real.equivR r)
• Chapter5.ExtendedReal.infty.toEReal = ⊤
• Chapter5.ExtendedReal.neg_infty.toEReal = ⊥

theorem Chapter5.ExtendedReal.coe_inj : Function.Injective toEReal

theorem Chapter5.ExtendedReal.coe_surj : Function.Surjective toEReal

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.equivEReal : ExtendedReal ≃ EReal

Equations

• Chapter5.ExtendedReal.equivEReal = { toFun := Chapter5.ExtendedReal.toEReal, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }