defining subsequence

Stream: new members

[Sabbir Rahman]

I couldn't find any good documentation/guide of how to define subsequences in mathlib. Of course I can define subsequence to be how it is convenient for my requirements, but I wanted to know how mathlib does it so that I can use related theorems easily. after searching for weierstrass, I found tendsto_subseq_of_bounded which does tell me how to define it, but is there any common place where this is explicitly stated like "We use subsequences with this definition"

[Etienne Marion]

I don’t think there is such a place, this I think is the standard way to talk about subsequences in maths generally.

[Sabbir Rahman]

I guess so, though when I was thinking about subsequences, first thing that came to mind was "leaving out" terms, so I was confused how that'd translate to lean.

[Etienne Marion]

Again this is not specific to Lean, it is how it is usually done in maths.

[Matt Diamond]

if you're working with finite sequences there's docs#List.Sublist

[Scott Carnahan]

It looks like both order embeddings and strictly monotone maps are used.

docs#Nat.orderEmbeddingOfSet produces an order embedding from an infinite subset of natural numbers.

docs#Filter.extraction_of_frequently_atTop' produces a strictMono map from an unbounded subset of natural numbers (but I think it could be moved: #24207)

[Sabbir Rahman]

Scott Carnahan said:

It looks like both order embeddings and strictly monotone maps are used.

docs#Nat.orderEmbeddingOfSet produces an order embedding from an infinite subset of natural numbers.

docs#Filter.extraction_of_frequently_atTop' produces a strictMono map from an unbounded subset of natural numbers (but I think it could be moved: #24207)

Yeah this is what I was talking about, even though the definition of subsequence in math is in general well defined, there can be multiple way to state this by using different things in mathlib. Maybe a definition of subsequence in mathlib would be good?