Exercise 6.1.10 mismatch

Stream: Analysis I

[Rado Kirov]

It seems that the exercise in the companion doesn't match the book.

In the book

Exercise 6.1.10 Show that the concept of equivalent Cauchy sequence, as defined in Definition
5.2.6, does not change if ε is required to be positive real instead of positive rational. ...

while currently in the companion

/-- Exercise 6.1.10 -/
theorem Chapter5.Sequence.IsCauchy_iff (a:Chapter5.Sequence) :
    a.IsCauchy ↔ ∀ ε > (0:ℝ), ∃ N ≥ a.n₀, ∀ n ≥ N, ∀ m ≥ N, |a n - a m| ≤ ε := by sorry

(which is a theorem already proved under a different name earlier in the chapter)

I think it should be something like

abbrev Real.SeqCloseSeq (ε: ℝ) (a b: Chapter5.Sequence) : Prop :=
  ∀ n, n ≥ a.n₀ → n ≥ b.n₀ → ε.Close (a n) (b n)

abbrev Real.SeqEventuallyClose (ε: ℝ) (a b: Chapter5.Sequence): Prop :=
  ∃ N, SeqCloseSeq ε (a.from N) (b.from N)

abbrev Chapter5.Sequence.RatEquiv (a b: ℕ → ℚ) : Prop :=
  ∀ (ε:ℝ), ε > 0 → Real.SeqEventuallyClose ε (a:Chapter5.Sequence) (b:Chapter5.Sequence)

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

with the new definitions added. I don't fully understand how namespacing works for allowing one to write ε .Close ... vs Close ε ... so wrote them in the expanded fort.

[Terence Tao]

Hmm, no idea how that happened. Yes, the new version sounds good. As for namespacing, anything of the form Type.Subtype can replaceType by the first argument that matches that type, so for instance Real.SeqCloseSeq ε can alternatively be written as ε.SeqCloseSeq.

[Rado Kirov]

Sg, will send a PR tonight

[Rado Kirov]

https://github.com/teorth/analysis/pull/383 the issue with the namespaces had to do with I can't write def Real.X while in opened namespace Chapter6, because it introduces a Chapter6.Real which is different from _root_.Real. Simply closing the namespace before defining the new Real.X definitions fixed the problem.