structure Chapter5.DedekindCut : Type

• E : Set ℚ
• nonempty : self.E.Nonempty
• bounded : BddAbove self.E
• lower : IsLowerSet self.E
• nomax (q : ℚ) : q ∈ self.E → ∃ r ∈ self.E, r > q

theorem Chapter5.DedekindCut.ext_iff {x y : DedekindCut} : x = y ↔ x.E = y.E

theorem Chapter5.DedekindCut.ext {x y : DedekindCut} (E : x.E = y.E) : x = y

theorem Chapter5.isLowerSet_iff (E : Set ℚ) : IsLowerSet E ↔ ∀ (q r : ℚ), r < q → q ∈ E → r ∈ E

@[reducible, inline]

abbrev Chapter5.Real.toSet_Rat (x : Real) : Set ℚ

Equations

• x.toSet_Rat = {q : ℚ | ↑q < x}

theorem Chapter5.Real.toSet_Rat_nonempty (x : Real) : x.toSet_Rat.Nonempty

theorem Chapter5.Real.toSet_Rat_bounded (x : Real) : BddAbove x.toSet_Rat

theorem Chapter5.Real.toSet_Rat_lower (x : Real) : IsLowerSet x.toSet_Rat

theorem Chapter5.Real.toSet_Rat_nomax {x : Real} (q : ℚ) : q ∈ x.toSet_Rat → ∃ r ∈ x.toSet_Rat, r > q

@[reducible, inline]

abbrev Chapter5.Real.toCut (x : Real) : DedekindCut

Equations

• x.toCut = { E := x.toSet_Rat, nonempty := ⋯, bounded := ⋯, lower := ⋯, nomax := ⋯ }

@[reducible, inline]

abbrev Chapter5.DedekindCut.toSet_Real (c : DedekindCut) : Set Real

Equations

• c.toSet_Real = (fun (q : ℚ) => ↑q) '' c.E

theorem Chapter5.DedekindCut.toSet_Real_nonempty (c : DedekindCut) : c.toSet_Real.Nonempty

theorem Chapter5.DedekindCut.toSet_Real_bounded (c : DedekindCut) : BddAbove c.toSet_Real

@[reducible, inline]

noncomputable abbrev Chapter5.DedekindCut.toReal (c : DedekindCut) : Real

Equations

• c.toReal = sSup c.toSet_Real

theorem Chapter5.DedekindCut.toReal_isLUB (c : DedekindCut) : IsLUB c.toSet_Real c.toReal

@[reducible, inline]

noncomputable abbrev Chapter5.Real.equivCut : Real ≃ DedekindCut

Equations

