Аналіз I, Розділ 5, Епілог

In this (technical) epilogue, we show that the "Chapter 5" real numbers Chapter5.Real : TypeChapter5.Real are isomorphic in various standard senses to the standard real numbers ℝ : Typeℝ. This we do by matching both structures with Dedekind cuts of the (Mathlib) rational numbers ℚ : Typeℚ.

From this point onwards, Chapter5.Real : TypeChapter5.Real will be deprecated, and we will use the standard real numbers ℝ : Typeℝ instead. In particular, one should use the full Mathlib API for ℝ : Typeℝ for all subsequent chapters, in lieu of the Chapter5.Real : TypeChapter5.Real API.

Filling the sorries here requires both the Chapter5.Real API and the Mathlib API for the standard natural numbers ℝ : Typeℝ. As such, they are excellent exercises to prepare you for the aforementioned transition.

namespace Chapter5structure DedekindCut where E : Set ℚ nonempty : E.Nonempty bounded : BddAbove E lower: IsLowerSet E nomax : ∀ q ∈ E, ∃ r ∈ E, r > qtheorem isLowerSet_iff (E: Set ℚ) : IsLowerSet E ↔ ∀ q r, r < q → q ∈ E → r ∈ E := isLowerSet_iff_forall_ltabbrev Real.toSet_Rat (x:Real) : Set ℚ := { q | (q:Real) < x }lemma declaration uses 'sorry'Real.toSet_Rat_nonempty (x:Real) : x.toSet_Rat.Nonempty := x:Real⊢ x.toSet_Rat.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_bounded (x:Real) : BddAbove x.toSet_Rat := x:Real⊢ BddAbove x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_lower (x:Real) : IsLowerSet x.toSet_Rat := x:Real⊢ IsLowerSet x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_nomax {x:Real} : ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q := x:Real⊢ ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q All goals completed! 🐙abbrev Real.toCut (x:Real) : DedekindCut := { E := x.toSet_Rat nonempty := x.toSet_Rat_nonempty bounded := x.toSet_Rat_bounded lower := x.toSet_Rat_lower nomax := x.toSet_Rat_nomax }abbrev DedekindCut.toSet_Real (c: DedekindCut) : Set Real := (fun (q:ℚ) ↦ (q:Real)) '' c.Elemma declaration uses 'sorry'DedekindCut.toSet_Real_nonempty (c: DedekindCut) : c.toSet_Real.Nonempty := c:DedekindCut⊢ c.toSet_Real.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'DedekindCut.toSet_Real_bounded (c: DedekindCut) : BddAbove c.toSet_Real := c:DedekindCut⊢ BddAbove c.toSet_Real All goals completed! 🐙noncomputable abbrev DedekindCut.toReal (c: DedekindCut) : Real := sSup c.toSet_Reallemma DedekindCut.toReal_isLUB (c: DedekindCut) : IsLUB c.toSet_Real c.toReal := ExtendedReal.sSup_of_bounded c.toSet_Real_nonempty c.toSet_Real_boundednoncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'Real.equivCut : Real ≃ DedekindCut where toFun := Real.toCut invFun := DedekindCut.toReal left_inv x := x:Real⊢ x.toCut.toReal = x All goals completed! 🐙 right_inv c := c:DedekindCut⊢ c.toReal.toCut = c All goals completed! 🐙end Chapter5

Now to develop analogous results for the Mathlib reals.

abbrev Real.toSet_Rat (x:ℝ) : Set ℚ := { q | (q:ℝ) < x }
lemma declaration uses 'sorry'Real.toSet_Rat_nonempty (x:ℝ) : x.toSet_Rat.Nonempty := x:ℝ⊢ x.toSet_Rat.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_bounded (x:ℝ) : BddAbove x.toSet_Rat := x:ℝ⊢ BddAbove x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_lower (x:ℝ) : IsLowerSet x.toSet_Rat := x:ℝ⊢ IsLowerSet x.toSet_Rat All goals completed! 🐙lemma declaration uses 'sorry'Real.toSet_Rat_nomax (x:ℝ) : ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q := x:ℝ⊢ ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q All goals completed! 🐙abbrev Real.toCut (x:ℝ) : Chapter5.DedekindCut := { E := x.toSet_Rat nonempty := x.toSet_Rat_nonempty bounded := x.toSet_Rat_bounded lower := x.toSet_Rat_lower nomax := x.toSet_Rat_nomax }namespace Chapter5abbrev DedekindCut.toSet_R (c: DedekindCut) : Set ℝ := (fun (q:ℚ) ↦ (q:ℝ)) '' c.Elemma declaration uses 'sorry'DedekindCut.toSet_R_nonempty (c: DedekindCut) : c.toSet_R.Nonempty := c:DedekindCut⊢ c.toSet_R.Nonempty All goals completed! 🐙lemma declaration uses 'sorry'DedekindCut.toSet_R_bounded (c: DedekindCut) : BddAbove c.toSet_R := c:DedekindCut⊢ BddAbove c.toSet_R All goals completed! 🐙noncomputable abbrev DedekindCut.toR (c: DedekindCut) : ℝ := sSup c.toSet_Rlemma DedekindCut.toR_isLUB (c: DedekindCut) : IsLUB c.toSet_R c.toR := isLUB_csSup c.toSet_R_nonempty c.toSet_R_boundedend Chapter5noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'Real.equivCut : ℝ ≃ Chapter5.DedekindCut where toFun := _root_.Real.toCut invFun := Chapter5.DedekindCut.toR left_inv x := x:ℝ⊢ x.toCut.toR = x All goals completed! 🐙 right_inv c := c:Chapter5.DedekindCut⊢ c.toR.toCut = c All goals completed! 🐙namespace Chapter5

The isomorphism between the Chapter 5 reals and the Mathlib reals.

noncomputable abbrev Real.equivR : Real ≃ ℝ := Real.equivCut.trans _root_.Real.equivCut.symm
lemma Real.equivR_iff (x : Real) (y : ℝ) : y = Real.equivR x ↔ y.toCut = x.toCut := x:Realy:ℝ⊢ y = equivR x ↔ y.toCut = x.toCut x:Realy:ℝ⊢ _root_.Real.equivCut y = equivCut x ↔ y.toCut = x.toCut All goals completed! 🐙

The isomorphism preserves order and ring operations

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.equivR_ordered_ring : Real ≃+*o ℝ where toEquiv := equivR map_add' := ⊢ ∀ (x y : Real), equivR.toFun (x + y) = equivR.toFun x + equivR.toFun y All goals completed! 🐙 map_mul' := ⊢ ∀ (x y : Real), equivR.toFun (x * y) = equivR.toFun x * equivR.toFun y All goals completed! 🐙 map_le_map_iff' := ⊢ ∀ {a b : Real}, equivR.toFun a ≤ equivR.toFun b ↔ a ≤ b All goals completed! 🐙
end Chapter5