Аналіз I, Глава 6.2

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:

• Some API for Mathlib's extended reals EReal, particularly with regard to the supremum operation sSup and infimum operation sInf.

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

Визначення 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)

Визначення 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 = ⊥

Визначення 6.2.3 (Ordering of extended reals)

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

Визначення 6.2.3 (Ordering of extended reals)

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

Твердження 6.2.5(a) / Вправа 6.2.1

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

Твердження 6.2.5(b) / Вправа 6.2.1

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

Твердження 6.2.5(b) / Вправа 6.2.1

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

Твердження 6.2.5(b) / Вправа 6.2.1

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

Твердження 6.2.5(b) / Вправа 6.2.1

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

Твердження 6.2.5(c) / Вправа 6.2.1

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

Твердження 6.2.5(d) / Вправа 6.2.1

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

Визначення 6.2.6

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

Визначення 6.2.6

theorem EReal.sup_of_empty : sSup ∅ = ⊥

Визначення 6.2.6

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

Визначення 6.2.6

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

Визначення 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

Приклад 6.2.7

Equations

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

@[reducible, inline]

abbrev Example_6_2_8 : Set EReal

Приклад 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

Приклад 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

Теорема 6.2.11 (a) / Вправа 6.2.2

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

Теорема 6.2.11 (a) / Вправа 6.2.2

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

Теорема 6.2.11 (b) / Вправа 6.2.2

theorem EReal.inf_ge_upper (E : Set EReal) {M : EReal} (hM : M ∈ upperBounds E) : sInf E ≥ M

Теорема 6.2.11 (c) / Вправа 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 extended reals.

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

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