Аналіз I, Розділ 6.2: Розширена система дійсних чисел

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Інтерфейс (API) для розширених дійсних Mathlib EReal, зокрема щодо операцій супремуму sSup та інфімуму 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 (Негація розширених дійсних)

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

Визначення 6.2.3 (Порядок на розширених дійсних)

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

Визначення 6.2.3 (Порядок на розширених дійсних)

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) : sInf E ≤ x

Теорема 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 ∈ lowerBounds E) : sInf E ≥ M

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

@[reducible, inline]

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

Не в підручнику: ототожнення розширених дійсних Розділу 5 із EReal з Mathlib.

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.