@[reducible, inline]

abbrev Real.Close (ε x y : ℝ) : Prop

Equations

• ε.Close x y = (dist x y ≤ ε)

theorem Real.close_def (ε x y : ℝ) : ε.Close x y ↔ dist x y ≤ ε

Definition 6.1.2 (ε-close). This is similar to the previous notion of ε-closeness, but where all quantities are real instead of rational.

structure Chapter6.Sequence : Type

Definition 6.1.3 (Sequence). This is similar to the Chapter 5 sequence, except that now the sequence is real-valued. As with Chapter 5, we start sequences from 0 by default.

• m : ℤ
• seq : ℤ → ℝ
• vanish (n : ℤ) : n < self.m → self.seq n = 0

theorem Chapter6.Sequence.ext_iff {x y : Sequence} : x = y ↔ x.m = y.m ∧ x.seq = y.seq

theorem Chapter6.Sequence.ext {x y : Sequence} (m : x.m = y.m) (seq : x.seq = y.seq) : x = y

@[implicit_reducible]

instance Chapter6.Sequence.instCoeFun : CoeFun Sequence fun (x : Sequence) => ℤ → ℝ

Sequences can be thought of as functions from ℤ to ℝ.

Equations

• Chapter6.Sequence.instCoeFun = { coe := fun (a : Chapter6.Sequence) => a.seq }

@[reducible, inline]

abbrev Chapter6.Sequence.ofNatFun (a : ℕ → ℝ) : Sequence

Equations

• ↑a = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }

@[implicit_reducible]

instance Chapter6.Sequence.instCoe : Coe (ℕ → ℝ) Sequence

Functions from ℕ to ℝ can be thought of as sequences.

Equations

• Chapter6.Sequence.instCoe = { coe := Chapter6.Sequence.ofNatFun }

@[reducible, inline]

abbrev Chapter6.Sequence.mk' (m : ℤ) (a : { n : ℤ // n ≥ m } → ℝ) : Sequence

Equations

• Chapter6.Sequence.mk' m a = { m := m, seq := fun (n : ℤ) => if h : n ≥ m then a ⟨n, h⟩ else 0, vanish := ⋯ }