• Chapter5.Real.equivCut = { toFun := Chapter5.Real.toCut, invFun := Chapter5.DedekindCut.toReal, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

abbrev Real.toSet_Rat (x : ℝ) : Set ℚ

Now to develop analogous results for the Mathlib reals.

Equations

• x.toSet_Rat = {q : ℚ | ↑q < x}

theorem Real.toSet_Rat_nonempty (x : ℝ) : x.toSet_Rat.Nonempty

theorem Real.toSet_Rat_bounded (x : ℝ) : BddAbove x.toSet_Rat

theorem Real.toSet_Rat_lower (x : ℝ) : IsLowerSet x.toSet_Rat

theorem Real.toSet_Rat_nomax (x : ℝ) (q : ℚ) : q ∈ x.toSet_Rat → ∃ r ∈ x.toSet_Rat, r > q

@[reducible, inline]

abbrev Real.toCut (x : ℝ) : Chapter5.DedekindCut

Equations

• x.toCut = { E := x.toSet_Rat, nonempty := ⋯, bounded := ⋯, lower := ⋯, nomax := ⋯ }

@[reducible, inline]

abbrev Chapter5.DedekindCut.toSet_R (c : DedekindCut) : Set ℝ

Equations

• c.toSet_R = (fun (q : ℚ) => ↑q) '' c.E

theorem Chapter5.DedekindCut.toSet_R_nonempty (c : DedekindCut) : c.toSet_R.Nonempty

theorem Chapter5.DedekindCut.toSet_R_bounded (c : DedekindCut) : BddAbove c.toSet_R

@[reducible, inline]

noncomputable abbrev Chapter5.DedekindCut.toR (c : DedekindCut) : ℝ

Equations

• c.toR = sSup c.toSet_R

theorem Chapter5.DedekindCut.toR_isLUB (c : DedekindCut) : IsLUB c.toSet_R c.toR

@[reducible, inline]

noncomputable abbrev Real.equivCut : ℝ ≃ Chapter5.DedekindCut

Equations

• Real.equivCut = { toFun := Real.toCut, invFun := Chapter5.DedekindCut.toR, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter5.Real.equivR : Real ≃ ℝ

The isomorphism between the Chapter5.Real numbers and the Mathlib reals.

Equations

• Chapter5.Real.equivR = Chapter5.Real.equivCut.trans Real.equivCut.symm

theorem Chapter5.Real.equivR_iff (x : Real) (y : ℝ) : y = equivR x ↔ y.toCut = x.toCut

theorem Chapter5.Real.equivR_ratCast {q : ℚ} : equivR ↑q = ↑q

theorem Chapter5.Real.equivR_nat {n : ℕ} : equivR ↑n = ↑n

theorem Chapter5.Real.equivR_int {n : ℤ} : equivR ↑n = ↑n

theorem Chapter5.Sequence.IsCauchy.to_IsCauSeq {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : IsCauSeq _root_.abs a

@[reducible, inline]

abbrev Chapter5.Sequence.IsCauchy.CauSeq {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : _root_.CauSeq ℚ _root_.abs

Equations

• x✝.CauSeq = ⟨a, ⋯⟩

theorem Chapter5.Sequence.Equiv.LimZero {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) (h : Equiv a b) : (ha.CauSeq - hb.CauSeq).LimZero

theorem Chapter5.Real.mk_eq_mk {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) (hab : Sequence.Equiv a b) : Real.mk ha.CauSeq = Real.mk hb.CauSeq

theorem Chapter5.Sequence.Equiv_iff_LimZero {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : Equiv a b ↔ (ha.CauSeq - hb.CauSeq).LimZero

theorem Chapter5.Sequence.difference_approaches_zero {a : ℕ → ℚ} (ha : (↑a).IsCauchy) (ε : ℚ) : ε > 0 → ∃ (N : ℕ), ∀ n ≥ N, |LIM a - ↑(a n)| ≤ ↑ε

theorem Chapter5.Real.exists_equiv_above {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : ∃ (b : ℕ → ℚ), (↑b).IsCauchy ∧ Sequence.Equiv a b ∧ ∀ (n : ℕ), LIM a ≤ ↑(b n)

theorem Chapter5.Real.exists_equiv_below {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : ∃ (b : ℕ → ℚ), (↑b).IsCauchy ∧ Sequence.Equiv a b ∧ ∀ (n : ℕ), ↑(b n) ≤ LIM a

theorem Chapter5.Real.equivR_eq' {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : equivR (LIM a) = Real.mk ha.CauSeq

theorem Chapter5.Real.equivR_eq (x : Real) : ∃ (a : ℕ → ℚ) (ha : (↑a).IsCauchy), x = LIM a ∧ equivR x = Real.mk ha.CauSeq

@[reducible, inline]

noncomputable abbrev Chapter5.Real.equivR_ordered_ring : Real ≃+*o ℝ

The isomorphism preserves order and ring operations.

Equations

• Chapter5.Real.equivR_ordered_ring = { toEquiv := Chapter5.Real.equivR, map_mul' := ⋯, map_add' := ⋯, map_le_map_iff' := ⋯ }

theorem Chapter5.Real.equivR_map_mul {x y : Real} : equivR (x * y) = equivR x * equivR y

theorem Chapter5.Real.equivR_map_inv {x : Real} : equivR x⁻¹ = (equivR x)⁻¹

theorem Chapter5.Real.equivR_map_pos {x : Real} : 0 < x ↔ 0 < equivR x

theorem Chapter5.Real.equivR_map_nonneg {x : Real} : 0 ≤ x ↔ 0 ≤ equivR x

theorem Chapter5.Real.pow_of_equivR (x : Real) (n : ℕ) : equivR (x ^ n) = equivR x ^ n

theorem Chapter5.Real.zpow_of_equivR (x : Real) (n : ℤ) : equivR (x ^ n) = equivR x ^ n

theorem Chapter5.Real.ratPow_of_equivR (x : Real) (q : ℚ) (hx : x > 0) : equivR (x ^ q) = equivR x ^ ↑q