## Stream: maths

### Topic: complementary sequences

#### Johan Commelin (Sep 03 2019 at 20:16):

Suppose I have a strictly monotonous f : nat → nat. How hard is it to define g : nat → nat that is the strictly monotonous sequence of numbers that don't occur in the sequence f...

#### Floris van Doorn (Sep 03 2019 at 20:20):

You need additional assumptions on f, right? You cannot define g when f = id.

#### Chris Hughes (Sep 03 2019 at 20:27):

I constructively proved at some point that every infinite subset of nat was denumerable.

#### Chris Hughes (Sep 03 2019 at 20:28):

It's in mathlib. It was part of the denumerability of Q proof.

#### Floris van Doorn (Sep 03 2019 at 20:29):

The Figure Figure sequences is a bit tricky since it is a mutual definition. I would probably define them mutually, together with R_list which is equal to (list.range n).map R

#### Patrick Massot (Sep 03 2019 at 20:30):

What's the point of this sequence? I skimmed through the wikipedia page without understand why it could be interesting

#### Kevin Buzzard (Sep 03 2019 at 22:40):

Just because it's in the OEIS doesn't mean it's interesting to someone who doesn't care about sequences. The OEIS contains huge collections of uninteresting sequences now, which to be honest is really really good, because whenever someone like me runs into a sequence it's now very likely it will be there. Someone like you is I guess far less likely to be running into sequences of positive integers in your day job.

#### Kevin Buzzard (Sep 03 2019 at 22:43):

"This is the lexicographically earliest sequence that together with its first differences contains every positive integer exactly once". If that floats your boat, then that's the point of the sequence.

Last updated: May 06 2021 at 18:20 UTC