@[reducible, inline]

abbrev Rat.CloseSeq (ε : ℚ) (a b : Chapter5.Sequence) : Prop

Equations

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

@[reducible, inline]

abbrev Rat.EventuallyClose (ε : ℚ) (a b : Chapter5.Sequence) : Prop

Equations

• ε.EventuallyClose a b = ∃ (N : ℤ), ε.CloseSeq (a.from N) (b.from N)

theorem Chapter5.Rat.closeSeq_def (ε : ℚ) (a b : Sequence) : ε.CloseSeq a b ↔ ∀ n ≥ a.n₀, n ≥ b.n₀ → ε.Close (a.seq n) (b.seq n)

Definition 5.2.1 ($ε$-close sequences)

theorem Chapter5.Rat.eventuallyClose_def (ε : ℚ) (a b : Sequence) : ε.EventuallyClose a b ↔ ∃ (N : ℤ), ε.CloseSeq (a.from N) (b.from N)

Definition 5.2.3 (Eventually ε-close sequences)

theorem Chapter5.Rat.eventuallyClose_iff (ε : ℚ) (a b : ℕ → ℚ) : ε.EventuallyClose ↑a ↑b ↔ ∃ (N : ℕ), ∀ n ≥ N, |a n - b n| ≤ ε

Definition 5.2.3 (Eventually ε-close sequences)

@[reducible, inline]

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

Definition 5.2.6 (Equivalent sequences)

Equations

• Chapter5.Sequence.Equiv a b = ∀ ε > 0, ε.EventuallyClose ↑a ↑b

theorem Chapter5.Sequence.equiv_def (a b : ℕ → ℚ) : Equiv a b ↔ ∀ ε > 0, ε.EventuallyClose ↑a ↑b

Definition 5.2.6 (Equivalent sequences)

theorem Chapter5.Sequence.equiv_iff (a b : ℕ → ℚ) : Equiv a b ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |a n - b n| ≤ ε

Definition 5.2.6 (Equivalent sequences)

theorem Chapter5.Sequence.equiv_example : Equiv (fun (n : ℕ) => 1 + 10 ^ (-↑n - 1)) fun (n : ℕ) => 1 - 10 ^ (-↑n - 1)

Proposition 5.2.8

theorem Chapter5.Sequence.isCauchy_of_equiv {a b : ℕ → ℚ} (hab : Equiv a b) : (↑a).IsCauchy ↔ (↑b).IsCauchy

Exercise 5.2.1

theorem Chapter5.Sequence.isBounded_of_eventuallyClose {ε : ℚ} {a b : ℕ → ℚ} (hab : ε.EventuallyClose ↑a ↑b) : (↑a).IsBounded ↔ (↑b).IsBounded

Exercise 5.2.2