Extensionality on Sequence

Stream: Analysis I

[Li Xuanji]

We define sequences as follows

@[ext]
structure Sequence where
  n₀ : ℤ
  seq : ℤ → ℚ
  vanish : ∀ n < n₀, seq n = 0

This means that if two Sequences have equal seq components (i.e. ∀ i, a.seq i = b.seq i) but unequal n₀ components, they are not considered equal. If I want to redefine equality of sequences to not care about unequal n₀ components, how might I do it - as a quotient?

(I'm asking mostly for curiosity, I don't expect this to cause problems as we don't work with Sequence equality that often. Where I could see this becoming a problem is reasoning about finite sequences (say we define them by the support being contained in some bounded interval, i.e. vanish' : ∀ n > n_max, seq n = 0))

[Aaron Liu]

See for example docs#DFinsupp

[Rado Kirov]

hmm, that would mean Sequence.from wouldn't work in the quotient. To me the more interesting question is why don't we define Sequence as \N -> Q like in the book?

[Terence Tao]

I think the operation of shifting a sequence, eg $(a_{n-m})_{n=m}^\infty$, worked better with integer subtraction rather than natural number subtraction.