'extraction'?

Stream: new members

[leafGecko]

What is this 'extraction' thing ..? Googling didn't find this term, and from definition it looks just like increasing function...
And it's appearing everywhere in the tutorial .....
def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

[leafGecko]

image.png I am deeply confused ...

[Mario Carneiro]

It's not just a (strictly) increasing function, it is a strictly increasing function on nat, which has some additional properties. I guess the reason it is called that is that it extracts a subsequence of natural numbers

[Kevin Buzzard]

Right -- it's a subsequence.

[leafGecko]

that makes sense. Thanks!

[Patrick Massot]

That may be a translation issue. I can tell you for sure it's a an extraction in French. Maybe I made up the English translation but nobody ever complained.

[Mario Carneiro]

I don't see anything relevant at https://fr.wikipedia.org/wiki/Extraction, how is the french word used here?

[Mario Carneiro]

the wikipedia page only mentions "extraction of square roots / n-th roots" which is used occasionally in english but seems unrelated to the usage here