theorem Chapter6.Sequence.eval_mk {n m : ℤ} (a : { n : ℤ // n ≥ m } → ℝ) (h : n ≥ m) : (mk' m a).seq n = a ⟨n, h⟩

@[simp]

theorem Chapter6.Sequence.eval_coe (n : ℕ) (a : ℕ → ℝ) : (↑a).seq ↑n = a n

@[reducible, inline]

abbrev Chapter6.Sequence.from (a : Sequence) (m₁ : ℤ) : Sequence

a.from n₁ starts a : Sequence from n₁. It is intended for use when n₁ ≥ n₀, but returns the "junk" value of the original sequence a otherwise.

Equations

• a.from m₁ = Chapter6.Sequence.mk' (max a.m m₁) fun (x : { n : ℤ // n ≥ max a.m m₁ }) => a.seq ↑x

theorem Chapter6.Sequence.from_eval (a : Sequence) {m₁ n : ℤ} (hn : n ≥ m₁) : (a.from m₁).seq n = a.seq n

@[reducible, inline]

abbrev Real.Steady (ε : ℝ) (a : Chapter6.Sequence) : Prop

Definition 6.1.3 (ε-steady)

Equations

• ε.Steady a = ∀ n ≥ a.m, ∀ m ≥ a.m, ε.Close (a.seq n) (a.seq m)

theorem Real.steady_def (ε : ℝ) (a : Chapter6.Sequence) : ε.Steady a ↔ ∀ n ≥ a.m, ∀ m ≥ a.m, ε.Close (a.seq n) (a.seq m)

Definition 6.1.3 (ε-steady)

@[reducible, inline]

abbrev Real.EventuallySteady (ε : ℝ) (a : Chapter6.Sequence) : Prop

Definition 6.1.3 (Eventually ε-steady)

Equations

• ε.EventuallySteady a = ∃ N ≥ a.m, ε.Steady (a.from N)

theorem Real.eventuallySteady_def (ε : ℝ) (a : Chapter6.Sequence) : ε.EventuallySteady a ↔ ∃ N ≥ a.m, ε.Steady (a.from N)

Definition 6.1.3 (Eventually ε-steady)

theorem Real.Steady.mono {a : Chapter6.Sequence} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) (hsteady : ε₁.Steady a) : ε₂.Steady a

For fixed a, the function ε ↦ ε.Steady s is monotone

theorem Real.EventuallySteady.mono {a : Chapter6.Sequence} {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) (hsteady : ε₁.EventuallySteady a) : ε₂.EventuallySteady a

For fixed a, the function ε ↦ ε.EventuallySteady s is monotone

@[reducible, inline]

abbrev Chapter6.Sequence.IsCauchy (a : Sequence) : Prop

Definition 6.1.3 (Cauchy sequence)

Equations

• a.IsCauchy = ∀ ε > 0, ε.EventuallySteady a

theorem Chapter6.Sequence.isCauchy_def (a : Sequence) : a.IsCauchy ↔ ∀ ε > 0, ε.EventuallySteady a

Definition 6.1.3 (Cauchy sequence)

theorem Chapter6.Sequence.IsCauchy.coe (a : ℕ → ℝ) : (↑a).IsCauchy ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ j ≥ N, ∀ k ≥ N, dist (a j) (a k) ≤ ε

This is almost the same as Chapter5.Sequence.IsCauchy.coe

theorem Chapter6.Sequence.IsCauchy.mk {n₀ : ℤ} (a : { n : ℤ // n ≥ n₀ } → ℝ) : (mk' n₀ a).IsCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε

@[reducible, inline]

abbrev Chapter6.Sequence.ofChapter5Sequence (a : Chapter5.Sequence) : Sequence

Equations

• ↑a = { m := a.n₀, seq := fun (n : ℤ) => ↑(a.seq n), vanish := ⋯ }

@[implicit_reducible]

instance Chapter6.Chapter5.Sequence.inst_coe_sequence : Coe Chapter5.Sequence Sequence

Equations

• Chapter6.Chapter5.Sequence.inst_coe_sequence = { coe := Chapter6.Sequence.ofChapter5Sequence }

@[simp]

theorem Chapter6.Chapter5.coe_sequence_eval (a : Chapter5.Sequence) (n : ℤ) : (↑a).seq n = ↑(a.seq n)

theorem Chapter6.Sequence.is_steady_of_rat (ε : ℚ) (a : Chapter5.Sequence) : ε.Steady a ↔ (↑ε).Steady ↑a

theorem Chapter6.Sequence.is_eventuallySteady_of_rat (ε : ℚ) (a : Chapter5.Sequence) : ε.EventuallySteady a ↔ (↑ε).EventuallySteady ↑a

theorem Chapter6.Sequence.isCauchy_of_rat (a : Chapter5.Sequence) : a.IsCauchy ↔ (↑a).IsCauchy

Proposition 6.1.4

@[reducible, inline]

abbrev Real.CloseSeq (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : Prop

Definition 6.1.5

Equations

• ε.CloseSeq a L = ∀ n ≥ a.m, ε.Close (a.seq n) L

theorem Real.closeSeq_def (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : ε.CloseSeq a L ↔ ∀ n ≥ a.m, dist (a.seq n) L ≤ ε

Definition 6.1.5

@[reducible, inline]

abbrev Real.EventuallyClose (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : Prop

Definition 6.1.5

Equations

• ε.EventuallyClose a L = ∃ N ≥ a.m, ε.CloseSeq (a.from N) L

theorem Real.eventuallyClose_def (ε : ℝ) (a : Chapter6.Sequence) (L : ℝ) : ε.EventuallyClose a L ↔ ∃ N ≥ a.m, ε.CloseSeq (a.from N) L

Definition 6.1.5

theorem Real.CloseSeq.coe (ε : ℝ) (a : ℕ → ℝ) (L : ℝ) : ε.CloseSeq (↑a) L ↔ ∀ (n : ℕ), dist (a n) L ≤ ε

theorem Real.CloseSeq.mono {a : Chapter6.Sequence} {ε₁ ε₂ L : ℝ} (hε : ε₁ ≤ ε₂) (hclose : ε₁.CloseSeq a L) : ε₂.CloseSeq a L

theorem Real.EventuallyClose.mono {a : Chapter6.Sequence} {ε₁ ε₂ L : ℝ} (hε : ε₁ ≤ ε₂) (hclose : ε₁.EventuallyClose a L) : ε₂.EventuallyClose a L

@[reducible, inline]

abbrev Chapter6.Sequence.TendsTo (a : Sequence) (L : ℝ) : Prop

Equations

• a.TendsTo L = ∀ ε > 0, ε.EventuallyClose a L

theorem Chapter6.Sequence.tendsTo_def (a : Sequence) (L : ℝ) : a.TendsTo L ↔ ∀ ε > 0, ε.EventuallyClose a L

theorem Chapter6.Sequence.tendsTo_iff (a : Sequence) (L : ℝ) : a.TendsTo L ↔ ∀ ε > 0, ∃ (N : ℤ), ∀ n ≥ N, |a.seq n - L| ≤ ε

Exercise 6.1.2

noncomputable def Chapter6.seq_6_1_6 : Sequence

Equations

• Chapter6.seq_6_1_6 = ↑fun (n : ℕ) => 1 - 10 ^ (-↑n - 1)

theorem Chapter6.Sequence.tendsTo_unique (a : Sequence) {L L' : ℝ} (h : L ≠ L') : ¬(a.TendsTo L ∧ a.TendsTo L')

Proposition 6.1.7 (Uniqueness of limits)

@[reducible, inline]

abbrev Chapter6.Sequence.Convergent (a : Sequence) : Prop

Definition 6.1.8

Equations

• a.Convergent = ∃ (L : ℝ), a.TendsTo L

theorem Chapter6.Sequence.convergent_def (a : Sequence) : a.Convergent ↔ ∃ (L : ℝ), a.TendsTo L

Definition 6.1.8

@[reducible, inline]

abbrev Chapter6.Sequence.Divergent (a : Sequence) : Prop

Definition 6.1.8

Equations

• a.Divergent = ¬a.Convergent

theorem Chapter6.Sequence.divergent_def (a : Sequence) : a.Divergent ↔ ¬a.Convergent

Definition 6.1.8

@[reducible, inline]

noncomputable abbrev Chapter6.lim (a : Sequence) : ℝ

Definition 6.1.8. We give the limit of a sequence the junk value of 0 if it is not convergent.

Equations

• Chapter6.lim a = if h : a.Convergent then Exists.choose h else 0

theorem Chapter6.Sequence.lim_def {a : Sequence} (h : a.Convergent) : a.TendsTo (lim a)

Definition 6.1.8

theorem Chapter6.Sequence.lim_eq {a : Sequence} {L : ℝ} : a.TendsTo L ↔ a.Convergent ∧ lim a = L

Definition 6.1.8

theorem Chapter6.Sequence.lim_harmonic : (↑fun (n : ℕ) => (↑n + 1)⁻¹).Convergent ∧ (lim ↑fun (n : ℕ) => (↑n + 1)⁻¹) = 0

Proposition 6.1.11

theorem Chapter6.Sequence.IsCauchy.convergent {a : Sequence} (h : a.Convergent) : a.IsCauchy

Proposition 6.1.12 / Exercise 6.1.5

theorem Chapter6.Sequence.lim_eq_LIM {a : ℕ → ℚ} (h : (↑a).IsCauchy) : (↑↑a).TendsTo (Chapter5.Real.equivR (Chapter5.LIM a))

Proposition 6.1.15 / Exercise 6.1.6 (Formal limits are genuine limits)

@[reducible, inline]

abbrev Chapter6.Sequence.BoundedBy (a : Sequence) (M : ℝ) : Prop

Definition 6.1.16

Equations

• a.BoundedBy M = ∀ (n : ℤ), |a.seq n| ≤ M

theorem Chapter6.Sequence.boundedBy_def (a : Sequence) (M : ℝ) : a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M

Definition 6.1.16

@[reducible, inline]

abbrev Chapter6.Sequence.IsBounded (a : Sequence) : Prop

Definition 6.1.16

Equations

• a.IsBounded = ∃ M ≥ 0, a.BoundedBy M

theorem Chapter6.Sequence.isBounded_def (a : Sequence) : a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M

Definition 6.1.16

theorem Chapter6.Sequence.bounded_of_cauchy {a : Sequence} (h : a.IsCauchy) : a.IsBounded

theorem Chapter6.Sequence.bounded_of_convergent {a : Sequence} (h : a.Convergent) : a.IsBounded

Corollary 6.1.17

@[implicit_reducible]

instance Chapter6.Sequence.inst_add : Add Sequence

Equations

• Chapter6.Sequence.inst_add = { add := fun (a b : Chapter6.Sequence) => { m := min a.m b.m, seq := fun (n : ℤ) => a.seq n + b.seq n, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.add_eval {a b : Sequence} (n : ℤ) : (a + b).seq n = a.seq n + b.seq n

theorem Chapter6.Sequence.add_coe (a b : ℕ → ℝ) : ↑a + ↑b = ↑fun (n : ℕ) => a n + b n

theorem Chapter6.Sequence.tendsTo_add {a b : Sequence} {L M : ℝ} (ha : a.TendsTo L) (hb : b.TendsTo M) : (a + b).TendsTo (L + M)

Theorem 6.1.19(a) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem Chapter6.Sequence.lim_add {a b : Sequence} (ha : a.Convergent) (hb : b.Convergent) : (a + b).Convergent ∧ lim (a + b) = lim a + lim b

@[implicit_reducible]

instance Chapter6.Sequence.inst_mul : Mul Sequence

Equations

• Chapter6.Sequence.inst_mul = { mul := fun (a b : Chapter6.Sequence) => { m := min a.m b.m, seq := fun (n : ℤ) => a.seq n * b.seq n, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.mul_eval {a b : Sequence} (n : ℤ) : (a * b).seq n = a.seq n * b.seq n

theorem Chapter6.Sequence.mul_coe (a b : ℕ → ℝ) : ↑a * ↑b = ↑fun (n : ℕ) => a n * b n

theorem Chapter6.Sequence.tendsTo_mul {a b : Sequence} {L M : ℝ} (ha : a.TendsTo L) (hb : b.TendsTo M) : (a * b).TendsTo (L * M)

Theorem 6.1.19(b) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem Chapter6.Sequence.lim_mul {a b : Sequence} (ha : a.Convergent) (hb : b.Convergent) : (a * b).Convergent ∧ lim (a * b) = lim a * lim b

@[implicit_reducible]

instance Chapter6.Sequence.inst_smul : SMul ℝ Sequence

Equations

• Chapter6.Sequence.inst_smul = { smul := fun (c : ℝ) (a : Chapter6.Sequence) => { m := a.m, seq := fun (n : ℤ) => c * a.seq n, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.smul_eval {a : Sequence} (c : ℝ) (n : ℤ) : (c • a).seq n = c * a.seq n

theorem Chapter6.Sequence.smul_coe (c : ℝ) (a : ℕ → ℝ) : c • ↑a = ↑fun (n : ℕ) => c * a n

theorem Chapter6.Sequence.tendsTo_smul (c : ℝ) {a : Sequence} {L : ℝ} (ha : a.TendsTo L) : (c • a).TendsTo (c * L)

Theorem 6.1.19(c) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem Chapter6.Sequence.lim_smul (c : ℝ) {a : Sequence} (ha : a.Convergent) : (c • a).Convergent ∧ lim (c • a) = c * lim a

@[implicit_reducible]

instance Chapter6.Sequence.inst_sub : Sub Sequence

Equations

• Chapter6.Sequence.inst_sub = { sub := fun (a b : Chapter6.Sequence) => { m := min a.m b.m, seq := fun (n : ℤ) => a.seq n - b.seq n, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.sub_eval {a b : Sequence} (n : ℤ) : (a - b).seq n = a.seq n - b.seq n

theorem Chapter6.Sequence.sub_coe (a b : ℕ → ℝ) : ↑a - ↑b = ↑fun (n : ℕ) => a n - b n

theorem Chapter6.Sequence.tendsTo_sub {a b : Sequence} {L M : ℝ} (ha : a.TendsTo L) (hb : b.TendsTo M) : (a - b).TendsTo (L - M)

Theorem 6.1.19(d) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem Chapter6.Sequence.LIM_sub {a b : Sequence} (ha : a.Convergent) (hb : b.Convergent) : (a - b).Convergent ∧ lim (a - b) = lim a - lim b

@[implicit_reducible]

noncomputable instance Chapter6.Sequence.inst_inv : Inv Sequence

Equations

• Chapter6.Sequence.inst_inv = { inv := fun (a : Chapter6.Sequence) => { m := a.m, seq := fun (n : ℤ) => (a.seq n)⁻¹, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.inv_eval {a : Sequence} (n : ℤ) : a⁻¹.seq n = (a.seq n)⁻¹

theorem Chapter6.Sequence.inv_coe (a : ℕ → ℝ) : (↑a)⁻¹ = ↑fun (n : ℕ) => (a n)⁻¹

theorem Chapter6.Sequence.tendsTo_inv {a : Sequence} {L : ℝ} (ha : a.TendsTo L) (hnon : L ≠ 0) : a⁻¹.TendsTo L⁻¹

Theorem 6.1.19(e) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem Chapter6.Sequence.lim_inv {a : Sequence} (ha : a.Convergent) (hnon : lim a ≠ 0) : a⁻¹.Convergent ∧ lim a⁻¹ = (lim a)⁻¹

@[implicit_reducible]

noncomputable instance Chapter6.Sequence.inst_div : Div Sequence

Equations

• Chapter6.Sequence.inst_div = { div := fun (a b : Chapter6.Sequence) => { m := min a.m b.m, seq := fun (n : ℤ) => a.seq n / b.seq n, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.div_eval {a b : Sequence} (n : ℤ) : (a / b).seq n = a.seq n / b.seq n

theorem Chapter6.Sequence.div_coe (a b : ℕ → ℝ) : ↑a / ↑b = ↑fun (n : ℕ) => a n / b n

theorem Chapter6.Sequence.tendsTo_div {a b : Sequence} {L M : ℝ} (ha : a.TendsTo L) (hb : b.TendsTo M) (hnon : M ≠ 0) : (a / b).TendsTo (L / M)

Theorem 6.1.19(f) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem Chapter6.Sequence.lim_div {a b : Sequence} (ha : a.Convergent) (hb : b.Convergent) (hnon : lim b ≠ 0) : (a / b).Convergent ∧ lim (a / b) = lim a / lim b

@[implicit_reducible]

instance Chapter6.Sequence.inst_max : Max Sequence

Equations

• Chapter6.Sequence.inst_max = { max := fun (a b : Chapter6.Sequence) => { m := min a.m b.m, seq := fun (n : ℤ) => max (a.seq n) (b.seq n), vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.max_eval {a b : Sequence} (n : ℤ) : (a ⊔ b).seq n = max (a.seq n) (b.seq n)

theorem Chapter6.Sequence.max_coe (a b : ℕ → ℝ) : ↑a ⊔ ↑b = ↑fun (n : ℕ) => max (a n) (b n)

theorem Chapter6.Sequence.tendsTo_max {a b : Sequence} {L M : ℝ} (ha : a.TendsTo L) (hb : b.TendsTo M) : (a ⊔ b).TendsTo (max L M)

Theorem 6.1.19(g) (limit laws). The Sequence.TendsTo version is more usable than the lim version in applications.

theorem Chapter6.Sequence.lim_max {a b : Sequence} (ha : a.Convergent) (hb : b.Convergent) : (a ⊔ b).Convergent ∧ lim (a ⊔ b) = max (lim a) (lim b)

@[implicit_reducible]

instance Chapter6.Sequence.inst_min : Min Sequence

Equations

• Chapter6.Sequence.inst_min = { min := fun (a b : Chapter6.Sequence) => { m := min a.m b.m, seq := fun (n : ℤ) => min (a.seq n) (b.seq n), vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.min_eval {a b : Sequence} (n : ℤ) : (a ⊓ b).seq n = min (a.seq n) (b.seq n)

theorem Chapter6.Sequence.min_coe (a b : ℕ → ℝ) : ↑a ⊓ ↑b = ↑fun (n : ℕ) => min (a n) (b n)

theorem Chapter6.Sequence.tendsTo_min {a b : Sequence} {L M : ℝ} (ha : a.TendsTo L) (hb : b.TendsTo M) : (a ⊓ b).TendsTo (min L M)

Theorem 6.1.19(h) (limit laws)

theorem Chapter6.Sequence.lim_min {a b : Sequence} (ha : a.Convergent) (hb : b.Convergent) : (a ⊓ b).Convergent ∧ lim (a ⊓ b) = min (lim a) (lim b)

theorem Chapter6.Sequence.mono_if {a : ℕ → ℝ} (ha : ∀ (n : ℕ), a (n + 1) > a n) {n m : ℕ} (hnm : m > n) : a m > a n

Exercise 6.1.1

theorem Chapter6.Sequence.tendsTo_of_from {a : Sequence} {c : ℝ} (m : ℤ) : a.TendsTo c ↔ (a.from m).TendsTo c

Exercise 6.1.3

theorem Chapter6.Sequence.tendsTo_of_shift {a : Sequence} {c : ℝ} (k : ℕ) : a.TendsTo c ↔ (mk' a.m fun (n : { n : ℤ // n ≥ a.m }) => a.seq (↑n + ↑k)).TendsTo c

Exercise 6.1.4

theorem Chapter6.Sequence.isBounded_of_rat (a : Chapter5.Sequence) : a.IsBounded ↔ (↑a).IsBounded

Exercise 6.1.7

theorem Chapter6.Sequence.lim_div_fail : ∃ (a : Sequence) (b : Sequence), a.Convergent ∧ b.Convergent ∧ lim b = 0 ∧ ¬((a / b).Convergent ∧ lim (a / b) = lim a / lim b)

Exercise 6.1.9

theorem Chapter6.Chapter5.Sequence.IsCauchy_iff (a : Chapter5.Sequence) : a.IsCauchy ↔ ∀ ε > 0, ∃ N ≥ a.n₀, ∀ n ≥ N, ∀ m ≥ N, ↑|a.seq n - a.seq m| ≤ ε

@[reducible, inline]

abbrev Real.SeqCloseSeq (ε : ℝ) (a b : Chapter5.Sequence) : Prop

Equations

• ε.SeqCloseSeq a b = ∀ n ≥ a.n₀, n ≥ b.n₀ → ε.Close ↑(a.seq n) ↑(b.seq n)

@[reducible, inline]

abbrev Real.SeqEventuallyClose (ε : ℝ) (a b : Chapter5.Sequence) : Prop

Equations

• ε.SeqEventuallyClose a b = ∃ (N : ℤ), ε.SeqCloseSeq (a.from N) (b.from N)

@[reducible, inline]

abbrev Chapter5.Sequence.RatEquiv (a b : ℕ → ℚ) : Prop

Equations

• Chapter5.Sequence.RatEquiv a b = ∀ ε > 0, ε.SeqEventuallyClose ↑a ↑b

theorem Chapter6.Chapter5.Sequence.equiv_rat (a b : ℕ → ℚ) : Chapter5.Sequence.Equiv a b ↔ Chapter5.Sequence.RatEquiv a b

Exercise 6.1.10